changeset 62260 | f82f6c7476a1 |
parent 62234 | 7cc9d7b822ae |
child 62440 | 31fa592761da |
--- a/etc/symbols Thu Feb 04 12:11:27 2016 +0100 +++ b/etc/symbols Thu Feb 04 13:21:47 2016 +0100 @@ -357,7 +357,7 @@ \<some> code: 0x0003f5 \<hole> code: 0x002311 \<newline> code: 0x0023ce -\<comment> code: 0x002015 font: IsabelleText +\<comment> code: 0x002015 group: document font: IsabelleText \<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: << \<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \<here> code: 0x002302 font: IsabelleText