1.1 --- a/src/Pure/Concurrent/future.ML	Sat Dec 06 08:57:39 2008 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Sat Dec 06 12:18:05 2008 +0100
     1.3 @@ -36,6 +36,7 @@
     1.4    val group_of: 'a future -> group
     1.5    val peek: 'a future -> 'a Exn.result option
     1.6    val is_finished: 'a future -> bool
     1.7 +  val value: 'a -> 'a future
     1.8    val fork: (unit -> 'a) -> 'a future
     1.9    val fork_group: group -> (unit -> 'a) -> 'a future
    1.10    val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
    1.11 @@ -84,6 +85,11 @@
    1.12  fun peek (Future {result, ...}) = ! result;
    1.13  fun is_finished x = is_some (peek x);
    1.14  
    1.15 +fun value x = Future
    1.16 + {task = TaskQueue.new_task (),
    1.17 +  group = TaskQueue.new_group (),
    1.18 +  result = ref (SOME (Exn.Result x))};
    1.19 +
    1.20  
    1.21  
    1.22  (** scheduling **)

     2.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 08:57:39 2008 +0100
     2.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Dec 06 12:18:05 2008 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  signature TASK_QUEUE =
     2.5  sig
     2.6    eqtype task
     2.7 +  val new_task: unit -> task
     2.8    val str_of_task: task -> string
     2.9    eqtype group
    2.10    val new_group: unit -> group
    2.11 @@ -34,8 +35,11 @@
    2.12  (* identifiers *)
    2.13  
    2.14  datatype task = Task of serial;
    2.15 +fun new_task () = Task (serial ());
    2.16 +
    2.17  fun str_of_task (Task i) = string_of_int i;
    2.18  
    2.19 +
    2.20  datatype group = Group of serial * bool ref;
    2.21  
    2.22  fun new_group () = Group (serial (), ref true);
    2.23 @@ -81,8 +85,7 @@
    2.24  
    2.25  fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
    2.26    let
    2.27 -    val id = serial ();
    2.28 -    val task = Task id;
    2.29 +    val task as Task id = new_task ();
    2.30      val groups' = Inttab.cons_list (gid, task) groups;
    2.31      val jobs' = jobs
    2.32        |> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;

     3.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 06 08:57:39 2008 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Dec 06 12:18:05 2008 +0100
     3.3 @@ -744,7 +744,7 @@
     3.4      val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
     3.5      val _ =
     3.6        (case end_state of
     3.7 -        State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
     3.8 +        State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
     3.9        | _ => error "Unfinished development at end of input");
    3.10      val results = maps Lazy.force future_results;
    3.11    in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);

     4.1 --- a/src/Pure/Thy/thy_info.ML	Sat Dec 06 08:57:39 2008 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Dec 06 12:18:05 2008 +0100
     4.3 @@ -322,11 +322,22 @@
     4.4  
     4.5      fun future (name, body) tab =
     4.6        let
     4.7 -        val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
     4.8 -        val x = Future.fork_deps deps body;
     4.9 +        val deps = Graph.imm_preds task_graph name
    4.10 +          |> map_filter (fn parent =>
    4.11 +            (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
    4.12 +        fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
    4.13 +
    4.14 +        val x = Future.fork_deps (map #2 deps) (fn () =>
    4.15 +          (case map_filter failed deps of
    4.16 +            [] => body ()
    4.17 +          | bad => error (loader_msg
    4.18 +              ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
    4.19 +
    4.20        in (x, Symtab.update (name, x) tab) end;
    4.21 -    val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
    4.22 -  in () end;
    4.23 +
    4.24 +    val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
    4.25 +    val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
    4.26 +  in ignore (Exn.release_all (thy_results @ proof_results)) end;
    4.27  
    4.28  local
    4.29  

     5.1 --- a/src/Pure/context.ML	Sat Dec 06 08:57:39 2008 +0100
     5.2 +++ b/src/Pure/context.ML	Sat Dec 06 12:18:05 2008 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      Pure/context.ML
     5.5 -    ID:         $Id$
     5.6      Author:     Markus Wenzel, TU Muenchen
     5.7  
     5.8  Generic theory contexts with unique identity, arbitrarily typed data,
     5.9 @@ -392,14 +391,11 @@
    5.10  
    5.11  fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
    5.12    let
    5.13 -    val {name, version, intermediates} = history_of thy;
    5.14 -    val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
    5.15 -    val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
    5.16 -    val identity' = make_identity self id ids Inttab.empty;
    5.17 +    val {name, ...} = history_of thy;
    5.18 +    val Theory (identity', data', ancestry', _) = name_thy name thy;
    5.19      val history' = make_history name 0 [];
    5.20 -    val thy'' = vitalize (Theory (identity', data', ancestry', history'));
    5.21 -    val _ = List.app (fn r => r := thy'') rs;
    5.22 -  in thy'' end);
    5.23 +    val thy' = vitalize (Theory (identity', data', ancestry', history'));
    5.24 +  in thy' end);
    5.25  
    5.26  
    5.27  (* theory data *)

     6.1 --- a/src/Pure/pure_thy.ML	Sat Dec 06 08:57:39 2008 +0100
     6.2 +++ b/src/Pure/pure_thy.ML	Sat Dec 06 12:18:05 2008 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4    val intern_fact: theory -> xstring -> string
     6.5    val defined_fact: theory -> string -> bool
     6.6    val hide_fact: bool -> string -> theory -> theory
     6.7 -  val force_proofs: theory -> unit
     6.8 +  val join_proofs: theory list -> unit Exn.result list
     6.9    val get_fact: Context.generic -> theory -> Facts.ref -> thm list
    6.10    val get_thms: theory -> xstring -> thm list
    6.11    val get_thm: theory -> xstring -> thm
    6.12 @@ -79,10 +79,9 @@
    6.13  
    6.14  (* proofs *)
    6.15  
    6.16 -fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
    6.17 +fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
    6.18  
    6.19 -fun force_proofs thy =
    6.20 -  ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
    6.21 +val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
    6.22  
    6.23  
    6.24  

     7.1 --- a/src/Pure/thm.ML	Sat Dec 06 08:57:39 2008 +0100
     7.2 +++ b/src/Pure/thm.ML	Sat Dec 06 12:18:05 2008 +0100
     7.3 @@ -149,7 +149,7 @@
     7.4    val future: thm future -> cterm -> thm
     7.5    val proof_body_of: thm -> proof_body
     7.6    val proof_of: thm -> proof
     7.7 -  val force_proof: thm -> unit
     7.8 +  val join_proof: thm -> unit
     7.9    val extern_oracles: theory -> xstring list
    7.10    val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
    7.11  end;
    7.12 @@ -1638,7 +1638,7 @@
    7.13    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    7.14  
    7.15  val proof_of = Proofterm.proof_of o proof_body_of;
    7.16 -val force_proof = ignore o proof_body_of;
    7.17 +val join_proof = ignore o proof_body_of;
    7.18  
    7.19  
    7.20  (* closed derivations with official name *)