more operations;

--- 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)
             }

--- 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 + "\""