--- a/src/Pure/Isar/keyword.scala Thu Jul 07 21:10:12 2016 +0200
+++ b/src/Pure/Isar/keyword.scala Thu Jul 07 21:34:56 2016 +0200
@@ -151,11 +151,9 @@
def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
- def is_command_kind(name: String, pred: String => Boolean): Boolean =
- command_kind(name) match {
- case Some(kind) => pred(kind)
- case None => false
- }
+ 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 })
/* load commands */
--- a/src/Pure/Isar/outer_syntax.scala Thu Jul 07 21:10:12 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Jul 07 21:34:56 2016 +0200
@@ -156,7 +156,7 @@
val command1 = tokens.exists(_.is_command)
val depth1 =
- if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
+ if (tokens.exists(keywords.is_command(_, Keyword.theory))) 0
else if (command1) structure.after_span_depth
else structure.span_depth
@@ -164,13 +164,13 @@
((structure.span_depth, structure.after_span_depth) /: tokens) {
case ((x, y), tok) =>
if (tok.is_command) {
- if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
- else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
- else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
- else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
- else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
- else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
- else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
+ if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
+ else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
+ else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
+ else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
+ else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y + 1, y - 2)
+ else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
+ else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
else (x, y)
}
else (x, y)
--- a/src/Pure/Isar/token.scala Thu Jul 07 21:10:12 2016 +0200
+++ b/src/Pure/Isar/token.scala Thu Jul 07 21:34:56 2016 +0200
@@ -225,8 +225,6 @@
sealed case class Token(kind: Token.Kind.Value, source: String)
{
def is_command: Boolean = kind == Token.Kind.COMMAND
- def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
- is_command && keywords.is_command_kind(source, pred)
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/text_structure.scala Thu Jul 07 21:10:12 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Thu Jul 07 21:34:56 2016 +0200
@@ -72,11 +72,9 @@
Isabelle.buffer_syntax(text_area.getBuffer) match {
case Some(syntax) =>
+ val keywords = syntax.keywords
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
- def is_command_kind(token: Token, pred: String => Boolean): Boolean =
- 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).
filter(_.info.is_proper)
@@ -93,45 +91,45 @@
iterator(caret_line, 1).find(info => info.range.touches(caret))
match {
- case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
+ case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) =>
find_block(
- is_command_kind(_, Keyword.proof_goal),
- is_command_kind(_, Keyword.qed),
- is_command_kind(_, Keyword.qed_global),
+ keywords.is_command(_, Keyword.proof_goal),
+ keywords.is_command(_, Keyword.qed),
+ keywords.is_command(_, Keyword.qed_global),
t =>
- is_command_kind(t, Keyword.diag) ||
- is_command_kind(t, Keyword.proof),
+ keywords.is_command(t, Keyword.diag) ||
+ keywords.is_command(t, Keyword.proof),
caret_iterator())
- case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
+ case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) =>
find_block(
- is_command_kind(_, Keyword.proof_goal),
- is_command_kind(_, Keyword.qed),
+ keywords.is_command(_, Keyword.proof_goal),
+ keywords.is_command(_, Keyword.qed),
_ => false,
t =>
- is_command_kind(t, Keyword.diag) ||
- is_command_kind(t, Keyword.proof),
+ keywords.is_command(t, Keyword.diag) ||
+ keywords.is_command(t, Keyword.proof),
caret_iterator())
- 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))
+ case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) =>
+ rev_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory))
match {
case Some(Text.Info(range2, tok))
- if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
+ if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2))
case _ => None
}
- case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
+ case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) =>
find_block(
- is_command_kind(_, Keyword.qed),
+ keywords.is_command(_, Keyword.qed),
t =>
- is_command_kind(t, Keyword.proof_goal) ||
- is_command_kind(t, Keyword.theory_goal),
+ keywords.is_command(t, Keyword.proof_goal) ||
+ keywords.is_command(t, Keyword.theory_goal),
_ => false,
t =>
- is_command_kind(t, Keyword.diag) ||
- is_command_kind(t, Keyword.proof) ||
- is_command_kind(t, Keyword.theory_goal),
+ keywords.is_command(t, Keyword.diag) ||
+ keywords.is_command(t, Keyword.proof) ||
+ keywords.is_command(t, Keyword.theory_goal),
rev_caret_iterator())
case Some(Text.Info(range1, tok)) if tok.is_begin =>
@@ -147,7 +145,7 @@
find(info => info.info.is_command || info.info.is_begin)
match {
case Some(Text.Info(range3, tok)) =>
- if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
+ if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3))
else Some((range1, range2))
case None => None
}