# HG changeset patch
# User wenzelm
# Date 1343827988 -7200
# Node ID c9344758080d3e01acbd682ad294d5f2742c1efc
# Parent  21c42b095c841d1a7508c143d6b6e98d95dbfa69
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);

diff -r 21c42b095c84 -r c9344758080d src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun May 20 11:34:33 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 01 15:33:08 2012 +0200
@@ -672,31 +672,34 @@
 );
 
 fun proof_result immediate (tr, proof_trs) st =
-  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;
+  let val st' = command tr st in
+    if immediate orelse null proof_trs orelse not (can proof_of st')
+    then
+      let val (results, st'') = fold_map command_result proof_trs st'
+      in (Future.value ((tr, st') :: results), st'') end
+    else
+      let
+        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 (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 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 (tr |> set_print false |> 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 st'' = st'
+          |> command (tr |> set_print false |> 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'')]);
 
-    in (result, st'') end;
+      in (result, st'') end
+  end;
 
 end;