# HG changeset patch
# User wenzelm
# Date 1535910495 -7200
# Node ID 9203eb13bef717f377b4dd268c7610da4d13e706
# Parent  33d78e5e0a0087532bbfd868776662db211e17c3
clarified reset_notepad;

diff -r 33d78e5e0a00 -r 9203eb13bef7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Sep 02 14:56:26 2018 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Sep 02 19:48:15 2018 +0200
@@ -95,6 +95,7 @@
   val begin_notepad: context -> state
   val end_notepad: state -> context
   val is_notepad: state -> bool
+  val reset_notepad: state -> state
   val proof: Method.text_range option -> state -> state Seq.result Seq.seq
   val defer: int -> state -> state
   val prefer: int -> state -> state
@@ -893,13 +894,19 @@
   #> close_block
   #> context_of;
 
-fun is_notepad (State stack) =
+fun get_notepad_context (State stack) =
   let
-    fun bottom_goal [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
-      | bottom_goal [Node {goal = SOME _, ...}] = true
-      | bottom_goal [] = false
-      | bottom_goal (_ :: rest) = bottom_goal rest;
-  in not (bottom_goal (op :: (Stack.dest stack))) end;
+    fun escape [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = NONE
+      | escape [Node {goal = SOME _, ...}] = NONE
+      | escape [Node {goal = NONE, context = ctxt, ...}] = SOME ctxt
+      | escape [] = NONE
+      | escape (_ :: rest) = escape rest;
+  in escape (op :: (Stack.dest stack)) end;
+
+val is_notepad = is_some o get_notepad_context;
+
+fun reset_notepad state =
+  begin_notepad (the_default (context_of state) (get_notepad_context state));
 
 
 (* sub-proofs *)
diff -r 33d78e5e0a00 -r 9203eb13bef7 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:56:26 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 19:48:15 2018 +0200
@@ -649,7 +649,7 @@
       (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));
+    (proof Proof.reset_notepad);
 
 end;