strictly sequential abbrevs;

--- a/src/Pure/General/completion.scala	Mon Sep 05 23:39:15 2016 +0200
+++ b/src/Pure/General/completion.scala	Tue Sep 06 13:26:14 2016 +0200
@@ -402,23 +402,26 @@
   }
 
   def add_abbrevs(abbrevs: List[(String, String)]): Completion =
-    if (abbrevs.isEmpty) this
-    else {
-      val words =
-        for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
-          yield (abbr, text)
-      val abbrs =
-        for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
-          yield (abbr.reverse, (abbr, text))
-      val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
+    (this /: abbrevs)(_.add_abbrev(_))
+
+  private def add_abbrev(abbrev: (String, String)): Completion =
+  {
+    val (abbr, text) = abbrev
+    val rev_abbr = abbr.reverse
+    val is_word = Completion.Word_Parsers.is_word(abbr)
 
-      new Completion(
-        keywords,
-        words_lex ++ words.map(_._1) -- remove,
-        words_map ++ words -- remove,
-        abbrevs_lex ++ abbrs.map(_._1) -- remove,
-        abbrevs_map ++ abbrs -- remove)
-    }
+    val (words_lex1, words_map1) =
+      if (!is_word) (words_lex, words_map)
+      else if (text != "") (words_lex + abbr, words_map + abbrev)
+      else (words_lex -- List(abbr), words_map - abbr)
+
+    val (abbrevs_lex1, abbrevs_map1) =
+      if (is_word) (abbrevs_lex, abbrevs_map)
+      else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
+      else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
+
+    new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+  }
 
   private def load(): Completion =
     add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)

--- a/src/Pure/Pure.thy	Mon Sep 05 23:39:15 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Sep 06 13:26:14 2016 +0200
@@ -94,7 +94,9 @@
 abbrevs
   "default_sort" = ""
   "simproc_setup" = ""
+  "hence" = ""
   "hence" = "then have"
+  "thus" = ""
   "thus" = "then show"
   "apply_end" = ""
   "realizers" = ""