# HG changeset patch
# User wenzelm
# Date 1362387778 -3600
# Node ID f249bd08d851841c3eeb67c579cc73130825af4c
# Parent  a75040aaf369b60e44a601740bf62ae1629abf00
more explicit datatype result;

diff -r a75040aaf369 -r f249bd08d851 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Mar 03 18:50:46 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Mon Mar 04 10:02:58 2013 +0100
@@ -164,7 +164,11 @@
 
 (* scheduling loader tasks *)
 
-type result = theory * serial * unit future * (unit -> unit);
+datatype result =
+  Result of {theory: theory, id: serial, present: unit future, commit: unit -> unit};
+
+fun result_theory (Result {theory, ...}) = theory;
+fun theory_result theory = Result {theory = theory, id = 0, present = Future.value (), commit = I};
 
 datatype task =
   Task of string list * (theory list -> result) |
@@ -177,14 +181,14 @@
 
 local
 
-fun finish_thy ((thy, id, present, commit): result) =
+fun finish_thy (Result {theory, id, present, commit}) =
   let
-    val result1 = Exn.capture Thm.join_theory_proofs thy;
+    val result1 = Exn.capture Thm.join_theory_proofs theory;
     val results2 = Future.join_results (Goal.peek_futures id);
     val result3 = Future.join_result present;
     val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
     val _ = commit ();
-  in thy end;
+  in theory end;
 
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
@@ -203,11 +207,11 @@
                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
               (fn () =>
                 (case filter (not o can Future.join o #2) deps of
-                  [] => body (map (#1 o Future.join) (task_parents deps parents))
+                  [] => body (map (result_theory o Future.join) (task_parents deps parents))
                 | bad =>
                     error (loader_msg ("failed to load " ^ quote name ^
                       " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
-        | Finished thy => Future.value (thy, 0, Future.value (), I)))
+        | Finished theory => Future.value (theory_result theory)))
       |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
 
     (* FIXME avoid global reset_futures (!??) *)
@@ -253,7 +257,7 @@
       Thy_Load.load_thy last_timing update_time dir header text_pos text
         (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
     fun commit () = update_thy deps theory;
-  in (theory, id, present, commit) end;
+  in Result {theory = theory, id = id, present = present, commit = commit} end;
 
 fun check_deps dir name =
   (case lookup_deps name of