strictly sequential abbrevs;
authorwenzelm
Tue Sep 06 13:26:14 2016 +0200 (2016-09-06)
changeset 63808e8462a4349fc
parent 63807 5f77017055a3
child 63809 56670ab6f55e
strictly sequential abbrevs;
src/Pure/General/completion.scala
src/Pure/Pure.thy
     1.1 --- a/src/Pure/General/completion.scala	Mon Sep 05 23:39:15 2016 +0200
     1.2 +++ b/src/Pure/General/completion.scala	Tue Sep 06 13:26:14 2016 +0200
     1.3 @@ -402,23 +402,26 @@
     1.4    }
     1.5  
     1.6    def add_abbrevs(abbrevs: List[(String, String)]): Completion =
     1.7 -    if (abbrevs.isEmpty) this
     1.8 -    else {
     1.9 -      val words =
    1.10 -        for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
    1.11 -          yield (abbr, text)
    1.12 -      val abbrs =
    1.13 -        for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
    1.14 -          yield (abbr.reverse, (abbr, text))
    1.15 -      val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
    1.16 +    (this /: abbrevs)(_.add_abbrev(_))
    1.17 +
    1.18 +  private def add_abbrev(abbrev: (String, String)): Completion =
    1.19 +  {
    1.20 +    val (abbr, text) = abbrev
    1.21 +    val rev_abbr = abbr.reverse
    1.22 +    val is_word = Completion.Word_Parsers.is_word(abbr)
    1.23  
    1.24 -      new Completion(
    1.25 -        keywords,
    1.26 -        words_lex ++ words.map(_._1) -- remove,
    1.27 -        words_map ++ words -- remove,
    1.28 -        abbrevs_lex ++ abbrs.map(_._1) -- remove,
    1.29 -        abbrevs_map ++ abbrs -- remove)
    1.30 -    }
    1.31 +    val (words_lex1, words_map1) =
    1.32 +      if (!is_word) (words_lex, words_map)
    1.33 +      else if (text != "") (words_lex + abbr, words_map + abbrev)
    1.34 +      else (words_lex -- List(abbr), words_map - abbr)
    1.35 +
    1.36 +    val (abbrevs_lex1, abbrevs_map1) =
    1.37 +      if (is_word) (abbrevs_lex, abbrevs_map)
    1.38 +      else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
    1.39 +      else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
    1.40 +
    1.41 +    new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    1.42 +  }
    1.43  
    1.44    private def load(): Completion =
    1.45      add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
     2.1 --- a/src/Pure/Pure.thy	Mon Sep 05 23:39:15 2016 +0200
     2.2 +++ b/src/Pure/Pure.thy	Tue Sep 06 13:26:14 2016 +0200
     2.3 @@ -94,7 +94,9 @@
     2.4  abbrevs
     2.5    "default_sort" = ""
     2.6    "simproc_setup" = ""
     2.7 +  "hence" = ""
     2.8    "hence" = "then have"
     2.9 +  "thus" = ""
    2.10    "thus" = "then show"
    2.11    "apply_end" = ""
    2.12    "realizers" = ""