misc tuning and simplification;

--- a/src/Pure/Isar/toplevel.ML	Tue Apr 10 21:31:05 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 10 22:53:41 2012 +0200
@@ -659,50 +659,43 @@
 
 fun command_result tr st =
   let val st' = command tr st
-  in (st', st') end;
+  in ((tr, st'), st') end;
 
 
 (* scheduled proof result *)
 
-structure States = Proof_Data
+structure Result = Proof_Data
 (
-  type T = state list future option;
-  fun init _ = NONE;
+  type T = (transition * state) list future;
+  val empty: T = Future.value [];
+  fun init _ = empty;
 );
 
 fun proof_result immediate (tr, proof_trs) st =
-  let val st' = command tr st in
-    if immediate orelse null proof_trs orelse not (can proof_of st')
-    then
-      let val (states, st'') = fold_map command_result proof_trs st'
-      in (Future.value ((tr, st') :: (proof_trs ~~ states)), st'') end
-    else
-      let
-        val (body_trs, end_tr) = split_last proof_trs;
-        val finish = Context.Theory o Proof_Context.theory_of;
+  if immediate orelse null proof_trs
+  then fold_map command_result (tr :: proof_trs) st |>> Future.value
+  else
+    let
+      val st' = command tr st;
+      val (body_trs, end_tr) = split_last proof_trs;
+      val finish = Context.Theory o Proof_Context.theory_of;
 
-        val future_proof = Proof.global_future_proof
-          (fn prf =>
-            Goal.fork_name "Toplevel.future_proof"
-              (fn () =>
-                let val (states, result_state) =
-                  (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
-                    => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
-                  |> fold_map command_result body_trs
-                  ||> command (end_tr |> set_print false);
-                in (states, presentation_context_of result_state) end))
-          #> (fn (states, ctxt) => States.put (SOME states) ctxt);
+      val future_proof = Proof.global_future_proof
+        (fn prf =>
+          Goal.fork_name "Toplevel.future_proof"
+            (fn () =>
+              let val (result, result_state) =
+                (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev)
+                  => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev))
+                |> fold_map command_result body_trs ||> command end_tr;
+              in (result, presentation_context_of result_state) end))
+        #-> Result.put;
 
-        val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+      val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof));
+      val result =
+        Result.get (presentation_context_of st'')
+        |> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]);
 
-        val states =
-          (case States.get (presentation_context_of st'') of
-            NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr))
-          | SOME states => states);
-        val result = states
-          |> Future.map (fn sts => (tr, st') :: (body_trs ~~ sts) @ [(end_tr, st'')]);
-
-      in (result, st'') end
-  end;
+    in (result, st'') end;
 
 end;