# HG changeset patch
# User wenzelm
# Date 1535892986 -7200
# Node ID 33d78e5e0a0087532bbfd868776662db211e17c3
# Parent  cefaac3d24ffce5aba370a55347cfc832b37da9f
more robust reset_state: begin/end structure takes precedence over goal/proof structure;

diff -r cefaac3d24ff -r 33d78e5e0a00 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:14:43 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:56:26 2018 +0200
@@ -84,6 +84,7 @@
   val command_exception: bool -> transition -> state -> state
   val reset_theory: state -> state option
   val reset_proof: state -> state option
+  val reset_notepad: state -> state option
   type result
   val join_results: result -> (transition * state) list
   val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
@@ -642,6 +643,14 @@
       (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy))
         | _ => raise UNDEF)));
 
+val reset_notepad =
+  reset_state
+    (fn st =>
+      (case try proof_of st of
+        SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state
+      | NONE => true))
+    (proof (Proof.begin_notepad o Proof.context_of));
+
 end;
 
 
diff -r cefaac3d24ff -r 33d78e5e0a00 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Sep 02 14:14:43 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Sun Sep 02 14:56:26 2018 +0200
@@ -193,6 +193,10 @@
     val res =
       if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
       else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
+      else if Keyword.is_theory_end keywords name then
+        (case Toplevel.reset_notepad st0 of
+          NONE => Toplevel.reset_theory st0
+        | some => some)
       else NONE;
   in
     (case res of