explicit kind "before_command";
authorwenzelm
Mon Jul 11 16:36:29 2016 +0200 (2016-07-11)
changeset 634414c3fa4dba79f
parent 63440 2ce032a41a3a
child 63442 f6b5124b7023
explicit kind "before_command";
tuned signature;
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
src/Pure/Pure.thy
src/Pure/System/options.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/Isar/keyword.ML	Mon Jul 11 14:25:06 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Mon Jul 11 16:36:29 2016 +0200
     1.3 @@ -32,9 +32,11 @@
     1.4    val prf_script: string
     1.5    val prf_script_goal: string
     1.6    val prf_script_asm_goal: string
     1.7 +  val before_command: string
     1.8    val quasi_command: string
     1.9    type spec = (string * string list) * string list
    1.10    val no_spec: spec
    1.11 +  val before_command_spec: spec
    1.12    val quasi_command_spec: spec
    1.13    type keywords
    1.14    val minor_keywords: keywords -> Scan.lexicon
    1.15 @@ -107,6 +109,8 @@
    1.16  val prf_script = "prf_script";
    1.17  val prf_script_goal = "prf_script_goal";
    1.18  val prf_script_asm_goal = "prf_script_asm_goal";
    1.19 +
    1.20 +val before_command = "before_command";
    1.21  val quasi_command = "quasi_command";
    1.22  
    1.23  val command_kinds =
    1.24 @@ -121,6 +125,7 @@
    1.25  type spec = (string * string list) * string list;
    1.26  
    1.27  val no_spec: spec = (("", []), []);
    1.28 +val before_command_spec: spec = ((before_command, []), []);
    1.29  val quasi_command_spec: spec = ((quasi_command, []), []);
    1.30  
    1.31  type entry =
    1.32 @@ -175,7 +180,7 @@
    1.33  
    1.34  val add_keywords =
    1.35    fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
    1.36 -    if kind = "" orelse kind = quasi_command then
    1.37 +    if kind = "" orelse kind = before_command orelse kind = quasi_command then
    1.38        let
    1.39          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
    1.40        in (minor', major, commands) end
     2.1 --- a/src/Pure/Isar/keyword.scala	Mon Jul 11 14:25:06 2016 +0200
     2.2 +++ b/src/Pure/Isar/keyword.scala	Mon Jul 11 16:36:29 2016 +0200
     2.3 @@ -39,6 +39,8 @@
     2.4    val PRF_SCRIPT = "prf_script"
     2.5    val PRF_SCRIPT_GOAL = "prf_script_goal"
     2.6    val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
     2.7 +
     2.8 +  val BEFORE_COMMAND = "before_command"
     2.9    val QUASI_COMMAND = "quasi_command"
    2.10  
    2.11  
    2.12 @@ -90,6 +92,7 @@
    2.13    type Spec = ((String, List[String]), List[String])
    2.14  
    2.15    val no_spec: Spec = (("", Nil), Nil)
    2.16 +  val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
    2.17    val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
    2.18  
    2.19    object Keywords
    2.20 @@ -100,22 +103,20 @@
    2.21    class Keywords private(
    2.22      val minor: Scan.Lexicon = Scan.Lexicon.empty,
    2.23      val major: Scan.Lexicon = Scan.Lexicon.empty,
    2.24 -    protected val quasi_commands: Set[String] = Set.empty,
    2.25 -    protected val commands: Map[String, (String, List[String])] = Map.empty)
    2.26 +    val kinds: Map[String, String] = Map.empty,
    2.27 +    val load_commands: Map[String, List[String]] = Map.empty)
    2.28    {
    2.29      override def toString: String =
    2.30      {
    2.31 -      val keywords1 =
    2.32 -        for (name <- minor.iterator.toList) yield {
    2.33 -          if (quasi_commands.contains(name)) (name, quote(name) + " :: \"quasi_command\"")
    2.34 -          else (name, quote(name))
    2.35 +      val entries =
    2.36 +        for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
    2.37 +          val exts = load_commands.getOrElse(name, Nil)
    2.38 +          val kind_decl =
    2.39 +            if (kind == "") ""
    2.40 +            else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
    2.41 +          quote(name) + kind_decl
    2.42          }
    2.43 -      val keywords2 =
    2.44 -        for ((name, (kind, files)) <- commands.toList) yield {
    2.45 -          (name, quote(name) + " :: " + quote(kind) +
    2.46 -            (if (files.isEmpty) "" else " (" + commas_quote(files) + ")"))
    2.47 -        }
    2.48 -      (keywords1 ::: keywords2).sortBy(_._1).map(_._2).mkString("keywords\n  ", " and\n  ", "")
    2.49 +      entries.mkString("keywords\n  ", " and\n  ", "")
    2.50      }
    2.51  
    2.52  
    2.53 @@ -129,58 +130,58 @@
    2.54        else {
    2.55          val minor1 = minor ++ other.minor
    2.56          val major1 = major ++ other.major
    2.57 -        val quasi_commands1 = quasi_commands ++ other.quasi_commands
    2.58 -        val commands1 =
    2.59 -          if (commands eq other.commands) commands
    2.60 -          else if (commands.isEmpty) other.commands
    2.61 -          else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    2.62 -        new Keywords(minor1, major1, quasi_commands1, commands1)
    2.63 +        val kinds1 =
    2.64 +          if (kinds eq other.kinds) kinds
    2.65 +          else if (kinds.isEmpty) other.kinds
    2.66 +          else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    2.67 +        val load_commands1 =
    2.68 +          if (load_commands eq other.load_commands) load_commands
    2.69 +          else if (load_commands.isEmpty) other.load_commands
    2.70 +          else
    2.71 +            (load_commands /: other.load_commands) {
    2.72 +              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    2.73 +        new Keywords(minor1, major1, kinds1, load_commands1)
    2.74        }
    2.75  
    2.76  
    2.77      /* add keywords */
    2.78  
    2.79 -    def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
    2.80 -      if (kind == "") new Keywords(minor + name, major, quasi_commands, commands)
    2.81 -      else if (kind == QUASI_COMMAND)
    2.82 -        new Keywords(minor + name, major, quasi_commands + name, commands)
    2.83 -      else {
    2.84 -        val major1 = major + name
    2.85 -        val commands1 = commands + (name -> (kind, tags))
    2.86 -        new Keywords(minor, major1, quasi_commands, commands1)
    2.87 -      }
    2.88 +    def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
    2.89 +    {
    2.90 +      val kinds1 = kinds + (name -> kind)
    2.91 +      val (minor1, major1) =
    2.92 +        if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND)
    2.93 +          (minor + name, major)
    2.94 +        else (minor, major + name)
    2.95 +      val load_commands1 =
    2.96 +        if (kind == THY_LOAD) load_commands + (name -> exts)
    2.97 +        else load_commands
    2.98 +      new Keywords(minor1, major1, kinds1, load_commands1)
    2.99 +    }
   2.100  
   2.101      def add_keywords(header: Thy_Header.Keywords): Keywords =
   2.102        (this /: header) {
   2.103 -        case (keywords, (name, ((kind, tags), _), _)) =>
   2.104 +        case (keywords, (name, ((kind, exts), _), _)) =>
   2.105            if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
   2.106 -          else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
   2.107 +          else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
   2.108        }
   2.109  
   2.110  
   2.111      /* command kind */
   2.112  
   2.113 -    def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
   2.114 -
   2.115      def is_command(token: Token, check_kind: String => Boolean): Boolean =
   2.116        token.is_command &&
   2.117 -        (command_kind(token.source) match { case Some(k) => check_kind(k) case None => false })
   2.118 +        (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
   2.119 +
   2.120 +    def is_before_command(token: Token): Boolean =
   2.121 +      token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
   2.122  
   2.123      def is_quasi_command(token: Token): Boolean =
   2.124 -      token.is_keyword && quasi_commands.contains(token.source)
   2.125 +      token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
   2.126  
   2.127  
   2.128      /* load commands */
   2.129  
   2.130 -    def load_command(name: String): Option[List[String]] =
   2.131 -      commands.get(name) match {
   2.132 -        case Some((THY_LOAD, exts)) => Some(exts)
   2.133 -        case _ => None
   2.134 -      }
   2.135 -
   2.136 -    private lazy val load_commands: List[(String, List[String])] =
   2.137 -      (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
   2.138 -
   2.139      def load_commands_in(text: String): Boolean =
   2.140        load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   2.141    }
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Jul 11 14:25:06 2016 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Jul 11 16:36:29 2016 +0200
     3.3 @@ -118,7 +118,7 @@
     3.4  
     3.5    /* load commands */
     3.6  
     3.7 -  def load_command(name: String): Option[List[String]] = keywords.load_command(name)
     3.8 +  def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
     3.9    def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
    3.10  
    3.11  
    3.12 @@ -209,8 +209,9 @@
    3.13  
    3.14      for (tok <- toks) {
    3.15        if (tok.is_improper) improper += tok
    3.16 -      else if (tok.is_command_modifier ||
    3.17 -        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
    3.18 +      else if (keywords.is_before_command(tok) ||
    3.19 +        tok.is_command &&
    3.20 +          (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
    3.21        { flush(); content += tok }
    3.22        else { content ++= improper; improper.clear; content += tok }
    3.23      }
    3.24 @@ -236,7 +237,7 @@
    3.25        case Thy_Header.PARAGRAPH => Some(4)
    3.26        case Thy_Header.SUBPARAGRAPH => Some(5)
    3.27        case _ =>
    3.28 -        keywords.command_kind(name) match {
    3.29 +        keywords.kinds.get(name) match {
    3.30            case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
    3.31            case _ => None
    3.32          }
     4.1 --- a/src/Pure/Isar/token.scala	Mon Jul 11 14:25:06 2016 +0200
     4.2 +++ b/src/Pure/Isar/token.scala	Mon Jul 11 16:36:29 2016 +0200
     4.3 @@ -257,10 +257,6 @@
     4.4    def is_begin: Boolean = is_keyword && source == "begin"
     4.5    def is_end: Boolean = is_command && source == "end"
     4.6  
     4.7 -  // FIXME avoid hard-wired stuff
     4.8 -  def is_command_modifier: Boolean =
     4.9 -    is_keyword && (source == "public" || source == "private" || source == "qualified")
    4.10 -
    4.11    def content: String =
    4.12      if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
    4.13      else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)
     5.1 --- a/src/Pure/Pure.thy	Mon Jul 11 14:25:06 2016 +0200
     5.2 +++ b/src/Pure/Pure.thy	Mon Jul 11 16:36:29 2016 +0200
     5.3 @@ -8,8 +8,9 @@
     5.4  keywords
     5.5      "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     5.6      "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
     5.7 -    "open" "output" "overloaded" "pervasive" "premises" "private" "qualified"
     5.8 -    "structure" "unchecked" "where" "when" "|"
     5.9 +    "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked"
    5.10 +    "where" "when" "|"
    5.11 +  and "private" "qualified" :: before_command
    5.12    and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
    5.13      "obtains" "shows" :: quasi_command
    5.14    and "text" "txt" :: document_body
     6.1 --- a/src/Pure/System/options.scala	Mon Jul 11 14:25:06 2016 +0200
     6.2 +++ b/src/Pure/System/options.scala	Mon Jul 11 16:36:29 2016 +0200
     6.3 @@ -76,7 +76,9 @@
     6.4  
     6.5    lazy val options_syntax =
     6.6      Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
     6.7 -      (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL)
     6.8 +      (SECTION, Keyword.DOCUMENT_HEADING) +
     6.9 +      (PUBLIC, Keyword.BEFORE_COMMAND) +
    6.10 +      (OPTION, Keyword.THY_DECL)
    6.11  
    6.12    lazy val prefs_syntax = Outer_Syntax.init() + "="
    6.13  
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 11 14:25:06 2016 +0200
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 11 16:36:29 2016 +0200
     7.3 @@ -93,7 +93,7 @@
     7.4    }
     7.5  
     7.6    def token_markup(syntax: Outer_Syntax, token: Token): Byte =
     7.7 -    if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
     7.8 +    if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
     7.9      else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL
    7.10      else if (token.is_delimiter) JEditToken.OPERATOR
    7.11      else token_style(token.kind)
     8.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 14:25:06 2016 +0200
     8.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 16:36:29 2016 +0200
     8.3 @@ -275,13 +275,15 @@
     8.4    def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
     8.5      : Option[Text.Info[Command_Span.Span]] =
     8.6    {
     8.7 +    val keywords = syntax.keywords
     8.8 +
     8.9      def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
    8.10        token_reverse_iterator(syntax, buffer, i).
    8.11 -        find(info => info.info.is_command_modifier || info.info.is_command)
    8.12 +        find(info => keywords.is_before_command(info.info) || info.info.is_command)
    8.13  
    8.14      def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
    8.15        token_iterator(syntax, buffer, i).
    8.16 -        find(info => info.info.is_command_modifier || info.info.is_command)
    8.17 +        find(info => keywords.is_before_command(info.info) || info.info.is_command)
    8.18  
    8.19      if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
    8.20        val start_info =
    8.21 @@ -291,15 +293,16 @@
    8.22            case Some(Text.Info(range1, tok1)) if tok1.is_command =>
    8.23              val info2 = maybe_command_start(range1.start - 1)
    8.24              info2 match {
    8.25 -              case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
    8.26 +              case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
    8.27                case _ => info1
    8.28              }
    8.29            case _ => info1
    8.30          }
    8.31        }
    8.32 -      val (start_is_command_modifier, start, start_next) =
    8.33 +      val (start_before_command, start, start_next) =
    8.34          start_info match {
    8.35 -          case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
    8.36 +          case Some(Text.Info(range, tok)) =>
    8.37 +            (keywords.is_before_command(tok), range.start, range.stop)
    8.38            case None => (false, 0, 0)
    8.39          }
    8.40  
    8.41 @@ -307,7 +310,7 @@
    8.42        {
    8.43          val info1 = maybe_command_stop(start_next)
    8.44          info1 match {
    8.45 -          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
    8.46 +          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
    8.47              maybe_command_stop(range1.stop)
    8.48            case _ => info1
    8.49          }