src/Pure/Isar/outer_syntax.scala
changeset 58907 0ee3563803c9
parent 58901 47809a811eba
child 58938 0c45680b7d9d
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 21:21:15 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 21:59:21 2014 +0100
     1.3 @@ -86,6 +86,8 @@
     1.4  
     1.5    /* add keywords */
     1.6  
     1.7 +  def + (name: String): Outer_Syntax = this + (name, None, None)
     1.8 +  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
     1.9    def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
    1.10      : Outer_Syntax =
    1.11    {
    1.12 @@ -99,8 +101,6 @@
    1.13        else completion + (name, replace getOrElse name)
    1.14      new Outer_Syntax(keywords1, completion1, language_context, true)
    1.15    }
    1.16 -  def + (name: String): Outer_Syntax = this + (name, None, None)
    1.17 -  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
    1.18  
    1.19    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.20      (this /: keywords) {