src/Pure/General/comment.scala
changeset 67449 1caeb087d957
parent 67438 fdb7b995974d
child 69891 def3ec9cdb7e
--- 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 =
   {