src/Pure/Isar/outer_syntax.scala
changeset 63867 fb46c031c841
parent 63865 ccac33e291b1
child 64616 dc3ec40fe41b
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Sep 14 12:51:40 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Sep 14 12:56:57 2016 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4  final class Outer_Syntax private(
     1.5    val keywords: Keyword.Keywords = Keyword.Keywords.empty,
     1.6    val completion: Completion = Completion.empty,
     1.7 +  val rev_abbrevs: Thy_Header.Abbrevs = Nil,
     1.8    val language_context: Completion.Language_Context = Completion.Language_Context.outer,
     1.9    val has_tokens: Boolean = true)
    1.10  {
    1.11 @@ -54,7 +55,7 @@
    1.12    override def toString: String = keywords.toString
    1.13  
    1.14  
    1.15 -  /* add keywords */
    1.16 +  /* keywords */
    1.17  
    1.18    def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
    1.19    {
    1.20 @@ -65,7 +66,7 @@
    1.21            (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    1.22             else Nil) :::
    1.23            (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
    1.24 -    new Outer_Syntax(keywords1, completion1, language_context, true)
    1.25 +    new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
    1.26    }
    1.27  
    1.28    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.29 @@ -74,18 +75,24 @@
    1.30          syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    1.31      }
    1.32  
    1.33 -  def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
    1.34 -    if (abbrevs.isEmpty) this
    1.35 +
    1.36 +  /* abbrevs */
    1.37 +
    1.38 +  def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
    1.39 +
    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) <- abbrevs) yield {
    1.46 +          (for ((a, b) <- new_abbrevs) yield {
    1.47              val a1 = Symbol.decode(a)
    1.48              val a2 = Symbol.encode(a)
    1.49              val b1 = Symbol.decode(b)
    1.50              List((a1, b1), (a2, b1))
    1.51            }).flatten)
    1.52 -      new Outer_Syntax(keywords, completion1, language_context, has_tokens)
    1.53 +      val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
    1.54 +      new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
    1.55      }
    1.56  
    1.57  
    1.58 @@ -96,8 +103,9 @@
    1.59      else {
    1.60        val keywords1 = keywords ++ other.keywords
    1.61        val completion1 = completion ++ other.completion
    1.62 +      val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
    1.63        if ((keywords eq keywords1) && (completion eq completion1)) this
    1.64 -      else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.65 +      else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
    1.66      }
    1.67  
    1.68  
    1.69 @@ -110,13 +118,14 @@
    1.70    /* language context */
    1.71  
    1.72    def set_language_context(context: Completion.Language_Context): Outer_Syntax =
    1.73 -    new Outer_Syntax(keywords, completion, context, has_tokens)
    1.74 +    new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
    1.75  
    1.76    def no_tokens: Outer_Syntax =
    1.77    {
    1.78      require(keywords.is_empty)
    1.79      new Outer_Syntax(
    1.80        completion = completion,
    1.81 +      rev_abbrevs = rev_abbrevs,
    1.82        language_context = language_context,
    1.83        has_tokens = false)
    1.84    }