src/Pure/Isar/toplevel.ML
changeset 68877 33d78e5e0a00
parent 68876 cefaac3d24ff
child 68878 9203eb13bef7
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:14:43 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:56:26 2018 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4    val command_exception: bool -> transition -> state -> state
     1.5    val reset_theory: state -> state option
     1.6    val reset_proof: state -> state option
     1.7 +  val reset_notepad: state -> state option
     1.8    type result
     1.9    val join_results: result -> (transition * state) list
    1.10    val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
    1.11 @@ -642,6 +643,14 @@
    1.12        (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy))
    1.13          | _ => raise UNDEF)));
    1.14  
    1.15 +val reset_notepad =
    1.16 +  reset_state
    1.17 +    (fn st =>
    1.18 +      (case try proof_of st of
    1.19 +        SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state
    1.20 +      | NONE => true))
    1.21 +    (proof (Proof.begin_notepad o Proof.context_of));
    1.22 +
    1.23  end;
    1.24  
    1.25