streamlined abstract datatype;
authorwenzelm
Thu Feb 23 19:58:49 2012 +0100 (2012-02-23)
changeset 46624dc4c72092088
parent 46623 bce24d3f29e7
child 46625 630542c79604
streamlined abstract datatype;
src/Pure/Isar/outer_syntax.scala
src/Pure/Thy/completion.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 19:35:05 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Feb 23 19:58:49 2012 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  {
     1.5    protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
     1.6    protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
     1.7 -  lazy val completion: Completion = (new Completion).add_symbols // FIXME odd initialization
     1.8 +  lazy val completion: Completion = Completion.init()  // FIXME odd initialization
     1.9  
    1.10    def keyword_kind(name: String): Option[String] = keywords.get(name)
    1.11  
     2.1 --- a/src/Pure/Thy/completion.scala	Thu Feb 23 19:35:05 2012 +0100
     2.2 +++ b/src/Pure/Thy/completion.scala	Thu Feb 23 19:58:49 2012 +0100
     2.3 @@ -10,14 +10,20 @@
     2.4  import scala.util.parsing.combinator.RegexParsers
     2.5  
     2.6  
     2.7 -private object Completion
     2.8 +object Completion
     2.9  {
    2.10 +  val empty: Completion =
    2.11 +    new Completion(Scan.Lexicon(), Map.empty, Scan.Lexicon(), Map.empty)
    2.12 +
    2.13 +  def init(): Completion = empty.add_symbols()
    2.14 +
    2.15 +
    2.16    /** word completion **/
    2.17  
    2.18 -  val word_regex = "[a-zA-Z0-9_']+".r
    2.19 -  def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    2.20 +  private val word_regex = "[a-zA-Z0-9_']+".r
    2.21 +  private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    2.22  
    2.23 -  object Parse extends RegexParsers
    2.24 +  private object Parse extends RegexParsers
    2.25    {
    2.26      override val whiteSpace = "".r
    2.27  
    2.28 @@ -36,33 +42,24 @@
    2.29    }
    2.30  }
    2.31  
    2.32 -class Completion
    2.33 +class Completion private(
    2.34 +  words_lex: Scan.Lexicon,
    2.35 +  words_map: Map[String, String],
    2.36 +  abbrevs_lex: Scan.Lexicon,
    2.37 +  abbrevs_map: Map[String, (String, String)])
    2.38  {
    2.39 -  /* representation */
    2.40 -
    2.41 -  protected val words_lex = Scan.Lexicon()
    2.42 -  protected val words_map = Map[String, String]()
    2.43 -
    2.44 -  protected val abbrevs_lex = Scan.Lexicon()
    2.45 -  protected val abbrevs_map = Map[String, (String, String)]()
    2.46 -
    2.47 -
    2.48    /* adding stuff */
    2.49  
    2.50    def + (keyword: String, replace: String): Completion =
    2.51 -  {
    2.52 -    val old = this
    2.53 -    new Completion {
    2.54 -      override val words_lex = old.words_lex + keyword
    2.55 -      override val words_map = old.words_map + (keyword -> replace)
    2.56 -      override val abbrevs_lex = old.abbrevs_lex
    2.57 -      override val abbrevs_map = old.abbrevs_map
    2.58 -    }
    2.59 -  }
    2.60 +    new Completion(
    2.61 +      words_lex + keyword,
    2.62 +      words_map + (keyword -> replace),
    2.63 +      abbrevs_lex,
    2.64 +      abbrevs_map)
    2.65  
    2.66    def + (keyword: String): Completion = this + (keyword, keyword)
    2.67  
    2.68 -  def add_symbols: Completion =
    2.69 +  private def add_symbols(): Completion =
    2.70    {
    2.71      val words =
    2.72        (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
    2.73 @@ -73,13 +70,11 @@
    2.74        (for ((x, y) <- Symbol.abbrevs if !Completion.is_word(y))
    2.75          yield (y.reverse.toString, (y, x))).toList
    2.76  
    2.77 -    val old = this
    2.78 -    new Completion {
    2.79 -      override val words_lex = old.words_lex ++ words.map(_._1)
    2.80 -      override val words_map = old.words_map ++ words
    2.81 -      override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
    2.82 -      override val abbrevs_map = old.abbrevs_map ++ abbrs
    2.83 -    }
    2.84 +    new Completion(
    2.85 +      words_lex ++ words.map(_._1),
    2.86 +      words_map ++ words,
    2.87 +      abbrevs_lex ++ abbrs.map(_._1),
    2.88 +      abbrevs_map ++ abbrs)
    2.89    }
    2.90  
    2.91