# HG changeset patch
# User wenzelm
# Date 1470131370 -7200
# Node ID e8990d0e3965986bcfe331923a606e3b2a12b48f
# Parent  ba972a7dbeba4c150c64d9f14988ffd57c227e30
tuned;

diff -r ba972a7dbeba -r e8990d0e3965 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Aug 01 22:36:47 2016 +0200
+++ b/src/Pure/General/completion.scala	Tue Aug 02 11:49:30 2016 +0200
@@ -330,7 +330,7 @@
   private val caret_indicator = '\u0007'
   private val antiquote = "@{"
 
-  private val default_abbrs =
+  private val default_abbrevs =
     List("@{" -> "@{\u0007}",
       "`" -> "\\<close>",
       "`" -> "\\<open>",
@@ -340,7 +340,7 @@
       "\"" -> "\\<open>\u0007\\<close>")
 
   private def default_frequency(name: String): Option[Int] =
-    default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
+    default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
 }
 
 final class Completion private(
@@ -391,23 +391,29 @@
   def + (keyword: String): Completion = this + (keyword, keyword)
 
 
-  /* load symbols and abbrevs */
+  /* symbols and abbrevs */
 
-  private def load(): Completion =
+  def add_symbols(): Completion =
   {
-    val abbrevs = Completion.load_abbrevs()
-
     val words =
       (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
-      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
-      (for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text))
+      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
 
-    val non_word_abbrs =
-      (for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
-        yield (abbr, text)).toList
+    new Completion(
+      keywords,
+      words_lex ++ words.map(_._1),
+      words_map ++ words,
+      abbrevs_lex,
+      abbrevs_map)
+  }
 
+  def add_abbrevs(abbrevs: List[(String, String)]): Completion =
+  {
+    val words =
+      for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr))
+        yield (abbr, text)
     val abbrs =
-      for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs)
+      for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
         yield (abbr.reverse, (abbr, text))
 
     new Completion(
@@ -418,6 +424,9 @@
       abbrevs_map ++ abbrs)
   }
 
+  private def load(): Completion =
+    add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
+
 
   /* complete */
 
@@ -444,7 +453,7 @@
             case (abbr, _) :: _ =>
               val ok =
                 if (abbr == Completion.antiquote) language_context.antiquotes
-                else language_context.symbols || Completion.default_abbrs.exists(_._1 == abbr)
+                else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr)
               if (ok) Some((abbr, abbrevs))
               else None
           }