# HG changeset patch # User wenzelm # Date 1445448194 -7200 # Node ID 42afc789add83f8cfab7dd8cb1adfb6101e6a1a9 # Parent 56a167b31a7ff2a4fedfe55a6462aa11872b1507 rendering for \<^verbatim>; diff -r 56a167b31a7f -r 42afc789add8 NEWS --- a/NEWS Wed Oct 21 18:00:12 2015 +0200 +++ b/NEWS Wed Oct 21 19:23:14 2015 +0200 @@ -62,7 +62,9 @@ * There is a new short form for antiquotations with a single argument that is a cartouche: \<^name>\...\ is equivalent to @{name \...\} and -\...\ without control symbol is equivalent to @{cartouche \...\}. +\...\ without control symbol is equivalent to @{cartouche \...\}. The +standard Isabelle fonts provide glyphs to render important control +symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>". * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}. Consequently, \...\ without any decoration prints literal quasi-formal diff -r 56a167b31a7f -r 42afc789add8 etc/symbols --- a/etc/symbols Wed Oct 21 18:00:12 2015 +0200 +++ b/etc/symbols Wed Oct 21 19:23:14 2015 +0200 @@ -359,6 +359,7 @@ \<^item> code: 0x0025aa group: control font: IsabelleText \<^enum> code: 0x0025b8 group: control font: IsabelleText \<^descr> code: 0x0027a7 group: control font: IsabelleText +\<^verbatim> code: 0x0025a9 group: control font: IsabelleText \<^emph> code: 0x002217 group: control font: IsabelleText \<^bold> code: 0x002759 group: control font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText