src/Pure/General/completion.scala
changeset 67004 af72fa58f71b
parent 66985 7382ff5b46b9
child 67311 3869b2400e22
     1.1 --- a/src/Pure/General/completion.scala	Sat Nov 04 15:24:40 2017 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sat Nov 04 17:11:21 2017 +0100
     1.3 @@ -253,12 +253,13 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* init */
     1.8 +  /* make */
     1.9  
    1.10    val empty: Completion = new Completion()
    1.11  
    1.12 -  lazy val init: Completion =
    1.13 -    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
    1.14 +  def make(keywords: List[String], abbrevs: List[(String, String)]): Completion =
    1.15 +    empty.add_symbols.add_keywords(keywords).add_abbrevs(
    1.16 +      Completion.symbol_abbrevs ::: Completion.default_abbrevs ::: abbrevs)
    1.17  
    1.18  
    1.19    /* word parsers */
    1.20 @@ -337,39 +338,12 @@
    1.21  }
    1.22  
    1.23  final class Completion private(
    1.24 -  protected val keywords: Set[String] = Set.empty,
    1.25 -  protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.26 -  protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.27 -  protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.28 -  protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
    1.29 +  keywords: Set[String] = Set.empty,
    1.30 +  words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.31 +  words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.32 +  abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.33 +  abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
    1.34  {
    1.35 -  /* merge */
    1.36 -
    1.37 -  def is_empty: Boolean =
    1.38 -    keywords.isEmpty &&
    1.39 -    words_lex.is_empty &&
    1.40 -    words_map.isEmpty &&
    1.41 -    abbrevs_lex.is_empty &&
    1.42 -    abbrevs_map.isEmpty
    1.43 -
    1.44 -  def ++ (other: Completion): Completion =
    1.45 -    if (this eq other) this
    1.46 -    else if (is_empty) other
    1.47 -    else {
    1.48 -      val keywords1 =
    1.49 -        if (keywords eq other.keywords) keywords
    1.50 -        else if (keywords.isEmpty) other.keywords
    1.51 -        else (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
    1.52 -      val words_lex1 = words_lex ++ other.words_lex
    1.53 -      val words_map1 = words_map ++ other.words_map
    1.54 -      val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
    1.55 -      val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
    1.56 -      if ((keywords eq keywords1) && (words_lex eq words_lex1) && (words_map eq words_map1) &&
    1.57 -        (abbrevs_lex eq abbrevs_lex1) && (abbrevs_map eq abbrevs_map1)) this
    1.58 -      else new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    1.59 -    }
    1.60 -
    1.61 -
    1.62    /* keywords */
    1.63  
    1.64    private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
    1.65 @@ -380,6 +354,13 @@
    1.66    def add_keyword(keyword: String): Completion =
    1.67      new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
    1.68  
    1.69 +  def add_keywords(names: List[String]): Completion =
    1.70 +  {
    1.71 +    val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k }
    1.72 +    if (keywords eq keywords1) this
    1.73 +    else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map)
    1.74 +  }
    1.75 +
    1.76  
    1.77    /* symbols and abbrevs */
    1.78