# HG changeset patch
# User wenzelm
# Date 1216115403 -7200
# Node ID 6683cdb94af8c29b61b2b54ca95f8fe34e6c27a4
# Parent  90cbc874549fe19d1a4b0c74f0ffa429eae03cb8
simplified commit_exit: operate on previous node of final state, include warning here;
misc tuning;

diff -r 90cbc874549f -r 6683cdb94af8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 15 11:50:02 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 15 11:50:03 2008 +0200
@@ -38,7 +38,6 @@
   val profiling: int ref
   val skip_proofs: bool ref
   exception TERMINATE
-  exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
   exception CONTEXT of Proof.context * exn
   val exn_message: exn -> string
@@ -55,7 +54,6 @@
   val no_timing: transition -> transition
   val init_theory: string -> (bool -> theory) -> (theory -> unit) -> transition -> transition
   val exit: transition -> transition
-  val commit_exit: transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
@@ -88,8 +86,9 @@
   val unknown_context: transition -> transition
   val error_msg: transition -> exn * string -> unit
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
+  val commit_exit: transition
+  val excursion: transition list -> unit
   val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
-  val excursion: transition list -> unit
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -147,9 +146,8 @@
 
 (* datatype state *)
 
-datatype state = State of
-  (node * (theory -> unit)) option *  (*current node with exit operation*)
-  node option;                        (*previous node*)
+type node_info = node * (theory -> unit);  (*node with exit operation*)
+datatype state = State of node_info option * node_info option;  (*current, previous*)
 
 val toplevel = State (NONE, NONE);
 
@@ -170,7 +168,7 @@
 
 (* current node *)
 
-fun previous_node_of (State (_, prev_node)) = prev_node;
+fun previous_node_of (State (_, prev_node)) = Option.map #1 prev_node;
 
 fun node_of (State (NONE, _)) = raise UNDEF
   | node_of (State (SOME (node, _), _)) = node;
@@ -312,17 +310,15 @@
 end;
 
 
-(* node transactions and recovery from stale theories *)
-
-(*NB: proof commands should be non-destructive!*)
+(* node transactions -- maintaining stable checkpoints *)
 
 local
 
-fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
-
 fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy)
   | is_draft_theory _ = false;
 
+fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
+
 fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!")
   | stale_error some = some;
 
@@ -332,12 +328,12 @@
 
 in
 
-fun transaction pos f (node, exit) =
+fun apply_transaction pos f (node, exit) =
   let
     val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state";
     val cont_node = reset_presentation node;
     val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node;
-    fun state_error e nd = (State (SOME (nd, exit), SOME node), e);
+    fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e);
 
     val (result, err) =
       cont_node
@@ -360,11 +356,6 @@
 
 (* primitive transitions *)
 
-(*Note: Recovery from stale theories is provided only for theory-level
-  operations via Transaction.  Other node or state operations should
-  not touch theories at all.  Interrupts are enabled only for Keep and
-  Transaction.*)
-
 datatype trans =
   Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*)
   Exit |                                         (*formal exit of theory -- without committing*)
@@ -376,14 +367,14 @@
 
 fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
-  | apply_tr _ _ Exit (State (SOME (node as Theory (Context.Theory _, _), _), _)) =
-      State (NONE, SOME node)
-  | apply_tr _ _ CommitExit (State (SOME (Theory (Context.Theory thy, _), exit), _)) =
+  | apply_tr _ _ Exit (State (SOME (node as Theory (Context.Theory _, _), exit), _)) =
+      State (NONE, SOME (node, exit))
+  | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
       (controlled_execution exit thy; toplevel)
   | apply_tr int _ (Keep f) state =
       controlled_execution (fn x => tap (f int) x) state
   | apply_tr int pos (Transaction f) (State (SOME state, _)) =
-      transaction pos (fn x => f int x) state
+      apply_transaction pos (fn x => f int x) state
   | apply_tr _ _ _ _ = raise UNDEF;
 
 fun apply_union _ _ [] state = raise FAILURE (state, UNDEF)
@@ -462,9 +453,8 @@
 
 fun init_theory name f exit = add_trans (Init (name, f, exit));
 val exit = add_trans Exit;
-val commit_exit = add_trans CommitExit (name "end" empty);
 val keep' = add_trans o Keep;
-fun app_current f = add_trans (Transaction f);
+fun transaction f = add_trans (Transaction f);
 
 fun keep f = add_trans (Keep (fn _ => f));
 fun imperative f = keep (fn _ => f ());
