tuned;
authorwenzelm
Wed Nov 01 21:21:09 2017 +0100 (18 months ago)
changeset 669857382ff5b46b9
parent 66984 a1d3e5df0c95
child 66986 5188b1c59434
tuned;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Wed Nov 01 21:02:16 2017 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Wed Nov 01 21:21:09 2017 +0100
     1.3 @@ -356,12 +356,17 @@
     1.4      if (this eq other) this
     1.5      else if (is_empty) other
     1.6      else {
     1.7 -      val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
     1.8 +      val keywords1 =
     1.9 +        if (keywords eq other.keywords) keywords
    1.10 +        else if (keywords.isEmpty) other.keywords
    1.11 +        else (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
    1.12        val words_lex1 = words_lex ++ other.words_lex
    1.13        val words_map1 = words_map ++ other.words_map
    1.14        val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
    1.15        val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
    1.16 -      new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    1.17 +      if ((keywords eq keywords1) && (words_lex eq words_lex1) && (words_map eq words_map1) &&
    1.18 +        (abbrevs_lex eq abbrevs_lex1) && (abbrevs_map eq abbrevs_map1)) this
    1.19 +      else new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    1.20      }
    1.21  
    1.22