src/Pure/Isar/outer_syntax.scala
changeset 67004 af72fa58f71b
parent 66984 a1d3e5df0c95
child 67005 11fca474d87a
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Nov 04 15:24:40 2017 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Nov 04 17:11:21 2017 +0100
     1.3 @@ -16,8 +16,6 @@
     1.4  
     1.5    val empty: Outer_Syntax = new Outer_Syntax()
     1.6  
     1.7 -  lazy val init: Outer_Syntax = new Outer_Syntax(completion = Completion.init)
     1.8 -
     1.9    def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
    1.10  
    1.11  
    1.12 @@ -47,7 +45,6 @@
    1.13  
    1.14  final class Outer_Syntax private(
    1.15    val keywords: Keyword.Keywords = Keyword.Keywords.empty,
    1.16 -  val completion: Completion = Completion.empty,
    1.17    val rev_abbrevs: Thy_Header.Abbrevs = Nil,
    1.18    val language_context: Completion.Language_Context = Completion.Language_Context.outer,
    1.19    val has_tokens: Boolean = true)
    1.20 @@ -60,16 +57,8 @@
    1.21    /* keywords */
    1.22  
    1.23    def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
    1.24 -  {
    1.25 -    val keywords1 = keywords + (name, kind, exts)
    1.26 -    val completion1 =
    1.27 -      completion.add_keyword(name).
    1.28 -        add_abbrevs(
    1.29 -          (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    1.30 -           else Nil) :::
    1.31 -          (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
    1.32 -    new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
    1.33 -  }
    1.34 +    new Outer_Syntax(
    1.35 +      keywords + (name, kind, exts), rev_abbrevs, language_context, has_tokens = true)
    1.36  
    1.37    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.38      (this /: keywords) {
    1.39 @@ -87,17 +76,31 @@
    1.40    def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
    1.41      if (new_abbrevs.isEmpty) this
    1.42      else {
    1.43 -      val completion1 =
    1.44 -        completion.add_abbrevs(
    1.45 -          (for ((a, b) <- new_abbrevs) yield {
    1.46 +      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
    1.47 +      new Outer_Syntax(keywords, rev_abbrevs1, language_context, has_tokens)
    1.48 +    }
    1.49 +
    1.50 +
    1.51 +  /* completion */
    1.52 +
    1.53 +  lazy val completion: Completion =
    1.54 +  {
    1.55 +    val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList
    1.56 +    val completion_abbrevs =
    1.57 +      completion_keywords.flatMap(name =>
    1.58 +        (if (Keyword.theory_block.contains(keywords.kinds(name)))
    1.59 +          List((name, name + "\nbegin\n\u0007\nend"))
    1.60 +         else Nil) :::
    1.61 +        (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) :::
    1.62 +      abbrevs.flatMap(
    1.63 +        { case (a, b) =>
    1.64              val a1 = Symbol.decode(a)
    1.65              val a2 = Symbol.encode(a)
    1.66              val b1 = Symbol.decode(b)
    1.67              List((a1, b1), (a2, b1))
    1.68 -          }).flatten)
    1.69 -      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
    1.70 -      new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
    1.71 -    }
    1.72 +        })
    1.73 +    Completion.make(completion_keywords, completion_abbrevs)
    1.74 +  }
    1.75  
    1.76  
    1.77    /* build */
    1.78 @@ -110,11 +113,9 @@
    1.79      else if (this eq Outer_Syntax.empty) other
    1.80      else {
    1.81        val keywords1 = keywords ++ other.keywords
    1.82 -      val completion1 = completion ++ other.completion
    1.83        val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
    1.84 -      if ((keywords eq keywords1) && (completion eq completion1) && (rev_abbrevs eq rev_abbrevs1))
    1.85 -        this
    1.86 -      else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
    1.87 +      if ((keywords eq keywords1) && (rev_abbrevs eq rev_abbrevs1)) this
    1.88 +      else new Outer_Syntax(keywords1, rev_abbrevs1, language_context, has_tokens)
    1.89      }
    1.90  
    1.91  
    1.92 @@ -127,13 +128,12 @@
    1.93    /* language context */
    1.94  
    1.95    def set_language_context(context: Completion.Language_Context): Outer_Syntax =
    1.96 -    new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
    1.97 +    new Outer_Syntax(keywords, rev_abbrevs, context, has_tokens)
    1.98  
    1.99    def no_tokens: Outer_Syntax =
   1.100    {
   1.101      require(keywords.is_empty)
   1.102      new Outer_Syntax(
   1.103 -      completion = completion,
   1.104        rev_abbrevs = rev_abbrevs,
   1.105        language_context = language_context,
   1.106        has_tokens = false)