# HG changeset patch
# User wenzelm
# Date 1228562285 -3600
# Node ID 3ad09b8d2534ae0927126d54349fb0930bf1508f
# Parent  d863c103ded071102139c52576e02a9e598c1a63# Parent  d8d3cbbb6fcc17f9fdf1e82e5a9e9baa2e86110f
merged

diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/Concurrent/future.ML
--- 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 **)
diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/Concurrent/task_queue.ML
--- 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;
diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/Isar/toplevel.ML
--- 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);
diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/Thy/thy_info.ML
--- 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
 
diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/context.ML
--- 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 *)
diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/pure_thy.ML
--- 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))));
 
 
 
diff -r d863c103ded0 -r 3ad09b8d2534 src/Pure/thm.ML
--- 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 *)