# HG changeset patch
# User wenzelm
# Date 1516114422 -3600
# Node ID 1caeb087d957f6147c98a5d40d197ac57cf64ea2
# Parent  dbb1f02e667d1082bddaeafc4568deecd0b67145
tuned signature;

diff -r dbb1f02e667d -r 1caeb087d957 src/Pure/General/comment.scala
--- a/src/Pure/General/comment.scala	Tue Jan 16 15:42:21 2018 +0100
+++ b/src/Pure/General/comment.scala	Tue Jan 16 15:53:42 2018 +0100
@@ -21,7 +21,8 @@
       Symbol.cancel, Symbol.cancel_decoded,
       Symbol.latex, Symbol.latex_decoded)
 
-  def symbols_blanks(sym: Symbol.Symbol): Boolean = Symbol.is_comment(sym)
+  lazy val symbols_blanks: Set[Symbol.Symbol] =
+    Set(Symbol.comment, Symbol.comment_decoded)
 
   def content(source: String): String =
   {
diff -r dbb1f02e667d -r 1caeb087d957 src/Pure/General/symbol.scala
--- 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 */