# HG changeset patch
# User wenzelm
# Date 1418156051 -3600
# Node ID c1dbcde94cd27a735efab81fed1f74d6fb709acf
# Parent  8ea2748241da740b153a47f1d74a9a14543ceeca
tuned signature;

diff -r 8ea2748241da -r c1dbcde94cd2 src/Pure/Isar/keyword.scala
--- 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 */
 
diff -r 8ea2748241da -r c1dbcde94cd2 src/Pure/Isar/outer_syntax.scala
--- 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)
           }
diff -r 8ea2748241da -r c1dbcde94cd2 src/Pure/Isar/token.scala
--- 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
diff -r 8ea2748241da -r c1dbcde94cd2 src/Tools/jEdit/src/structure_matching.scala
--- 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).