# 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>\<open>...\<close> is equivalent to @{name \<open>...\<close>} and
-\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}.
+\<open>...\<close> without control symbol is equivalent to @{cartouche \<open>...\<close>}. 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, \<open>...\<close> 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