author | wenzelm |
Thu, 04 Feb 2016 13:21:47 +0100 | |
changeset 62260 | f82f6c7476a1 |
parent 62259 | 7afbd7fc32fd |
child 62261 | 74dc98bd9f51 |
etc/symbols | file | annotate | diff | comparison | revisions |
--- 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