more robust reset_state: begin/end structure takes precedence over goal/proof structure;
authorwenzelm
Sun Sep 02 14:56:26 2018 +0200 (9 months ago ago)
changeset 6887733d78e5e0a00
parent 68876 cefaac3d24ff
child 68878 9203eb13bef7
more robust reset_state: begin/end structure takes precedence over goal/proof structure;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
     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  
     2.1 --- a/src/Pure/PIDE/command.ML	Sun Sep 02 14:14:43 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Sun Sep 02 14:56:26 2018 +0200
     2.3 @@ -193,6 +193,10 @@
     2.4      val res =
     2.5        if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
     2.6        else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
     2.7 +      else if Keyword.is_theory_end keywords name then
     2.8 +        (case Toplevel.reset_notepad st0 of
     2.9 +          NONE => Toplevel.reset_theory st0
    2.10 +        | some => some)
    2.11        else NONE;
    2.12    in
    2.13      (case res of