# HG changeset patch
# User wenzelm
# Date 1509567669 -3600
# Node ID 7382ff5b46b931e899afd57d55efe174c7506dcc
# Parent  a1d3e5df0c95266b879256f7ab1165b40f52b87d
tuned;

diff -r a1d3e5df0c95 -r 7382ff5b46b9 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Nov 01 21:02:16 2017 +0100
+++ b/src/Pure/General/completion.scala	Wed Nov 01 21:21:09 2017 +0100
@@ -356,12 +356,17 @@
     if (this eq other) this
     else if (is_empty) other
     else {
-      val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
+      val keywords1 =
+        if (keywords eq other.keywords) keywords
+        else if (keywords.isEmpty) other.keywords
+        else (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
       val words_lex1 = words_lex ++ other.words_lex
       val words_map1 = words_map ++ other.words_map
       val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
       val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
-      new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+      if ((keywords eq keywords1) && (words_lex eq words_lex1) && (words_map eq words_map1) &&
+        (abbrevs_lex eq abbrevs_lex1) && (abbrevs_map eq abbrevs_map1)) this
+      else new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
     }