clarified representation of type Keywords;
authorwenzelm
Wed Nov 05 17:37:25 2014 +0100 (2014-11-05)
changeset 5890147809a811eba
parent 58900 1435cc20b022
child 58902 938bbacda12d
clarified representation of type Keywords;
tuned signature;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/structure_matching.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Wed Nov 05 16:57:12 2014 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Wed Nov 05 17:37:25 2014 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4  
     1.5    /* kinds */
     1.6  
     1.7 -  val MINOR = "minor"
     1.8    val DIAG = "diag"
     1.9    val HEADING = "heading"
    1.10    val THY_BEGIN = "thy_begin"
    1.11 @@ -74,55 +73,59 @@
    1.12    {
    1.13      def empty: Keywords = new Keywords()
    1.14  
    1.15 -    def apply(names: List[String]): Keywords =
    1.16 -      (empty /: names)({ case (keywords, a) => keywords + (a, (MINOR, Nil)) })
    1.17 +    def apply(keywords: List[String]): Keywords = (empty /: keywords)(_ + _)
    1.18    }
    1.19  
    1.20    class Keywords private(
    1.21 -    keywords: Map[String, (String, List[String])] = Map.empty,
    1.22      val minor: Scan.Lexicon = Scan.Lexicon.empty,
    1.23 -    val major: Scan.Lexicon = Scan.Lexicon.empty)
    1.24 +    val major: Scan.Lexicon = Scan.Lexicon.empty,
    1.25 +    command_kinds: Map[String, (String, List[String])] = Map.empty)
    1.26    {
    1.27      /* content */
    1.28  
    1.29 -    override def toString: String =
    1.30 -      (for ((name, (kind, files)) <- keywords) yield {
    1.31 -        if (kind == MINOR) quote(name)
    1.32 -        else
    1.33 -          quote(name) + " :: " + quote(kind) +
    1.34 -          (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
    1.35 -      }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
    1.36 +    def is_empty: Boolean = minor.isEmpty && major.isEmpty
    1.37  
    1.38 -    def is_empty: Boolean = keywords.isEmpty
    1.39 +    def + (name: String): Keywords =
    1.40 +      new Keywords(minor + name, major, command_kinds)
    1.41  
    1.42      def + (name: String, kind: (String, List[String])): Keywords =
    1.43      {
    1.44 -      val keywords1 = keywords + (name -> kind)
    1.45 -      val (minor1, major1) =
    1.46 -        if (kind._1 == MINOR) (minor + name, major) else (minor, major + name)
    1.47 -      new Keywords(keywords1, minor1, major1)
    1.48 +      val major1 = major + name
    1.49 +      val command_kinds1 = command_kinds + (name -> kind)
    1.50 +      new Keywords(minor, major1, command_kinds1)
    1.51 +    }
    1.52 +
    1.53 +    override def toString: String =
    1.54 +    {
    1.55 +      val keywords = minor.iterator.map(quote(_)).toList
    1.56 +      val commands =
    1.57 +        for ((name, (kind, files)) <- command_kinds.toList.sortBy(_._1)) yield {
    1.58 +          quote(name) + " :: " + quote(kind) +
    1.59 +          (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
    1.60 +        }
    1.61 +      (keywords ::: commands).mkString("keywords\n  ", " and\n  ", "")
    1.62      }
    1.63  
    1.64  
    1.65 -    /* kind */
    1.66 +    /* command kind */
    1.67  
    1.68 -    def kind(name: String): Option[String] = keywords.get(name).map(_._1)
    1.69 +    def command_kind(name: String): Option[String] = command_kinds.get(name).map(_._1)
    1.70  
    1.71 -    def command_kind(token: Token, pred: String => Boolean): Boolean =
    1.72 +    def is_command_kind(token: Token, pred: String => Boolean): Boolean =
    1.73        token.is_command &&
    1.74 -        (kind(token.source) match { case Some(k) => k != MINOR && pred(k) case None => false })
    1.75 +        (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
    1.76  
    1.77  
    1.78      /* load commands */
    1.79  
    1.80      def load_command(name: String): Option[List[String]] =
    1.81 -      keywords.get(name) match {
    1.82 +      command_kinds.get(name) match {
    1.83          case Some((THY_LOAD, exts)) => Some(exts)
    1.84          case _ => None
    1.85        }
    1.86  
    1.87      private lazy val load_commands: List[(String, List[String])] =
    1.88 -      (for ((name, (THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
    1.89 +      (for ((name, (THY_LOAD, files)) <- command_kinds.iterator) yield (name, files)).toList
    1.90  
    1.91      def load_commands_in(text: String): Boolean =
    1.92        load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 16:57:12 2014 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 05 17:37:25 2014 +0100
     2.3 @@ -86,33 +86,29 @@
     2.4  
     2.5    /* add keywords */
     2.6  
     2.7 -  def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
     2.8 +  def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
     2.9 +    : Outer_Syntax =
    2.10    {
    2.11 -    val keywords1 = keywords + (name, kind)
    2.12 +    val keywords1 =
    2.13 +      opt_kind match {
    2.14 +        case None => keywords + name
    2.15 +        case Some(kind) => keywords + (name, kind)
    2.16 +      }
    2.17      val completion1 =
    2.18        if (replace == Some("")) completion
    2.19        else completion + (name, replace getOrElse name)
    2.20      new Outer_Syntax(keywords1, completion1, language_context, true)
    2.21    }
    2.22 -
    2.23 -  def + (name: String, kind: (String, List[String])): Outer_Syntax =
    2.24 -    this + (name, kind, Some(name))
    2.25 -  def + (name: String, kind: String): Outer_Syntax =
    2.26 -    this + (name, (kind, Nil), Some(name))
    2.27 -  def + (name: String, replace: Option[String]): Outer_Syntax =
    2.28 -    this + (name, (Keyword.MINOR, Nil), replace)
    2.29 -  def + (name: String): Outer_Syntax = this + (name, None)
    2.30 +  def + (name: String): Outer_Syntax = this + (name, None, None)
    2.31 +  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
    2.32  
    2.33    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    2.34      (this /: keywords) {
    2.35 -      case (syntax, (name, Some((kind, _)), replace)) =>
    2.36 +      case (syntax, (name, opt_spec, replace)) =>
    2.37 +        val opt_kind = opt_spec.map(_._1)
    2.38          syntax +
    2.39 -          (Symbol.decode(name), kind, replace) +
    2.40 -          (Symbol.encode(name), kind, replace)
    2.41 -      case (syntax, (name, None, replace)) =>
    2.42 -        syntax +
    2.43 -          (Symbol.decode(name), replace) +
    2.44 -          (Symbol.encode(name), replace)
    2.45 +          (Symbol.decode(name), opt_kind, replace) +
    2.46 +          (Symbol.encode(name), opt_kind, replace)
    2.47      }
    2.48  
    2.49  
    2.50 @@ -149,7 +145,7 @@
    2.51      val command1 = tokens.exists(_.is_command)
    2.52  
    2.53      val depth1 =
    2.54 -      if (tokens.exists(tok => keywords.command_kind(tok, Keyword.theory))) 0
    2.55 +      if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
    2.56        else if (command1) struct.after_span_depth
    2.57        else struct.span_depth
    2.58  
    2.59 @@ -157,15 +153,15 @@
    2.60        ((struct.span_depth, struct.after_span_depth) /: tokens) {
    2.61          case ((x, y), tok) =>
    2.62            if (tok.is_command) {
    2.63 -            if (keywords.command_kind(tok, Keyword.theory_goal))
    2.64 +            if (keywords.is_command_kind(tok, Keyword.theory_goal))
    2.65                (2, 1)
    2.66 -            else if (keywords.command_kind(tok, Keyword.theory))
    2.67 +            else if (keywords.is_command_kind(tok, Keyword.theory))
    2.68                (1, 0)
    2.69 -            else if (keywords.command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
    2.70 +            else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
    2.71                (y + 2, y + 1)
    2.72 -            else if (keywords.command_kind(tok, Keyword.qed) || tok.is_end_block)
    2.73 +            else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
    2.74                (y + 1, y - 1)
    2.75 -            else if (keywords.command_kind(tok, Keyword.qed_global))
    2.76 +            else if (keywords.is_command_kind(tok, Keyword.qed_global))
    2.77                (1, 0)
    2.78              else (x, y)
    2.79            }
    2.80 @@ -254,7 +250,7 @@
    2.81        case "subsection" => Some(2)
    2.82        case "subsubsection" => Some(3)
    2.83        case _ =>
    2.84 -        keywords.kind(command.name) match {
    2.85 +        keywords.command_kind(command.name) match {
    2.86            case Some(kind) if Keyword.theory(kind) => Some(4)
    2.87            case _ => None
    2.88          }
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Nov 05 16:57:12 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Nov 05 17:37:25 2014 +0100
     3.3 @@ -85,7 +85,7 @@
     3.4    }
     3.5  
     3.6    def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     3.7 -    if (token.is_command) command_style(syntax.keywords.kind(token.content).getOrElse(""))
     3.8 +    if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
     3.9      else if (token.is_delimiter) JEditToken.OPERATOR
    3.10      else token_style(token.kind)
    3.11  
     4.1 --- a/src/Tools/jEdit/src/structure_matching.scala	Wed Nov 05 16:57:12 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/structure_matching.scala	Wed Nov 05 17:37:25 2014 +0100
     4.3 @@ -44,8 +44,8 @@
     4.4          case Some(syntax) =>
     4.5            val limit = PIDE.options.value.int("jedit_structure_limit") max 0
     4.6  
     4.7 -          def command_kind(token: Token, pred: String => Boolean): Boolean =
     4.8 -            syntax.keywords.command_kind(token, pred)
     4.9 +          def is_command_kind(token: Token, pred: String => Boolean): Boolean =
    4.10 +            syntax.keywords.is_command_kind(token, pred)
    4.11  
    4.12            def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    4.13              Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
    4.14 @@ -63,45 +63,45 @@
    4.15  
    4.16            iterator(caret_line, 1).find(info => info.range.touches(caret))
    4.17            match {
    4.18 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.theory_goal) =>
    4.19 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
    4.20                find_block(
    4.21 -                command_kind(_, Keyword.proof_goal),
    4.22 -                command_kind(_, Keyword.qed),
    4.23 -                command_kind(_, Keyword.qed_global),
    4.24 +                is_command_kind(_, Keyword.proof_goal),
    4.25 +                is_command_kind(_, Keyword.qed),
    4.26 +                is_command_kind(_, Keyword.qed_global),
    4.27                  t =>
    4.28 -                  command_kind(t, Keyword.diag) ||
    4.29 -                  command_kind(t, Keyword.proof),
    4.30 +                  is_command_kind(t, Keyword.diag) ||
    4.31 +                  is_command_kind(t, Keyword.proof),
    4.32                  caret_iterator())
    4.33  
    4.34 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.proof_goal) =>
    4.35 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
    4.36                find_block(
    4.37 -                command_kind(_, Keyword.proof_goal),
    4.38 -                command_kind(_, Keyword.qed),
    4.39 +                is_command_kind(_, Keyword.proof_goal),
    4.40 +                is_command_kind(_, Keyword.qed),
    4.41                  _ => false,
    4.42                  t =>
    4.43 -                  command_kind(t, Keyword.diag) ||
    4.44 -                  command_kind(t, Keyword.proof),
    4.45 +                  is_command_kind(t, Keyword.diag) ||
    4.46 +                  is_command_kind(t, Keyword.proof),
    4.47                  caret_iterator())
    4.48  
    4.49 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed_global) =>
    4.50 -              rev_caret_iterator().find(info => command_kind(info.info, Keyword.theory))
    4.51 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) =>
    4.52 +              rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory))
    4.53                match {
    4.54                  case Some(Text.Info(range2, tok))
    4.55 -                if command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
    4.56 +                if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
    4.57                  case _ => None
    4.58                }
    4.59  
    4.60 -            case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed) =>
    4.61 +            case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
    4.62                find_block(
    4.63 -                command_kind(_, Keyword.qed),
    4.64 +                is_command_kind(_, Keyword.qed),
    4.65                  t =>
    4.66 -                  command_kind(t, Keyword.proof_goal) ||
    4.67 -                  command_kind(t, Keyword.theory_goal),
    4.68 +                  is_command_kind(t, Keyword.proof_goal) ||
    4.69 +                  is_command_kind(t, Keyword.theory_goal),
    4.70                  _ => false,
    4.71                  t =>
    4.72 -                  command_kind(t, Keyword.diag) ||
    4.73 -                  command_kind(t, Keyword.proof) ||
    4.74 -                  command_kind(t, Keyword.theory_goal),
    4.75 +                  is_command_kind(t, Keyword.diag) ||
    4.76 +                  is_command_kind(t, Keyword.proof) ||
    4.77 +                  is_command_kind(t, Keyword.theory_goal),
    4.78                  rev_caret_iterator())
    4.79  
    4.80              case Some(Text.Info(range1, tok)) if tok.is_begin =>
    4.81 @@ -117,7 +117,7 @@
    4.82                      find(info => info.info.is_command || info.info.is_begin)
    4.83                    match {
    4.84                      case Some(Text.Info(range3, tok)) =>
    4.85 -                      if (command_kind(tok, Keyword.theory_block)) Some((range1, range3))
    4.86 +                      if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
    4.87                        else Some((range1, range2))
    4.88                      case None => None
    4.89                    }