# HG changeset patch
# User wenzelm
# Date 1399968950 -7200
# Node ID 578dc6b4be89fe0ce8db55955f9a162bb12b6a40
# Parent  a3abb5222fce65f26d702f1262aa3e4f394413b9
no reset for 'end' -- e.g. relevant for 'notepad';

diff -r a3abb5222fce -r 578dc6b4be89 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue May 13 09:21:22 2014 +0200
+++ b/src/Pure/Isar/keyword.ML	Tue May 13 10:15:50 2014 +0200
@@ -61,6 +61,7 @@
   val is_theory_begin: string -> bool
   val is_theory_load: string -> bool
   val is_theory: string -> bool
+  val is_theory_body: string -> bool
   val is_proof: string -> bool
   val is_proof_body: string -> bool
   val is_theory_goal: string -> bool
@@ -250,6 +251,9 @@
   [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     thy_load, thy_decl, thy_goal];
 
+val is_theory_body = command_category
+  [thy_heading1, thy_heading2, thy_heading3, thy_heading4, thy_load, thy_decl, thy_goal];
+
 val is_proof = command_category
   [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,
diff -r a3abb5222fce -r 578dc6b4be89 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Tue May 13 09:21:22 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Tue May 13 10:15:50 2014 +0200
@@ -198,10 +198,8 @@
   let
     val name = Toplevel.name_of tr;
     val res =
-      if Keyword.is_theory name andalso not (Keyword.is_theory_begin name) then
-        Toplevel.reset_theory st0
-      else if Keyword.is_proof name then
-        Toplevel.reset_proof st0
+      if Keyword.is_theory_body name then Toplevel.reset_theory st0
+      else if Keyword.is_proof name then Toplevel.reset_proof st0
       else NONE;
   in
     (case res of