--- a/src/Pure/General/symbol.scala Tue Jan 16 15:42:21 2018 +0100
+++ b/src/Pure/General/symbol.scala Tue Jan 16 15:53:42 2018 +0100
@@ -573,16 +573,12 @@
/* formal comments */
val comment: Symbol = "\\<comment>"
+ val cancel: Symbol = "\\<^cancel>"
+ val latex: Symbol = "\\<^latex>"
+
def comment_decoded: Symbol = symbols.comment_decoded
- def is_comment(sym: Symbol): Boolean = sym == comment || sym == comment_decoded
-
- val cancel: Symbol = "\\<^cancel>"
def cancel_decoded: Symbol = symbols.cancel_decoded
- def is_cancel(sym: Symbol): Boolean = sym == cancel || sym == cancel_decoded
-
- val latex: Symbol = "\\<^latex>"
def latex_decoded: Symbol = symbols.latex_decoded
- def is_latex(sym: Symbol): Boolean = sym == latex || sym == latex_decoded
/* cartouches */