Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
Changeset 63683:87c6158f4ef4 by wenzelm:
more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
The file was addedlib/fonts/Vacuous.sfd
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified etc/isabelle.css (diff)
The file was modified src/Pure/Thy/present.scala (diff)