more explicit datatype result;
authorwenzelm
Mon Mar 04 10:02:58 2013 +0100 (2013-03-04)
changeset 51330f249bd08d851
parent 51326 a75040aaf369
child 51331 e7fab0b5dbe7
more explicit datatype result;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sun Mar 03 18:50:46 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Mar 04 10:02:58 2013 +0100
     1.3 @@ -164,7 +164,11 @@
     1.4  
     1.5  (* scheduling loader tasks *)
     1.6  
     1.7 -type result = theory * serial * unit future * (unit -> unit);
     1.8 +datatype result =
     1.9 +  Result of {theory: theory, id: serial, present: unit future, commit: unit -> unit};
    1.10 +
    1.11 +fun result_theory (Result {theory, ...}) = theory;
    1.12 +fun theory_result theory = Result {theory = theory, id = 0, present = Future.value (), commit = I};
    1.13  
    1.14  datatype task =
    1.15    Task of string list * (theory list -> result) |
    1.16 @@ -177,14 +181,14 @@
    1.17  
    1.18  local
    1.19  
    1.20 -fun finish_thy ((thy, id, present, commit): result) =
    1.21 +fun finish_thy (Result {theory, id, present, commit}) =
    1.22    let
    1.23 -    val result1 = Exn.capture Thm.join_theory_proofs thy;
    1.24 +    val result1 = Exn.capture Thm.join_theory_proofs theory;
    1.25      val results2 = Future.join_results (Goal.peek_futures id);
    1.26      val result3 = Future.join_result present;
    1.27      val _ = Par_Exn.release_all (result1 :: results2 @ [result3]);
    1.28      val _ = commit ();
    1.29 -  in thy end;
    1.30 +  in theory end;
    1.31  
    1.32  val schedule_seq =
    1.33    String_Graph.schedule (fn deps => fn (_, task) =>
    1.34 @@ -203,11 +207,11 @@
    1.35                  deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
    1.36                (fn () =>
    1.37                  (case filter (not o can Future.join o #2) deps of
    1.38 -                  [] => body (map (#1 o Future.join) (task_parents deps parents))
    1.39 +                  [] => body (map (result_theory o Future.join) (task_parents deps parents))
    1.40                  | bad =>
    1.41                      error (loader_msg ("failed to load " ^ quote name ^
    1.42                        " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
    1.43 -        | Finished thy => Future.value (thy, 0, Future.value (), I)))
    1.44 +        | Finished theory => Future.value (theory_result theory)))
    1.45        |> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn]);
    1.46  
    1.47      (* FIXME avoid global reset_futures (!??) *)
    1.48 @@ -253,7 +257,7 @@
    1.49        Thy_Load.load_thy last_timing update_time dir header text_pos text
    1.50          (if name = Context.PureN then [ML_Context.the_global_context ()] else parents);
    1.51      fun commit () = update_thy deps theory;
    1.52 -  in (theory, id, present, commit) end;
    1.53 +  in Result {theory = theory, id = id, present = present, commit = commit} end;
    1.54  
    1.55  fun check_deps dir name =
    1.56    (case lookup_deps name of