diff -r 9ac666f343d4 -r 94c55cc73747 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sun Apr 13 19:55:16 2014 +0200
+++ b/src/Pure/General/completion.scala	Sun Apr 13 21:43:25 2014 +0200
@@ -91,7 +91,8 @@
     def + (entry: (String, Int)): History =
     {
       val (name, freq) = entry
-      new History(rep + (name -> (frequency(name) + freq)))
+      if (name == "") this
+      else new History(rep + (name -> (frequency(name) + freq)))
     }
 
     def ordering: Ordering[Item] =