# HG changeset patch # User wenzelm # Date 1467920096 -7200 # Node ID e4e15bbfb3e2b885108bc52568b602344180b3a3 # Parent ed65a6d9929bc896f08068e0740fba295b69a149 clarified signature; diff -r ed65a6d9929b -r e4e15bbfb3e2 src/Pure/Isar/keyword.scala --- 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 */ diff -r ed65a6d9929b -r e4e15bbfb3e2 src/Pure/Isar/outer_syntax.scala --- 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) diff -r ed65a6d9929b -r e4e15bbfb3e2 src/Pure/Isar/token.scala --- 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 diff -r ed65a6d9929b -r e4e15bbfb3e2 src/Tools/jEdit/src/text_structure.scala --- 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 }