# HG changeset patch # User wenzelm # Date 1468247789 -7200 # Node ID 4c3fa4dba79f1bb91bcd2c80dde1f18692a3e591 # Parent 2ce032a41a3abcd318b498273bf24eedab93c89e explicit kind "before_command"; tuned signature; diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Pure/Isar/keyword.ML Mon Jul 11 16:36:29 2016 +0200 @@ -32,9 +32,11 @@ val prf_script: string val prf_script_goal: string val prf_script_asm_goal: string + val before_command: string val quasi_command: string type spec = (string * string list) * string list val no_spec: spec + val before_command_spec: spec val quasi_command_spec: spec type keywords val minor_keywords: keywords -> Scan.lexicon @@ -107,6 +109,8 @@ val prf_script = "prf_script"; val prf_script_goal = "prf_script_goal"; val prf_script_asm_goal = "prf_script_asm_goal"; + +val before_command = "before_command"; val quasi_command = "quasi_command"; val command_kinds = @@ -121,6 +125,7 @@ type spec = (string * string list) * string list; val no_spec: spec = (("", []), []); +val before_command_spec: spec = ((before_command, []), []); val quasi_command_spec: spec = ((quasi_command, []), []); type entry = @@ -175,7 +180,7 @@ val add_keywords = fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) => - if kind = "" orelse kind = quasi_command then + if kind = "" orelse kind = before_command orelse kind = quasi_command then let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; in (minor', major, commands) end diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Pure/Isar/keyword.scala Mon Jul 11 16:36:29 2016 +0200 @@ -39,6 +39,8 @@ val PRF_SCRIPT = "prf_script" val PRF_SCRIPT_GOAL = "prf_script_goal" val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal" + + val BEFORE_COMMAND = "before_command" val QUASI_COMMAND = "quasi_command" @@ -90,6 +92,7 @@ type Spec = ((String, List[String]), List[String]) val no_spec: Spec = (("", Nil), Nil) + val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil) val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil) object Keywords @@ -100,22 +103,20 @@ class Keywords private( val minor: Scan.Lexicon = Scan.Lexicon.empty, val major: Scan.Lexicon = Scan.Lexicon.empty, - protected val quasi_commands: Set[String] = Set.empty, - protected val commands: Map[String, (String, List[String])] = Map.empty) + val kinds: Map[String, String] = Map.empty, + val load_commands: Map[String, List[String]] = Map.empty) { override def toString: String = { - val keywords1 = - for (name <- minor.iterator.toList) yield { - if (quasi_commands.contains(name)) (name, quote(name) + " :: \"quasi_command\"") - else (name, quote(name)) + val entries = + for ((name, kind) <- kinds.toList.sortBy(_._1)) yield { + val exts = load_commands.getOrElse(name, Nil) + val kind_decl = + if (kind == "") "" + else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")") + quote(name) + kind_decl } - val keywords2 = - for ((name, (kind, files)) <- commands.toList) yield { - (name, quote(name) + " :: " + quote(kind) + - (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")) - } - (keywords1 ::: keywords2).sortBy(_._1).map(_._2).mkString("keywords\n ", " and\n ", "") + entries.mkString("keywords\n ", " and\n ", "") } @@ -129,58 +130,58 @@ else { val minor1 = minor ++ other.minor val major1 = major ++ other.major - val quasi_commands1 = quasi_commands ++ other.quasi_commands - val commands1 = - if (commands eq other.commands) commands - else if (commands.isEmpty) other.commands - else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } - new Keywords(minor1, major1, quasi_commands1, commands1) + val kinds1 = + if (kinds eq other.kinds) kinds + else if (kinds.isEmpty) other.kinds + else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } + val load_commands1 = + if (load_commands eq other.load_commands) load_commands + else if (load_commands.isEmpty) other.load_commands + else + (load_commands /: other.load_commands) { + case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } + new Keywords(minor1, major1, kinds1, load_commands1) } /* add keywords */ - def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords = - if (kind == "") new Keywords(minor + name, major, quasi_commands, commands) - else if (kind == QUASI_COMMAND) - new Keywords(minor + name, major, quasi_commands + name, commands) - else { - val major1 = major + name - val commands1 = commands + (name -> (kind, tags)) - new Keywords(minor, major1, quasi_commands, commands1) - } + def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords = + { + val kinds1 = kinds + (name -> kind) + val (minor1, major1) = + if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND) + (minor + name, major) + else (minor, major + name) + val load_commands1 = + if (kind == THY_LOAD) load_commands + (name -> exts) + else load_commands + new Keywords(minor1, major1, kinds1, load_commands1) + } def add_keywords(header: Thy_Header.Keywords): Keywords = (this /: header) { - case (keywords, (name, ((kind, tags), _), _)) => + case (keywords, (name, ((kind, exts), _), _)) => if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name) - else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags) + else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts) } /* command kind */ - def command_kind(name: String): Option[String] = commands.get(name).map(_._1) - def is_command(token: Token, check_kind: String => Boolean): Boolean = token.is_command && - (command_kind(token.source) match { case Some(k) => check_kind(k) case None => false }) + (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false }) + + def is_before_command(token: Token): Boolean = + token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND) def is_quasi_command(token: Token): Boolean = - token.is_keyword && quasi_commands.contains(token.source) + token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND) /* load commands */ - def load_command(name: String): Option[List[String]] = - commands.get(name) match { - case Some((THY_LOAD, exts)) => Some(exts) - case _ => None - } - - private lazy val load_commands: List[(String, List[String])] = - (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList - def load_commands_in(text: String): Boolean = load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) } diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Mon Jul 11 16:36:29 2016 +0200 @@ -118,7 +118,7 @@ /* load commands */ - def load_command(name: String): Option[List[String]] = keywords.load_command(name) + def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name) def load_commands_in(text: String): Boolean = keywords.load_commands_in(text) @@ -209,8 +209,9 @@ for (tok <- toks) { if (tok.is_improper) improper += tok - else if (tok.is_command_modifier || - tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command))) + else if (keywords.is_before_command(tok) || + tok.is_command && + (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command))) { flush(); content += tok } else { content ++= improper; improper.clear; content += tok } } @@ -236,7 +237,7 @@ case Thy_Header.PARAGRAPH => Some(4) case Thy_Header.SUBPARAGRAPH => Some(5) case _ => - keywords.command_kind(name) match { + keywords.kinds.get(name) match { case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6) case _ => None } diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Pure/Isar/token.scala Mon Jul 11 16:36:29 2016 +0200 @@ -257,10 +257,6 @@ def is_begin: Boolean = is_keyword && source == "begin" def is_end: Boolean = is_command && source == "end" - // FIXME avoid hard-wired stuff - def is_command_modifier: Boolean = - is_keyword && (source == "public" || source == "private" || source == "qualified") - def content: String = if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source) else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source) diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Pure/Pure.thy Mon Jul 11 16:36:29 2016 +0200 @@ -8,8 +8,9 @@ keywords "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is" - "open" "output" "overloaded" "pervasive" "premises" "private" "qualified" - "structure" "unchecked" "where" "when" "|" + "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" + "where" "when" "|" + and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites" "obtains" "shows" :: quasi_command and "text" "txt" :: document_body diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Pure/System/options.scala --- a/src/Pure/System/options.scala Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Pure/System/options.scala Mon Jul 11 16:36:29 2016 +0200 @@ -76,7 +76,9 @@ lazy val options_syntax = Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded + - (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL) + (SECTION, Keyword.DOCUMENT_HEADING) + + (PUBLIC, Keyword.BEFORE_COMMAND) + + (OPTION, Keyword.THY_DECL) lazy val prefs_syntax = Outer_Syntax.init() + "=" diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Mon Jul 11 16:36:29 2016 +0200 @@ -93,7 +93,7 @@ } def token_markup(syntax: Outer_Syntax, token: Token): Byte = - if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse("")) + if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, "")) else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL else if (token.is_delimiter) JEditToken.OPERATOR else token_style(token.kind) diff -r 2ce032a41a3a -r 4c3fa4dba79f src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Mon Jul 11 14:25:06 2016 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Mon Jul 11 16:36:29 2016 +0200 @@ -275,13 +275,15 @@ def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Option[Text.Info[Command_Span.Span]] = { + val keywords = syntax.keywords + def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] = token_reverse_iterator(syntax, buffer, i). - find(info => info.info.is_command_modifier || info.info.is_command) + find(info => keywords.is_before_command(info.info) || info.info.is_command) def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] = token_iterator(syntax, buffer, i). - find(info => info.info.is_command_modifier || info.info.is_command) + find(info => keywords.is_before_command(info.info) || info.info.is_command) if (JEdit_Lib.buffer_range(buffer).contains(offset)) { val start_info = @@ -291,15 +293,16 @@ case Some(Text.Info(range1, tok1)) if tok1.is_command => val info2 = maybe_command_start(range1.start - 1) info2 match { - case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2 + case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2 case _ => info1 } case _ => info1 } } - val (start_is_command_modifier, start, start_next) = + val (start_before_command, start, start_next) = start_info match { - case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop) + case Some(Text.Info(range, tok)) => + (keywords.is_before_command(tok), range.start, range.stop) case None => (false, 0, 0) } @@ -307,7 +310,7 @@ { val info1 = maybe_command_stop(start_next) info1 match { - case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier => + case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command => maybe_command_stop(range1.stop) case _ => info1 }