--- a/src/Pure/Isar/keyword.scala Tue Dec 09 20:00:45 2014 +0100
+++ b/src/Pure/Isar/keyword.scala Tue Dec 09 21:14:11 2014 +0100
@@ -139,10 +139,6 @@
def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
- def is_command_kind(token: Token, pred: String => Boolean): Boolean =
- token.is_command &&
- (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
-
/* load commands */
--- a/src/Pure/Isar/outer_syntax.scala Tue Dec 09 20:00:45 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Tue Dec 09 21:14:11 2014 +0100
@@ -156,7 +156,7 @@
val command1 = tokens.exists(_.is_command)
val depth1 =
- if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
+ if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
else if (command1) struct.after_span_depth
else struct.span_depth
@@ -164,15 +164,15 @@
((struct.span_depth, struct.after_span_depth) /: tokens) {
case ((x, y), tok) =>
if (tok.is_command) {
- if (keywords.is_command_kind(tok, Keyword.theory_goal))
+ if (tok.is_command_kind(keywords, Keyword.theory_goal))
(2, 1)
- else if (keywords.is_command_kind(tok, Keyword.theory))
+ else if (tok.is_command_kind(keywords, Keyword.theory))
(1, 0)
- else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
+ else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
(y + 2, y + 1)
- else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
+ else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
(y + 1, y - 1)
- else if (keywords.is_command_kind(tok, Keyword.qed_global))
+ else if (tok.is_command_kind(keywords, Keyword.qed_global))
(1, 0)
else (x, y)
}
--- a/src/Pure/Isar/token.scala Tue Dec 09 20:00:45 2014 +0100
+++ b/src/Pure/Isar/token.scala Tue Dec 09 21:14:11 2014 +0100
@@ -194,6 +194,9 @@
sealed case class Token(val kind: Token.Kind.Value, val source: String)
{
def is_command: Boolean = kind == Token.Kind.COMMAND
+ def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
+ is_command &&
+ (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
def is_keyword: Boolean = kind == Token.Kind.KEYWORD
def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
def is_ident: Boolean = kind == Token.Kind.IDENT
--- a/src/Tools/jEdit/src/structure_matching.scala Tue Dec 09 20:00:45 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala Tue Dec 09 21:14:11 2014 +0100
@@ -45,7 +45,7 @@
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
def is_command_kind(token: Token, pred: String => Boolean): Boolean =
- syntax.keywords.is_command_kind(token, pred)
+ token.is_command_kind(syntax.keywords, pred)
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).