# HG changeset patch
# User wenzelm
# Date 1515961543 -3600
# Node ID e446505a4ec61606061eac6902426688d49f0e0f
# Parent  f83c1842a55907c5426611f92fbcfa3b5a9317fb
eliminated clones;

diff -r f83c1842a559 -r e446505a4ec6 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sun Jan 14 20:58:41 2018 +0100
+++ b/src/Pure/General/completion.scala	Sun Jan 14 21:25:43 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 =>
-                Library.cartouche_decoded(xname1)
+                Symbol.cartouche_decoded(xname1)
               case List(_, List(tok)) if tok.is_name => xname1
               case _ => quote(xname1)
             }
diff -r f83c1842a559 -r e446505a4ec6 src/Pure/Tools/update_comments.scala
--- a/src/Pure/Tools/update_comments.scala	Sun Jan 14 20:58:41 2018 +0100
+++ b/src/Pure/Tools/update_comments.scala	Sun Jan 14 21:25:43 2018 +0100
@@ -21,7 +21,7 @@
           rest.dropWhile(_.is_space) match {
             case tok1 :: rest1 if tok1.is_text =>
               val txt = Symbol.trim_blanks(tok1.content)
-              update(rest1, (Symbol.comment + Symbol.space + Library.cartouche(txt)) :: result)
+              update(rest1, (Symbol.comment + Symbol.space + Symbol.cartouche(txt)) :: result)
             case _ => update(rest, tok.source :: result)
           }
         case tok :: rest => update(rest, tok.source :: result)
diff -r f83c1842a559 -r e446505a4ec6 src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Jan 14 20:58:41 2018 +0100
+++ b/src/Pure/library.scala	Sun Jan 14 21:25:43 2018 +0100
@@ -148,12 +148,6 @@
   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 + "\""