# HG changeset patch
# User wenzelm
# Date 1512424471 -3600
# Node ID 85d10959c2e44242c0db9cd71de7bfe3bda240d1
# Parent  b023f64e0d162e6518c2e23ec03f04136b91b1a3
tuned signature;

diff -r b023f64e0d16 -r 85d10959c2e4 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Dec 04 22:52:16 2017 +0100
+++ b/src/Pure/General/symbol.scala	Mon Dec 04 22:54:31 2017 +0100
@@ -563,6 +563,9 @@
   def is_open(sym: Symbol): Boolean = sym == open_decoded || sym == open
   def is_close(sym: Symbol): Boolean = sym == close_decoded || sym == close
 
+  def cartouche(s: String): String = open + s + close
+  def cartouche_decoded(s: String): String = open_decoded + s + close_decoded
+
 
   /* symbols for symbolic identifiers */
 
diff -r b023f64e0d16 -r 85d10959c2e4 src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Mon Dec 04 22:52:16 2017 +0100
+++ b/src/Pure/Tools/update_cartouches.scala	Mon Dec 04 22:54:31 2017 +0100
@@ -11,9 +11,6 @@
 {
   /* update cartouches */
 
-  private def cartouche(s: String): String =
-    Symbol.open + s + Symbol.close
-
   private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r
 
   val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r
@@ -27,7 +24,7 @@
             ant match {
               case Antiquote.Antiq(Text_Antiq(body)) =>
                 Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match {
-                  case List(tok) => Antiquote.Control(cartouche(tok.content))
+                  case List(tok) => Antiquote.Control(Symbol.cartouche(tok.content))
                   case _ => ant
                 }
               case _ => ant
@@ -45,10 +42,10 @@
     val text1 =
       (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
         yield {
-          if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
+          if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content)
           else if (tok.kind == Token.Kind.VERBATIM) {
             tok.content match {
-              case Verbatim_Body(s) => cartouche(s)
+              case Verbatim_Body(s) => Symbol.cartouche(s)
               case s => tok.source
             }
           }
@@ -68,7 +65,7 @@
 
               if (content == content1) tok.source
               else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1)
-              else cartouche(content1)
+              else Symbol.cartouche(content1)
             }
             else tok.source
           }).mkString