# HG changeset patch
# User wenzelm
# Date 1231589407 -3600
# Node ID 7ba952481e29f4b1c214b799e71f55050c47d393
# Parent  6baa02c8263e687a37fc1e24c90b8d6680d2b083
excursion: commit_exit internally -- checkpoints are fully persistent now;
excursion: do not force intermediate result states yet -- great performance improvement;

diff -r 6baa02c8263e -r 7ba952481e29 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Jan 10 01:28:31 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Jan 10 13:10:07 2009 +0100
@@ -96,7 +96,7 @@
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val commit_exit: Position.T -> transition
   val command: transition -> state -> state
-  val excursion: (transition * transition list) list -> (transition * state) list * (unit -> unit)
+  val excursion: (transition * transition list) list -> (transition * state) list lazy
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -746,12 +746,12 @@
     val end_pos = if null input then error "No input" else pos_of (fst (List.last input));
 
     val immediate = not (Future.enabled ());
-    val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
+    val (results, end_state) = fold_map (proof_result immediate) input toplevel;
     val _ =
       (case end_state of
-        State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
+        State (NONE, SOME (Theory (Context.Theory _, _), _)) =>
+          command (commit_exit end_pos) end_state
       | _ => error "Unfinished development at end of input");
-    val results = maps Lazy.force future_results;
-  in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end;
+  in Lazy.lazy (fn () => maps Lazy.force results) end;
 
 end;