--- a/etc/symbols Sun Mar 10 15:31:24 2019 +0100
+++ b/etc/symbols Sun Mar 10 21:12:29 2019 +0100
@@ -359,9 +359,9 @@
\<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
+\<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<open> code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: <<
\<close> code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >>
\<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono