src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:17:50 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Feb 25 12:52:27 2013 +0100
@@ -95,7 +95,7 @@
   val put_timing: Time.time -> transition -> transition
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command: transition -> state -> state
-  val proof_result: bool -> transition * transition list -> state ->
+  val element_result: transition Thy_Syntax.element -> state ->
     (transition * state) list future * state
 end;
 
@@ -694,10 +694,6 @@
       if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
   | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
 
-fun command_result tr st =
-  let val st' = command tr st
-  in ((tr, st'), st') end;
-
 
 (* scheduled proof result *)
 
@@ -708,13 +704,27 @@
   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') orelse
-      Proof.is_relevant (proof_of st')
+fun element_result (Thy_Syntax.Element (head_tr, opt_proof)) st =
+  let
+    val future_enabled = Goal.future_enabled ();
+
+    fun atom_result tr st =
+      let val st' = command tr st
+      in ((tr, st'), st') end;
+
+    val proof_trs =
+      (case opt_proof of
+        NONE => []
+      | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out is_ignored);
+
+    val st' = command head_tr st;
+  in
+    if not future_enabled orelse is_ignored head_tr orelse
+      Keyword.is_schematic_goal (name_of head_tr) orelse null proof_trs orelse
+      not (can proof_of st') orelse Proof.is_relevant (proof_of st')
     then
-      let val (results, st'') = fold_map command_result proof_trs st'
-      in (Future.value ((tr, st') :: results), st'') end
+      let val (results, st'') = fold_map atom_result proof_trs st'
+      in (Future.value (if is_ignored head_tr then results else (head_tr, st') :: results), st'') end
     else
       let
         val (body_trs, end_tr) = split_last proof_trs;
@@ -732,15 +742,15 @@
                 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;
+                  |> fold_map atom_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));
+          |> command (head_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'')]);
+          |> Future.map (fn body => (head_tr, st') :: body @ [(end_tr, st'')]);
 
       in (result, st'') end
   end;