clarified reset_notepad;
authorwenzelm
Sun Sep 02 19:48:15 2018 +0200 (9 months ago ago)
changeset 688789203eb13bef7
parent 68877 33d78e5e0a00
child 68879 feb1b1b3c51f
clarified reset_notepad;
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Sep 02 14:56:26 2018 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Sep 02 19:48:15 2018 +0200
     1.3 @@ -95,6 +95,7 @@
     1.4    val begin_notepad: context -> state
     1.5    val end_notepad: state -> context
     1.6    val is_notepad: state -> bool
     1.7 +  val reset_notepad: state -> state
     1.8    val proof: Method.text_range option -> state -> state Seq.result Seq.seq
     1.9    val defer: int -> state -> state
    1.10    val prefer: int -> state -> state
    1.11 @@ -893,13 +894,19 @@
    1.12    #> close_block
    1.13    #> context_of;
    1.14  
    1.15 -fun is_notepad (State stack) =
    1.16 +fun get_notepad_context (State stack) =
    1.17    let
    1.18 -    fun bottom_goal [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
    1.19 -      | bottom_goal [Node {goal = SOME _, ...}] = true
    1.20 -      | bottom_goal [] = false
    1.21 -      | bottom_goal (_ :: rest) = bottom_goal rest;
    1.22 -  in not (bottom_goal (op :: (Stack.dest stack))) end;
    1.23 +    fun escape [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = NONE
    1.24 +      | escape [Node {goal = SOME _, ...}] = NONE
    1.25 +      | escape [Node {goal = NONE, context = ctxt, ...}] = SOME ctxt
    1.26 +      | escape [] = NONE
    1.27 +      | escape (_ :: rest) = escape rest;
    1.28 +  in escape (op :: (Stack.dest stack)) end;
    1.29 +
    1.30 +val is_notepad = is_some o get_notepad_context;
    1.31 +
    1.32 +fun reset_notepad state =
    1.33 +  begin_notepad (the_default (context_of state) (get_notepad_context state));
    1.34  
    1.35  
    1.36  (* sub-proofs *)
     2.1 --- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:56:26 2018 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 19:48:15 2018 +0200
     2.3 @@ -649,7 +649,7 @@
     2.4        (case try proof_of st of
     2.5          SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state
     2.6        | NONE => true))
     2.7 -    (proof (Proof.begin_notepad o Proof.context_of));
     2.8 +    (proof Proof.reset_notepad);
     2.9  
    2.10  end;
    2.11