# 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