# HG changeset patch
# User wenzelm
# Date 1454588507 -3600
# Node ID f82f6c7476a1f4faafd2c84e57ba2fcb19136227
# Parent  7afbd7fc32fd55782cc2b0ed4a1120675e8792f8
clarified;

diff -r 7afbd7fc32fd -r f82f6c7476a1 etc/symbols
--- 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