Fri, 22 Dec 2017 15:49:44 +0100 | wenzelm | HTML rendering of \<^control> as in Isabelle/jEdit; | file | diff | annotate |
Fri, 12 Aug 2016 22:51:45 +0200 | 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; | file | diff | annotate |