rendering for \<^verbatim>;
authorwenzelm
Wed Oct 21 19:23:14 2015 +0200 (2015-10-21)
changeset 6150142afc789add8
parent 61500 56a167b31a7f
child 61502 760e21900b01
rendering for \<^verbatim>;
NEWS
etc/symbols
     1.1 --- a/NEWS	Wed Oct 21 18:00:12 2015 +0200
     1.2 +++ b/NEWS	Wed Oct 21 19:23:14 2015 +0200
     1.3 @@ -62,7 +62,9 @@
     1.4  
     1.5  * There is a new short form for antiquotations with a single argument
     1.6  that is a cartouche: \<^name>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
     1.7 -\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
     1.8 +\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. The
     1.9 +standard Isabelle fonts provide glyphs to render important control
    1.10 +symbols, e.g. "\<^verbatim>", "\<^emph>", "\<^bold>".
    1.11  
    1.12  * Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
    1.13  Consequently, \<open>...\<close> without any decoration prints literal quasi-formal
     2.1 --- a/etc/symbols	Wed Oct 21 18:00:12 2015 +0200
     2.2 +++ b/etc/symbols	Wed Oct 21 19:23:14 2015 +0200
     2.3 @@ -359,6 +359,7 @@
     2.4  \<^item>                code: 0x0025aa  group: control  font: IsabelleText
     2.5  \<^enum>                code: 0x0025b8  group: control  font: IsabelleText
     2.6  \<^descr>               code: 0x0027a7  group: control  font: IsabelleText
     2.7 +\<^verbatim>            code: 0x0025a9  group: control  font: IsabelleText
     2.8  \<^emph>                code: 0x002217  group: control  font: IsabelleText
     2.9  \<^bold>                code: 0x002759  group: control  font: IsabelleText
    2.10  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText