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 = {