src/Pure/Isar/outer_syntax.scala
changeset 58901 47809a811eba
parent 58900 1435cc20b022
child 58907 0ee3563803c9
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 16:57:12 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 17:37:25 2014 +0100
     1.3 @@ -86,33 +86,29 @@
     1.4  
     1.5    /* add keywords */
     1.6  
     1.7 -  def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
     1.8 +  def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
     1.9 +    : Outer_Syntax =
    1.10    {
    1.11 -    val keywords1 = keywords + (name, kind)
    1.12 +    val keywords1 =
    1.13 +      opt_kind match {
    1.14 +        case None => keywords + name
    1.15 +        case Some(kind) => keywords + (name, kind)
    1.16 +      }
    1.17      val completion1 =
    1.18        if (replace == Some("")) completion
    1.19        else completion + (name, replace getOrElse name)
    1.20      new Outer_Syntax(keywords1, completion1, language_context, true)
    1.21    }
    1.22 -
    1.23 -  def + (name: String, kind: (String, List[String])): Outer_Syntax =
    1.24 -    this + (name, kind, Some(name))
    1.25 -  def + (name: String, kind: String): Outer_Syntax =
    1.26 -    this + (name, (kind, Nil), Some(name))
    1.27 -  def + (name: String, replace: Option[String]): Outer_Syntax =
    1.28 -    this + (name, (Keyword.MINOR, Nil), replace)
    1.29 -  def + (name: String): Outer_Syntax = this + (name, None)
    1.30 +  def + (name: String): Outer_Syntax = this + (name, None, None)
    1.31 +  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
    1.32  
    1.33    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.34      (this /: keywords) {
    1.35 -      case (syntax, (name, Some((kind, _)), replace)) =>
    1.36 +      case (syntax, (name, opt_spec, replace)) =>
    1.37 +        val opt_kind = opt_spec.map(_._1)
    1.38          syntax +
    1.39 -          (Symbol.decode(name), kind, replace) +
    1.40 -          (Symbol.encode(name), kind, replace)
    1.41 -      case (syntax, (name, None, replace)) =>
    1.42 -        syntax +
    1.43 -          (Symbol.decode(name), replace) +
    1.44 -          (Symbol.encode(name), replace)
    1.45 +          (Symbol.decode(name), opt_kind, replace) +
    1.46 +          (Symbol.encode(name), opt_kind, replace)
    1.47      }
    1.48  
    1.49  
    1.50 @@ -149,7 +145,7 @@
    1.51      val command1 = tokens.exists(_.is_command)
    1.52  
    1.53      val depth1 =
    1.54 -      if (tokens.exists(tok => keywords.command_kind(tok, Keyword.theory))) 0
    1.55 +      if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
    1.56        else if (command1) struct.after_span_depth
    1.57        else struct.span_depth
    1.58  
    1.59 @@ -157,15 +153,15 @@
    1.60        ((struct.span_depth, struct.after_span_depth) /: tokens) {
    1.61          case ((x, y), tok) =>
    1.62            if (tok.is_command) {
    1.63 -            if (keywords.command_kind(tok, Keyword.theory_goal))
    1.64 +            if (keywords.is_command_kind(tok, Keyword.theory_goal))
    1.65                (2, 1)
    1.66 -            else if (keywords.command_kind(tok, Keyword.theory))
    1.67 +            else if (keywords.is_command_kind(tok, Keyword.theory))
    1.68                (1, 0)
    1.69 -            else if (keywords.command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
    1.70 +            else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
    1.71                (y + 2, y + 1)
    1.72 -            else if (keywords.command_kind(tok, Keyword.qed) || tok.is_end_block)
    1.73 +            else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
    1.74                (y + 1, y - 1)
    1.75 -            else if (keywords.command_kind(tok, Keyword.qed_global))
    1.76 +            else if (keywords.is_command_kind(tok, Keyword.qed_global))
    1.77                (1, 0)
    1.78              else (x, y)
    1.79            }
    1.80 @@ -254,7 +250,7 @@
    1.81        case "subsection" => Some(2)
    1.82        case "subsubsection" => Some(3)
    1.83        case _ =>
    1.84 -        keywords.kind(command.name) match {
    1.85 +        keywords.command_kind(command.name) match {
    1.86            case Some(kind) if Keyword.theory(kind) => Some(4)
    1.87            case _ => None
    1.88          }