src/Pure/Isar/outer_syntax.scala
changeset 65383 089f2edefb77
parent 64616 dc3ec40fe41b
child 65384 36255c43c64c
equal deleted inserted replaced
65382:de848ac5e0d7 65383:089f2edefb77
    55   override def toString: String = keywords.toString
    55   override def toString: String = keywords.toString
    56 
    56 
    57 
    57 
    58   /* keywords */
    58   /* keywords */
    59 
    59 
    60   def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
    60   def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
    61   {
    61   {
    62     val keywords1 = keywords + (name, kind, tags)
    62     val keywords1 = keywords + (name, kind, exts)
    63     val completion1 =
    63     val completion1 =
    64       completion.add_keyword(name).
    64       completion.add_keyword(name).
    65         add_abbrevs(
    65         add_abbrevs(
    66           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    66           (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
    67            else Nil) :::
    67            else Nil) :::
    69     new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
    69     new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
    70   }
    70   }
    71 
    71 
    72   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    72   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    73     (this /: keywords) {
    73     (this /: keywords) {
    74       case (syntax, (name, ((kind, tags), _))) =>
    74       case (syntax, (name, ((kind, exts), _))) =>
    75         syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    75         syntax + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
    76     }
    76     }
    77 
    77 
    78 
    78 
    79   /* abbrevs */
    79   /* abbrevs */
    80 
    80