@@ -476,17 +466,17 @@
 
 (* theory transitions *)
 
-fun generic_theory f = app_current (fn _ =>
+fun generic_theory f = transaction (fn _ =>
   (fn Theory (gthy, _) => Theory (f gthy, NONE)
     | _ => raise UNDEF));
 
-fun theory' f = app_current (fn int =>
+fun theory' f = transaction (fn int =>
   (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
     | _ => raise UNDEF));
 
 fun theory f = theory' (K f);
 
-fun begin_local_theory begin f = app_current (fn _ =>
+fun begin_local_theory begin f = transaction (fn _ =>
   (fn Theory (Context.Theory thy, _) =>
         let
           val lthy = f thy;
@@ -494,13 +484,13 @@
         in Theory (gthy, SOME lthy) end
     | _ => raise UNDEF));
 
-val end_local_theory = app_current (fn _ =>
+val end_local_theory = transaction (fn _ =>
   (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
     | _ => raise UNDEF));
 
 local
 
-fun local_theory_presentation loc f g = app_current (fn int =>
+fun local_theory_presentation loc f g = transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
           val finish = loc_finish loc gthy;
@@ -518,7 +508,7 @@
 
 (* proof transitions *)
 
-fun end_proof f = app_current (fn int =>
+fun end_proof f = transaction (fn int =>
   (fn Proof (prf, (finish, _)) =>
         let val state = ProofNode.current prf in
           if can (Proof.assert_bottom true) state then
@@ -533,7 +523,7 @@
 
 local
 
-fun begin_proof init finish = app_current (fn int =>
+fun begin_proof init finish = transaction (fn int =>
   (fn Theory (gthy, _) =>
     let
       val prf = init int gthy;
@@ -562,17 +552,17 @@
 
 end;
 
-val forget_proof = app_current (fn _ =>
+val forget_proof = transaction (fn _ =>
   (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
-fun present_proof f = app_current (fn int =>
+fun present_proof f = transaction (fn int =>
   (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF) #> tap (f int));
 
-fun proofs' f = app_current (fn int =>
+fun proofs' f = transaction (fn int =>
   (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x)
     | skip as SkipProof _ => skip
     | _ => raise UNDEF));
@@ -581,15 +571,15 @@
 val proofs = proofs' o K;
 val proof = proof' o K;
 
-fun actual_proof f = app_current (fn _ =>
+fun actual_proof f = transaction (fn _ =>
   (fn Proof (prf, x) => Proof (f prf, x)
     | _ => raise UNDEF));
 
-fun skip_proof f = app_current (fn _ =>
+fun skip_proof f = transaction (fn _ =>
   (fn SkipProof (h, x) => SkipProof (f h, x)
     | _ => raise UNDEF));
 
-fun skip_proof_to_theory pred = app_current (fn _ =>
+fun skip_proof_to_theory pred = transaction (fn _ =>
   (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
   | _ => raise UNDEF));
 
@@ -646,29 +636,38 @@
 end;
 
 
+(* commit final exit *)
+
+val commit_exit =
+  name "end" empty
+  |> add_trans CommitExit
+  |> imperative (fn () => warning "Expected to find finished theory");
+
+
 (* excursion: toplevel -- apply transformers/presentation -- toplevel *)
 
 local
 
 fun no_pr _ _ _ = ();
 
-fun excur (tr, pr) st res =
+fun excur (tr, pr) (st, res) =
   (case transition (! interact) tr st of
     SOME (st', NONE) =>
-      (st, st', setmp_thread_position tr (fn () => pr st st' res) () handle exn =>
+      (st', setmp_thread_position tr (fn () => pr st st' res) () handle exn =>
         raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
   | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
   | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
 
-fun excurs (tr :: trs) (_, st, res) = excurs trs (excur tr st res)
-  | excurs [] (st, st', res') =
-      if is_toplevel st' then (excur (commit_exit, no_pr) st (); res')
-      else error "Unfinished development at end of input";
+fun excurs trs st_res =
+  let val (st', res') = fold excur trs st_res in
+    if is_toplevel st' then (excur (commit_exit, no_pr) (st', ()); res')
+    else error "Unfinished development at end of input"
+  end;
 
 in
 
 fun present_excursion trs res =
-  excurs trs (toplevel, toplevel, res) handle exn => error (exn_message exn);
+  excurs trs (toplevel, res) handle exn => error (exn_message exn);
 
 fun excursion trs = present_excursion (map (rpair no_pr) trs) ();