--- 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
--- 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) })
}
--- 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
}
--- 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)
--- 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
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "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
--- 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() + "="
--- 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)
--- 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
}