# HG changeset patch
# User wenzelm
# Date 1473855373 -7200
# Node ID 856d2f74c303e11b1784457e57ebae37f97ca2c5
# Parent  22037a819276f9f3ab22e716cffde614e7f723b2
tuned;

diff -r 22037a819276 -r 856d2f74c303 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Sep 14 14:07:09 2016 +0200
+++ b/src/Pure/General/completion.scala	Wed Sep 14 14:16:13 2016 +0200
@@ -329,7 +329,13 @@
     (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
   }
 
-  private val caret_indicator = '\u0007'
+  val caret_indicator = '\u0007'
+  def split_template(s: String): (String, String) =
+    space_explode(caret_indicator, s) match {
+      case List(s1, s2) => (s1, s2)
+      case _ => (s, "")
+    }
+
   private val antiquote = "@{"
 
   private val default_abbrevs =
@@ -505,11 +511,7 @@
             (complete_word, name0) <- completions
             name1 = decode(name0)
             if name1 != original
-            (s1, s2) =
-              space_explode(Completion.caret_indicator, name1) match {
-                case List(s1, s2) => (s1, s2)
-                case _ => (name1, "")
-              }
+            (s1, s2) = Completion.split_template(name1)
             move = - s2.length
             description =
               if (is_symbol(name0)) {