# HG changeset patch
# User wenzelm
# Date 1453546368 -3600
# Node ID 9bf0c9212f952d2239884d4b8e1e4517b1156d3b
# Parent  25f4a9cd8b682f6fa1b46a26ffbae38a26a2a69b
empty abbrevs are removed globally;

diff -r 25f4a9cd8b68 -r 9bf0c9212f95 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Jan 22 14:46:02 2016 +0100
+++ b/src/Pure/General/completion.scala	Sat Jan 23 11:52:48 2016 +0100
@@ -322,7 +322,9 @@
         if path.is_file
         entry <- Abbrevs_Parser.parse_file(path)
       } yield entry
-    symbol_abbrevs ::: more_abbrevs
+    val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet
+
+    (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
   }
 
   private val caret_indicator = '\u0007'