--- a/src/Pure/General/symbol.scala Sat Mar 09 23:57:07 2019 +0100
+++ b/src/Pure/General/symbol.scala Sun Mar 10 00:21:34 2019 +0100
@@ -493,6 +493,7 @@
/* misc symbols */
val newline_decoded = decode(newline)
+ val marker_decoded = decode(marker)
val comment_decoded = decode(comment)
val cancel_decoded = decode(cancel)
val latex_decoded = decode(latex)
@@ -578,6 +579,14 @@
else str
+ /* marker */
+
+ val marker: Symbol = "\\<marker>"
+ def marker_decoded: Symbol = symbols.marker_decoded
+
+ lazy val is_marker: Set[Symbol] = Set(marker, marker_decoded)
+
+
/* formal comments */
val comment: Symbol = "\\<comment>"