# HG changeset patch
# User wenzelm
# Date 1362405826 -3600
# Node ID 8707df0b0255651e3dd40781bd457776d1fdd713
# Parent  e7fab0b5dbe7c24e8b3bde35ec3e57ac8d2310d0
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;

diff -r e7fab0b5dbe7 -r 8707df0b0255 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Mar 04 11:36:16 2013 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Mar 04 15:03:46 2013 +0100
@@ -1191,7 +1191,7 @@
 in
 
 fun local_future_terminal_proof meths =
-  future_terminal_proof 2
+  future_terminal_proof 3
     (local_terminal_proof meths)
     (local_terminal_proof meths #> context_of) local_done_proof;
 
diff -r e7fab0b5dbe7 -r 8707df0b0255 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Mar 04 11:36:16 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML	Mon Mar 04 15:03:46 2013 +0100
@@ -96,8 +96,9 @@
   val transition: bool -> transition -> state -> (state * (exn * string) option) option
   val command_errors: bool -> transition -> state -> Runtime.error list * state option
   val command_exception: bool -> transition -> state -> state
-  val element_result: transition Thy_Syntax.element -> state ->
-    (transition * state) list future * state
+  type result
+  val join_results: result -> (transition * state) list
+  val element_result: transition Thy_Syntax.element -> state -> result * state
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -705,19 +706,26 @@
 
 (* scheduled proof result *)
 
+datatype result =
+  Result of transition * state |
+  Result_List of result list |
+  Result_Future of result future;
+
+fun join_results (Result x) = [x]
+  | join_results (Result_List xs) = maps join_results xs
+  | join_results (Result_Future x) = join_results (Future.join x);
+
 local
 
 structure Result = Proof_Data
 (
-  type T = (transition * state) list future;
-  val empty: T = Future.value [];
+  type T = result;
+  val empty: T = Result_List [];
   fun init _ = empty;
 );
 
-fun done_proof state =
-  if can (Proof.assert_bottom true) state
-  then Proof.global_done_proof state
-  else Proof.context_of (Proof.local_done_proof state);
+val get_result = Result.get o Proof.context_of;
+val put_result = Proof.map_context o Result.put;
 
 fun proof_future_enabled st =
   (case try proof_of st of
@@ -744,46 +752,52 @@
           (Goal.fork_name "Toplevel.diag" (priority (Thy_Syntax.atom tr))
             (fn () => command tr st); st)) ()
       else command tr st;
-  in ((tr, st'), st') end;
+  in (Result (tr, st'), st') end;
 
 in
 
-fun element_result (Thy_Syntax.Element (tr, NONE)) st =
-      let val (result, st') = atom_result tr st
-      in (Future.value [result], st') end
-  | element_result (Thy_Syntax.Element (head_tr, SOME proof)) st =
+fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
+  | element_result (Thy_Syntax.Element (head_tr, SOME element_rest)) st =
       let
         val (head_result, st') = atom_result head_tr st;
-        val (body_elems, end_tr) = proof;
-        val body_trs = maps Thy_Syntax.flat_element body_elems;
+        val (body_elems, end_tr) = element_rest;
       in
         if not (proof_future_enabled st')
         then
-          let val (proof_results, st'') = fold_map atom_result (body_trs @ [end_tr]) st'
-          in (Future.value (head_result :: proof_results), st'') end
+          let
+            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
+            val (proof_results, st'') = fold_map atom_result proof_trs st';
+          in (Result_List (head_result :: proof_results), st'') end
         else
           let
             val finish = Context.Theory o Proof_Context.theory_of;
 
             val future_proof = Proof.future_proof
-              (fn prf =>
+              (fn state =>
                 setmp_thread_position head_tr (fn () =>
                   Goal.fork_name "Toplevel.future_proof"
-                    (priority (Thy_Syntax.Element (empty, SOME proof)))
+                    (priority (Thy_Syntax.Element (empty, SOME element_rest)))
                     (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 atom_result body_trs ||> command end_tr;
-                      in (result, presentation_context_of result_state) end)) ())
-              #> (fn (result, state') => state' |> done_proof |> Result.put result);
+                      let
+                        val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st';
+                        val prf' = Proof_Node.apply (K state) prf;
+                        val (result, result_state) =
+                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
+                          |> fold_map element_result body_elems ||> command end_tr;
+                      in (Result_List result, presentation_context_of result_state) end)) ())
+              #> (fn (res, state') => state' |> put_result (Result_Future res));
+
+            val forked_proof =
+              proof (future_proof #>
+                (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o
+              end_proof (fn _ => future_proof #>
+                (fn state => state |> Proof.global_done_proof |> Result.put (get_result state)));
 
             val st'' = st'
-              |> command (head_tr |> set_print false |> reset_trans |> end_proof (K future_proof));
+              |> command (head_tr |> set_print false |> reset_trans |> forked_proof);
+            val end_result = Result (end_tr, st'');
             val result =
-              Result.get (presentation_context_of st'')
-              |> Future.map (fn body_results => head_result :: body_results @ [(end_tr, st'')]);
-
+              Result_List [head_result, Result.get (presentation_context_of st''), end_result];
           in (result, st'') end
       end;
 
diff -r e7fab0b5dbe7 -r 8707df0b0255 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Mar 04 11:36:16 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Mar 04 15:03:46 2013 +0100
@@ -242,7 +242,7 @@
         Multithreading.max_threads := Options.int options "threads";
         if Multithreading.max_threads_value () < 2
         then Multithreading.max_threads := 2 else ();
-        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 4 else 0);
+        Goal.parallel_proofs := (if Options.int options "parallel_proofs" > 0 then 3 else 0);
         Goal.parallel_proofs_threshold := Options.int options "parallel_proofs_threshold";
         tracing_messages := Options.int options "editor_tracing_messages"
       end);
diff -r e7fab0b5dbe7 -r 8707df0b0255 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Mon Mar 04 11:36:16 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Mon Mar 04 15:03:46 2013 +0100
@@ -260,7 +260,7 @@
 
     fun present () =
       let
-        val res = filter_out (Toplevel.is_ignored o #1) (flat (Future.joins results));
+        val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
         val ((minor, _), outer_syntax) = Outer_Syntax.get_syntax ();
       in
         Thy_Output.present_thy minor Keyword.command_tags