etc/symbols
changeset 69891 def3ec9cdb7e
parent 69885 6dc5506ad449
child 70015 c8e08d8ffb93
--- 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