src/Pure/General/symbol.ML

--- a/src/Pure/General/symbol.ML	Wed Nov 04 23:27:00 2015 +0100
+++ b/src/Pure/General/symbol.ML	Thu Nov 05 00:02:30 2015 +0100
@@ -10,6 +10,7 @@
   val STX: symbol
   val DEL: symbol
   val space: symbol
+  val comment: symbol
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
@@ -93,6 +94,8 @@
 
 val space = chr 32;
 
+val comment = "\\<comment>";
+
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;