# HG changeset patch
# User wenzelm
# Date 1414492971 -3600
# Node ID bfed1c26caed55596ff0fe5f6e51534d64418967
# Parent  944364b48eb908cf15f3f544cccd1c97dc295128
explicit keyword category for commands that may start a block;

diff -r 944364b48eb9 -r bfed1c26caed src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Oct 28 11:27:57 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Tue Oct 28 11:42:51 2014 +0100
@@ -18,6 +18,7 @@
   val thy_heading3: T
   val thy_heading4: T
   val thy_decl: T
+  val thy_decl_block: T
   val thy_load: T
   val thy_load_files: string list -> T
   val thy_goal: T
@@ -100,6 +101,7 @@
 val thy_heading3 = kind "thy_heading3";
 val thy_heading4 = kind "thy_heading4";
 val thy_decl = kind "thy_decl";
+val thy_decl_block = kind "thy_decl_block";
 val thy_load = kind "thy_load";
 fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
 val thy_goal = kind "thy_goal";
@@ -123,7 +125,7 @@
 
 val kinds =
   [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_goal, qed, qed_script, qed_block, qed_global,
+    thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global,
     prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
 
@@ -249,10 +251,11 @@
 
 val is_theory = command_category
   [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
-    thy_load, thy_decl, thy_goal];
+    thy_load, thy_decl, thy_decl_block, thy_goal];
 
 val is_theory_body = command_category
-  [thy_heading1, thy_heading2, thy_heading3, thy_heading4, thy_load, thy_decl, thy_goal];
+  [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
+    thy_load, thy_decl, thy_decl_block, thy_goal];
 
 val is_proof = command_category
   [qed, qed_script, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
diff -r 944364b48eb9 -r bfed1c26caed src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Tue Oct 28 11:27:57 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Tue Oct 28 11:42:51 2014 +0100
@@ -21,6 +21,7 @@
   val THY_HEADING3 = "thy_heading3"
   val THY_HEADING4 = "thy_heading4"
   val THY_DECL = "thy_decl"
+  val THY_DECL_BLOCK = "thy_decl_block"
   val THY_LOAD = "thy_load"
   val THY_GOAL = "thy_goal"
   val QED = "qed"
@@ -54,6 +55,8 @@
     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
       THY_LOAD, THY_DECL, THY_GOAL)
 
+  val theory_block = Set(THY_BEGIN, THY_DECL_BLOCK)
+
   val theory_body =
     Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
 
diff -r 944364b48eb9 -r bfed1c26caed src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Oct 28 11:27:57 2014 +0100
+++ b/src/Pure/Pure.thy	Tue Oct 28 11:42:51 2014 +0100
@@ -43,18 +43,18 @@
   and "bundle" :: thy_decl
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
-  and "context" "locale" :: thy_decl
+  and "context" "locale" :: thy_decl_block
   and "sublocale" "interpretation" :: thy_goal
   and "interpret" :: prf_goal % "proof"
-  and "class" :: thy_decl
+  and "class" :: thy_decl_block
   and "subclass" :: thy_goal
-  and "instantiation" :: thy_decl
+  and "instantiation" :: thy_decl_block
   and "instance" :: thy_goal
-  and "overloading" :: thy_decl
+  and "overloading" :: thy_decl_block
   and "code_datatype" :: thy_decl
   and "theorem" "lemma" "corollary" :: thy_goal
   and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
-  and "notepad" :: thy_decl
+  and "notepad" :: thy_decl_block
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof" == "then have"
   and "show" :: prf_asm_goal % "proof"
diff -r 944364b48eb9 -r bfed1c26caed src/Pure/Tools/keywords.scala
--- a/src/Pure/Tools/keywords.scala	Tue Oct 28 11:27:57 2014 +0100
+++ b/src/Pure/Tools/keywords.scala	Tue Oct 28 11:42:51 2014 +0100
@@ -25,6 +25,7 @@
     "thy_heading4" -> "theory-heading",
     "thy_load" -> "theory-decl",
     "thy_decl" -> "theory-decl",
+    "thy_decl_block" -> "theory-decl",
     "thy_goal" -> "theory-goal",
     "qed_script" -> "qed",
     "qed_block" -> "qed-block",
diff -r 944364b48eb9 -r bfed1c26caed src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 11:27:57 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 11:42:51 2014 +0100
@@ -110,12 +110,14 @@
               find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
               match {
                 case Some((_, range2)) =>
-                  rev_caret_iterator().dropWhile(info => info.range != range2).
-                    find(info =>
-                      // FIXME more precise keyword category
-                      syntax.command_kind(info.info, Set(Keyword.THY_BEGIN, Keyword.THY_DECL)))
+                  rev_caret_iterator().
+                    dropWhile(info => info.range != range2).
+                    dropWhile(info => info.range == range2).
+                    find(info => info.info.is_command || info.info.is_begin)
                   match {
-                    case Some(Text.Info(range3, _)) => Some((range1, range3))
+                    case Some(Text.Info(range3, tok)) =>
+                      if (syntax.command_kind(tok, Keyword.theory_block)) Some((range1, range3))
+                      else Some((range1, range2))
                     case None => None
                   }
                 case None => None