tuned signature;
authorwenzelm
Tue Jan 16 15:53:42 2018 +0100 (2018-01-16 ago)
changeset 674491caeb087d957
parent 67448 dbb1f02e667d
child 67450 b0ae74b86ef3
tuned signature;
src/Pure/General/comment.scala
src/Pure/General/symbol.scala
     1.1 --- a/src/Pure/General/comment.scala	Tue Jan 16 15:42:21 2018 +0100
     1.2 +++ b/src/Pure/General/comment.scala	Tue Jan 16 15:53:42 2018 +0100
     1.3 @@ -21,7 +21,8 @@
     1.4        Symbol.cancel, Symbol.cancel_decoded,
     1.5        Symbol.latex, Symbol.latex_decoded)
     1.6  
     1.7 -  def symbols_blanks(sym: Symbol.Symbol): Boolean = Symbol.is_comment(sym)
     1.8 +  lazy val symbols_blanks: Set[Symbol.Symbol] =
     1.9 +    Set(Symbol.comment, Symbol.comment_decoded)
    1.10  
    1.11    def content(source: String): String =
    1.12    {
     2.1 --- a/src/Pure/General/symbol.scala	Tue Jan 16 15:42:21 2018 +0100
     2.2 +++ b/src/Pure/General/symbol.scala	Tue Jan 16 15:53:42 2018 +0100
     2.3 @@ -573,16 +573,12 @@
     2.4    /* formal comments */
     2.5  
     2.6    val comment: Symbol = "\\<comment>"
     2.7 +  val cancel: Symbol = "\\<^cancel>"
     2.8 +  val latex: Symbol = "\\<^latex>"
     2.9 +
    2.10    def comment_decoded: Symbol = symbols.comment_decoded
    2.11 -  def is_comment(sym: Symbol): Boolean = sym == comment || sym == comment_decoded
    2.12 -
    2.13 -  val cancel: Symbol = "\\<^cancel>"
    2.14    def cancel_decoded: Symbol = symbols.cancel_decoded
    2.15 -  def is_cancel(sym: Symbol): Boolean = sym == cancel || sym == cancel_decoded
    2.16 -
    2.17 -  val latex: Symbol = "\\<^latex>"
    2.18    def latex_decoded: Symbol = symbols.latex_decoded
    2.19 -  def is_latex(sym: Symbol): Boolean = sym == latex || sym == latex_decoded
    2.20  
    2.21  
    2.22    /* cartouches */