no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
authorwenzelm
Sun Sep 02 14:14:43 2018 +0200 (9 months ago ago)
changeset 68876cefaac3d24ff
parent 68875 7f0151c951e3
child 68877 33d78e5e0a00
no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
src/Pure/Isar/toplevel.ML
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 13:53:55 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:14:43 2018 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4      (local_theory -> Proof.state) -> transition -> transition
     1.5    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
     1.6    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
     1.7 -  val forget_proof: bool -> transition -> transition
     1.8 +  val forget_proof: transition -> transition
     1.9    val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    1.10    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    1.11    val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    1.12 @@ -517,10 +517,10 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -fun forget_proof strict = transaction (fn _ =>
    1.17 +val forget_proof = transaction (fn _ =>
    1.18    (fn Proof (prf, (_, orig_gthy)) =>
    1.19 -        if strict andalso Proof.is_notepad (Proof_Node.current prf)
    1.20 -        then raise UNDEF else Theory (orig_gthy, NONE)
    1.21 +        if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF
    1.22 +        else Theory (orig_gthy, NONE)
    1.23      | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.24      | _ => raise UNDEF));
    1.25  
    1.26 @@ -634,7 +634,7 @@
    1.27  
    1.28  in
    1.29  
    1.30 -val reset_theory = reset_state is_theory (forget_proof false);
    1.31 +val reset_theory = reset_state is_theory forget_proof;
    1.32  
    1.33  val reset_proof =
    1.34    reset_state is_proof
     2.1 --- a/src/Pure/Pure.thy	Sun Sep 02 13:53:55 2018 +0200
     2.2 +++ b/src/Pure/Pure.thy	Sun Sep 02 14:14:43 2018 +0200
     2.3 @@ -916,7 +916,7 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
     2.7 -    (Scan.succeed (Toplevel.forget_proof true));
     2.8 +    (Scan.succeed Toplevel.forget_proof);
     2.9  
    2.10  in end\<close>
    2.11