--- a/src/Pure/Isar/keyword.scala Wed Nov 05 16:57:12 2014 +0100
+++ b/src/Pure/Isar/keyword.scala Wed Nov 05 17:37:25 2014 +0100
@@ -13,7 +13,6 @@
/* kinds */
- val MINOR = "minor"
val DIAG = "diag"
val HEADING = "heading"
val THY_BEGIN = "thy_begin"
@@ -74,55 +73,59 @@
{
def empty: Keywords = new Keywords()
- def apply(names: List[String]): Keywords =
- (empty /: names)({ case (keywords, a) => keywords + (a, (MINOR, Nil)) })
+ def apply(keywords: List[String]): Keywords = (empty /: keywords)(_ + _)
}
class Keywords private(
- keywords: Map[String, (String, List[String])] = Map.empty,
val minor: Scan.Lexicon = Scan.Lexicon.empty,
- val major: Scan.Lexicon = Scan.Lexicon.empty)
+ val major: Scan.Lexicon = Scan.Lexicon.empty,
+ command_kinds: Map[String, (String, List[String])] = Map.empty)
{
/* content */
- override def toString: String =
- (for ((name, (kind, files)) <- keywords) yield {
- if (kind == MINOR) quote(name)
- else
- quote(name) + " :: " + quote(kind) +
- (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
- }).toList.sorted.mkString("keywords\n ", " and\n ", "")
+ def is_empty: Boolean = minor.isEmpty && major.isEmpty
- def is_empty: Boolean = keywords.isEmpty
+ def + (name: String): Keywords =
+ new Keywords(minor + name, major, command_kinds)
def + (name: String, kind: (String, List[String])): Keywords =
{
- val keywords1 = keywords + (name -> kind)
- val (minor1, major1) =
- if (kind._1 == MINOR) (minor + name, major) else (minor, major + name)
- new Keywords(keywords1, minor1, major1)
+ val major1 = major + name
+ val command_kinds1 = command_kinds + (name -> kind)
+ new Keywords(minor, major1, command_kinds1)
+ }
+
+ override def toString: String =
+ {
+ val keywords = minor.iterator.map(quote(_)).toList
+ val commands =
+ for ((name, (kind, files)) <- command_kinds.toList.sortBy(_._1)) yield {
+ quote(name) + " :: " + quote(kind) +
+ (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
+ }
+ (keywords ::: commands).mkString("keywords\n ", " and\n ", "")
}
- /* kind */
+ /* command kind */
- def kind(name: String): Option[String] = keywords.get(name).map(_._1)
+ def command_kind(name: String): Option[String] = command_kinds.get(name).map(_._1)
- def command_kind(token: Token, pred: String => Boolean): Boolean =
+ def is_command_kind(token: Token, pred: String => Boolean): Boolean =
token.is_command &&
- (kind(token.source) match { case Some(k) => k != MINOR && pred(k) case None => false })
+ (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
/* load commands */
def load_command(name: String): Option[List[String]] =
- keywords.get(name) match {
+ command_kinds.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)) <- keywords.iterator) yield (name, files)).toList
+ (for ((name, (THY_LOAD, files)) <- command_kinds.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 Wed Nov 05 16:57:12 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Wed Nov 05 17:37:25 2014 +0100
@@ -86,33 +86,29 @@
/* add keywords */
- def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
+ def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
+ : Outer_Syntax =
{
- val keywords1 = keywords + (name, kind)
+ val keywords1 =
+ opt_kind match {
+ case None => keywords + name
+ case Some(kind) => keywords + (name, kind)
+ }
val completion1 =
if (replace == Some("")) completion
else completion + (name, replace getOrElse name)
new Outer_Syntax(keywords1, completion1, language_context, true)
}
-
- def + (name: String, kind: (String, List[String])): Outer_Syntax =
- this + (name, kind, Some(name))
- def + (name: String, kind: String): Outer_Syntax =
- this + (name, (kind, Nil), Some(name))
- def + (name: String, replace: Option[String]): Outer_Syntax =
- this + (name, (Keyword.MINOR, Nil), replace)
- def + (name: String): Outer_Syntax = this + (name, None)
+ def + (name: String): Outer_Syntax = this + (name, None, None)
+ def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
(this /: keywords) {
- case (syntax, (name, Some((kind, _)), replace)) =>
+ case (syntax, (name, opt_spec, replace)) =>
+ val opt_kind = opt_spec.map(_._1)
syntax +
- (Symbol.decode(name), kind, replace) +
- (Symbol.encode(name), kind, replace)
- case (syntax, (name, None, replace)) =>
- syntax +
- (Symbol.decode(name), replace) +
- (Symbol.encode(name), replace)
+ (Symbol.decode(name), opt_kind, replace) +
+ (Symbol.encode(name), opt_kind, replace)
}
@@ -149,7 +145,7 @@
val command1 = tokens.exists(_.is_command)
val depth1 =
- if (tokens.exists(tok => keywords.command_kind(tok, Keyword.theory))) 0
+ if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
else if (command1) struct.after_span_depth
else struct.span_depth
@@ -157,15 +153,15 @@
((struct.span_depth, struct.after_span_depth) /: tokens) {
case ((x, y), tok) =>
if (tok.is_command) {
- if (keywords.command_kind(tok, Keyword.theory_goal))
+ if (keywords.is_command_kind(tok, Keyword.theory_goal))
(2, 1)
- else if (keywords.command_kind(tok, Keyword.theory))
+ else if (keywords.is_command_kind(tok, Keyword.theory))
(1, 0)
- else if (keywords.command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
+ else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
(y + 2, y + 1)
- else if (keywords.command_kind(tok, Keyword.qed) || tok.is_end_block)
+ else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
(y + 1, y - 1)
- else if (keywords.command_kind(tok, Keyword.qed_global))
+ else if (keywords.is_command_kind(tok, Keyword.qed_global))
(1, 0)
else (x, y)
}
@@ -254,7 +250,7 @@
case "subsection" => Some(2)
case "subsubsection" => Some(3)
case _ =>
- keywords.kind(command.name) match {
+ keywords.command_kind(command.name) match {
case Some(kind) if Keyword.theory(kind) => Some(4)
case _ => None
}
--- a/src/Tools/jEdit/src/rendering.scala Wed Nov 05 16:57:12 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Wed Nov 05 17:37:25 2014 +0100
@@ -85,7 +85,7 @@
}
def token_markup(syntax: Outer_Syntax, token: Token): Byte =
- if (token.is_command) command_style(syntax.keywords.kind(token.content).getOrElse(""))
+ if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
else if (token.is_delimiter) JEditToken.OPERATOR
else token_style(token.kind)
--- a/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 16:57:12 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 17:37:25 2014 +0100
@@ -44,8 +44,8 @@
case Some(syntax) =>
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
- def command_kind(token: Token, pred: String => Boolean): Boolean =
- syntax.keywords.command_kind(token, pred)
+ def is_command_kind(token: Token, pred: String => Boolean): Boolean =
+ syntax.keywords.is_command_kind(token, pred)
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
@@ -63,45 +63,45 @@
iterator(caret_line, 1).find(info => info.range.touches(caret))
match {
- case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.theory_goal) =>
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
find_block(
- command_kind(_, Keyword.proof_goal),
- command_kind(_, Keyword.qed),
- command_kind(_, Keyword.qed_global),
+ is_command_kind(_, Keyword.proof_goal),
+ is_command_kind(_, Keyword.qed),
+ is_command_kind(_, Keyword.qed_global),
t =>
- command_kind(t, Keyword.diag) ||
- command_kind(t, Keyword.proof),
+ is_command_kind(t, Keyword.diag) ||
+ is_command_kind(t, Keyword.proof),
caret_iterator())
- case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.proof_goal) =>
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
find_block(
- command_kind(_, Keyword.proof_goal),
- command_kind(_, Keyword.qed),
+ is_command_kind(_, Keyword.proof_goal),
+ is_command_kind(_, Keyword.qed),
_ => false,
t =>
- command_kind(t, Keyword.diag) ||
- command_kind(t, Keyword.proof),
+ is_command_kind(t, Keyword.diag) ||
+ is_command_kind(t, Keyword.proof),
caret_iterator())
- case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed_global) =>
- rev_caret_iterator().find(info => command_kind(info.info, Keyword.theory))
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) =>
+ rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory))
match {
case Some(Text.Info(range2, tok))
- if command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
+ if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
case _ => None
}
- case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed) =>
+ case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
find_block(
- command_kind(_, Keyword.qed),
+ is_command_kind(_, Keyword.qed),
t =>
- command_kind(t, Keyword.proof_goal) ||
- command_kind(t, Keyword.theory_goal),
+ is_command_kind(t, Keyword.proof_goal) ||
+ is_command_kind(t, Keyword.theory_goal),
_ => false,
t =>
- command_kind(t, Keyword.diag) ||
- command_kind(t, Keyword.proof) ||
- command_kind(t, Keyword.theory_goal),
+ is_command_kind(t, Keyword.diag) ||
+ is_command_kind(t, Keyword.proof) ||
+ is_command_kind(t, Keyword.theory_goal),
rev_caret_iterator())
case Some(Text.Info(range1, tok)) if tok.is_begin =>
@@ -117,7 +117,7 @@
find(info => info.info.is_command || info.info.is_begin)
match {
case Some(Text.Info(range3, tok)) =>
- if (command_kind(tok, Keyword.theory_block)) Some((range1, range3))
+ if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
else Some((range1, range2))
case None => None
}