--- a/etc/symbols Sat Mar 09 13:24:59 2019 +0100
+++ b/etc/symbols Sat Mar 09 13:35:49 2019 +0100
@@ -359,6 +359,7 @@
\<hole> code: 0x002311
\<newline> code: 0x0023ce
\<comment> code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono
+\<marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<^latex> group: document argument: cartouche
\<open> code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: <<