Summary
- 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 added | lib/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) |