src/Pure/Isar/outer_syntax.scala
changeset 50128 599c935aac82
parent 48885 d5fdaf7dd1f8
child 50428 7a78a74139f5
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Nov 19 20:47:13 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Nov 19 22:34:17 2012 +0100
     1.3 @@ -61,22 +61,29 @@
     1.4    def thy_load_commands: List[(String, List[String])] =
     1.5      (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
     1.6  
     1.7 -  def + (name: String, kind: (String, List[String]), replace: String): Outer_Syntax =
     1.8 +  def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
     1.9      new Outer_Syntax(
    1.10        keywords + (name -> kind),
    1.11        lexicon + name,
    1.12 -      if (Keyword.control(kind._1)) completion else completion + (name, replace))
    1.13 +      if (Keyword.control(kind._1) || replace == Some("")) completion
    1.14 +      else completion + (name, replace getOrElse name))
    1.15  
    1.16 -  def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, name)
    1.17 -  def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), name)
    1.18 -  def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    1.19 +  def + (name: String, kind: (String, List[String])): Outer_Syntax = this + (name, kind, Some(name))
    1.20 +  def + (name: String, kind: String): Outer_Syntax = this + (name, (kind, Nil), Some(name))
    1.21 +  def + (name: String, replace: Option[String]): Outer_Syntax =
    1.22 +    this + (name, (Keyword.MINOR, Nil), replace)
    1.23 +  def + (name: String): Outer_Syntax = this + (name, None)
    1.24  
    1.25    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.26      (this /: keywords) {
    1.27 -      case (syntax, ((name, Some((kind, _))))) =>
    1.28 -        syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
    1.29 -      case (syntax, ((name, None))) =>
    1.30 -        syntax + Symbol.decode(name) + Symbol.encode(name)
    1.31 +      case (syntax, ((name, Some((kind, _)), replace))) =>
    1.32 +        syntax +
    1.33 +          (Symbol.decode(name), kind, replace) +
    1.34 +          (Symbol.encode(name), kind, replace)
    1.35 +      case (syntax, ((name, None, replace))) =>
    1.36 +        syntax +
    1.37 +          (Symbol.decode(name), replace) +
    1.38 +          (Symbol.encode(name), replace)
    1.39      }
    1.40  
    1.41    def is_command(name: String): Boolean =