--- a/src/Pure/Concurrent/future.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/Concurrent/future.ML Sat Dec 06 12:18:05 2008 +0100
@@ -36,6 +36,7 @@
val group_of: 'a future -> group
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
+ val value: 'a -> 'a future
val fork: (unit -> 'a) -> 'a future
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
@@ -84,6 +85,11 @@
fun peek (Future {result, ...}) = ! result;
fun is_finished x = is_some (peek x);
+fun value x = Future
+ {task = TaskQueue.new_task (),
+ group = TaskQueue.new_group (),
+ result = ref (SOME (Exn.Result x))};
+
(** scheduling **)
--- a/src/Pure/Concurrent/task_queue.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Sat Dec 06 12:18:05 2008 +0100
@@ -8,6 +8,7 @@
signature TASK_QUEUE =
sig
eqtype task
+ val new_task: unit -> task
val str_of_task: task -> string
eqtype group
val new_group: unit -> group
@@ -34,8 +35,11 @@
(* identifiers *)
datatype task = Task of serial;
+fun new_task () = Task (serial ());
+
fun str_of_task (Task i) = string_of_int i;
+
datatype group = Group of serial * bool ref;
fun new_group () = Group (serial (), ref true);
@@ -81,8 +85,7 @@
fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
let
- val id = serial ();
- val task = Task id;
+ val task as Task id = new_task ();
val groups' = Inttab.cons_list (gid, task) groups;
val jobs' = jobs
|> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;
--- a/src/Pure/Isar/toplevel.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML Sat Dec 06 12:18:05 2008 +0100
@@ -744,7 +744,7 @@
val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
val _ =
(case end_state of
- State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
+ State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
| _ => error "Unfinished development at end of input");
val results = maps Lazy.force future_results;
in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
--- a/src/Pure/Thy/thy_info.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Dec 06 12:18:05 2008 +0100
@@ -322,11 +322,22 @@
fun future (name, body) tab =
let
- val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
- val x = Future.fork_deps deps body;
+ val deps = Graph.imm_preds task_graph name
+ |> map_filter (fn parent =>
+ (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
+ fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
+
+ val x = Future.fork_deps (map #2 deps) (fn () =>
+ (case map_filter failed deps of
+ [] => body ()
+ | bad => error (loader_msg
+ ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+
in (x, Symtab.update (name, x) tab) end;
- val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
- in () end;
+
+ val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
+ val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
+ in ignore (Exn.release_all (thy_results @ proof_results)) end;
local
--- a/src/Pure/context.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/context.ML Sat Dec 06 12:18:05 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/context.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generic theory contexts with unique identity, arbitrarily typed data,
@@ -392,14 +391,11 @@
fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
let
- val {name, version, intermediates} = history_of thy;
- val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
- val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
- val identity' = make_identity self id ids Inttab.empty;
+ val {name, ...} = history_of thy;
+ val Theory (identity', data', ancestry', _) = name_thy name thy;
val history' = make_history name 0 [];
- val thy'' = vitalize (Theory (identity', data', ancestry', history'));
- val _ = List.app (fn r => r := thy'') rs;
- in thy'' end);
+ val thy' = vitalize (Theory (identity', data', ancestry', history'));
+ in thy' end);
(* theory data *)
--- a/src/Pure/pure_thy.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/pure_thy.ML Sat Dec 06 12:18:05 2008 +0100
@@ -11,7 +11,7 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val force_proofs: theory -> unit
+ val join_proofs: theory list -> unit Exn.result list
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
@@ -79,10 +79,9 @@
(* proofs *)
-fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
+fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
-fun force_proofs thy =
- ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
+val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
--- a/src/Pure/thm.ML Sat Dec 06 08:57:39 2008 +0100
+++ b/src/Pure/thm.ML Sat Dec 06 12:18:05 2008 +0100
@@ -149,7 +149,7 @@
val future: thm future -> cterm -> thm
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
- val force_proof: thm -> unit
+ val join_proof: thm -> unit
val extern_oracles: theory -> xstring list
val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
@@ -1638,7 +1638,7 @@
in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
val proof_of = Proofterm.proof_of o proof_body_of;
-val force_proof = ignore o proof_body_of;
+val join_proof = ignore o proof_body_of;
(* closed derivations with official name *)