tuned signature;
authorwenzelm
Mon Dec 04 22:54:31 2017 +0100 (4 months ago)
changeset 6713185d10959c2e4
parent 67130 b023f64e0d16
child 67132 336831647779
tuned signature;
src/Pure/General/symbol.scala
src/Pure/Tools/update_cartouches.scala
     1.1 --- a/src/Pure/General/symbol.scala	Mon Dec 04 22:52:16 2017 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Mon Dec 04 22:54:31 2017 +0100
     1.3 @@ -563,6 +563,9 @@
     1.4    def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
     1.5    def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
     1.6  
     1.7 +  def cartouche(s: String): String = open + s + close
     1.8 +  def cartouche_decoded(s: String): String = open_decoded + s + close_decoded
     1.9 +
    1.10  
    1.11    /* symbols for symbolic identifiers */
    1.12  
     2.1 --- a/src/Pure/Tools/update_cartouches.scala	Mon Dec 04 22:52:16 2017 +0100
     2.2 +++ b/src/Pure/Tools/update_cartouches.scala	Mon Dec 04 22:54:31 2017 +0100
     2.3 @@ -11,9 +11,6 @@
     2.4  {
     2.5    /* update cartouches */
     2.6  
     2.7 -  private def cartouche(s: String): String =
     2.8 -    Symbol.open + s + Symbol.close
     2.9 -
    2.10    private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
    2.11  
    2.12    val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
    2.13 @@ -27,7 +24,7 @@
    2.14              ant match {
    2.15                case Antiquote.Antiq(Text_Antiq(body)) =>
    2.16                  Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
    2.17 -                  case List(tok) => Antiquote.Control(cartouche(tok.content))
    2.18 +                  case List(tok) => Antiquote.Control(Symbol.cartouche(tok.content))
    2.19                    case _ => ant
    2.20                  }
    2.21                case _ => ant
    2.22 @@ -45,10 +42,10 @@
    2.23      val text1 =
    2.24        (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
    2.25          yield {
    2.26 -          if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
    2.27 +          if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content)
    2.28            else if (tok.kind == Token.Kind.VERBATIM) {
    2.29              tok.content match {
    2.30 -              case Verbatim_Body(s) => cartouche(s)
    2.31 +              case Verbatim_Body(s) => Symbol.cartouche(s)
    2.32                case s => tok.source
    2.33              }
    2.34            }
    2.35 @@ -68,7 +65,7 @@
    2.36  
    2.37                if (content == content1) tok.source
    2.38                else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
    2.39 -              else cartouche(content1)
    2.40 +              else Symbol.cartouche(content1)
    2.41              }
    2.42              else tok.source
    2.43            }).mkString