src/Pure/Isar/outer_syntax.scala
changeset 63579 73939a9b70a3
parent 63528 0f39f59317c1
child 63584 68751fe1c036
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 11:49:30 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 17:35:18 2016 +0200
     1.3 @@ -85,24 +85,35 @@
     1.4  
     1.5    /* add keywords */
     1.6  
     1.7 -  def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
     1.8 -    : Outer_Syntax =
     1.9 +  def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
    1.10    {
    1.11      val keywords1 = keywords + (name, kind, tags)
    1.12      val completion1 =
    1.13 -      if (replace == Some("")) completion
    1.14 -      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
    1.15 -        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
    1.16 -      else completion + (name, replace getOrElse name)
    1.17 +      completion.add_keyword(name).add_abbrevs(
    1.18 +        if (Keyword.theory_block.contains(kind))
    1.19 +          List((name, name + "\nbegin\n\u0007\nend"), (name, name))
    1.20 +        else List((name, name)))
    1.21      new Outer_Syntax(keywords1, completion1, language_context, true)
    1.22    }
    1.23  
    1.24    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.25      (this /: keywords) {
    1.26 -      case (syntax, (name, ((kind, tags), _), replace)) =>
    1.27 -        syntax +
    1.28 -          (Symbol.decode(name), kind, tags, replace) +
    1.29 -          (Symbol.encode(name), kind, tags, replace)
    1.30 +      case (syntax, (name, ((kind, tags), _))) =>
    1.31 +        syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    1.32 +    }
    1.33 +
    1.34 +  def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
    1.35 +    if (abbrevs.isEmpty) this
    1.36 +    else {
    1.37 +      val completion1 =
    1.38 +        completion.add_abbrevs(
    1.39 +          (for ((a, b) <- abbrevs) yield {
    1.40 +            val a1 = Symbol.decode(a)
    1.41 +            val a2 = Symbol.encode(a)
    1.42 +            val b1 = Symbol.decode(b)
    1.43 +            List((a1, b1), (a2, b1))
    1.44 +          }).flatten)
    1.45 +      new Outer_Syntax(keywords, completion1, language_context, has_tokens)
    1.46      }
    1.47  
    1.48