diff -r dec7cc38a5dc -r 6dc5506ad449 etc/symbols
--- 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: <<