# HG changeset patch
# User wenzelm
# Date 1515955489 -3600
# Node ID 84e143e64336d47c8a2f95e417f6b2f96041ef79
# Parent  149b742070e9493a769fd444e5e9a4e40e682336
more operations;

diff -r 149b742070e9 -r 84e143e64336 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sun Jan 14 16:48:21 2018 +0100
+++ b/src/Pure/General/completion.scala	Sun Jan 14 19:44:49 2018 +0100
@@ -220,7 +220,7 @@
           val replacement =
             List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match {
               case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE =>
-                Symbol.open_decoded + xname1 + Symbol.close_decoded
+                Library.cartouche_decoded(xname1)
               case List(_, List(tok)) if tok.is_name => xname1
               case _ => quote(xname1)
             }
diff -r 149b742070e9 -r 84e143e64336 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Jan 14 16:48:21 2018 +0100
+++ b/src/Pure/library.scala	Sun Jan 14 19:44:49 2018 +0100
@@ -148,6 +148,12 @@
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
 
+  /* cartouche */
+
+  def cartouche(s: String): String = Symbol.open + s + Symbol.close
+  def cartouche_decoded(s: String): String = Symbol.open_decoded + s + Symbol.close_decoded
+
+
   /* quote */
 
   def quote(s: String): String = "\"" + s + "\""