src/Pure/Thy/thy_info.ML
changeset 28445 526b8adcd117
parent 28435 97de495414e8
child 28449 b6c57eb0fc39
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Oct 01 12:00:04 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Oct 01 12:00:05 2008 +0200
     1.3 @@ -320,19 +320,17 @@
     1.4      val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
     1.5        (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
     1.6  
     1.7 -    val group = TaskQueue.new_group ();
     1.8      fun future (name, body) tab =
     1.9        let
    1.10 +        val group = TaskQueue.new_group ();
    1.11          val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
    1.12          val x = Future.future (SOME group) deps true body;
    1.13        in (x, Symtab.update (name, Future.task_of x) tab) end;
    1.14 -
    1.15 -    val exns = #1 (fold_map future tasks Symtab.empty)
    1.16 -      |> uninterruptible (fn _ => Future.join_results)
    1.17 -      |> map_filter Exn.get_exn;
    1.18    in
    1.19 -    if null exns then ()
    1.20 -    else raise Exn.EXCEPTIONS (exns, "")
    1.21 +    #1 (fold_map future tasks Symtab.empty)
    1.22 +    |> uninterruptible (fn _ => Future.join_results)
    1.23 +    |> Exn.release_all
    1.24 +    |> ignore
    1.25    end;
    1.26  
    1.27  local
    1.28 @@ -372,10 +370,7 @@
    1.29       (warning (loader_msg "no multithreading within critical section" []);
    1.30        schedule_seq tasks)
    1.31      else if ! future_scheduler then future_schedule tasks
    1.32 -    else
    1.33 -      (case Schedule.schedule (Int.min (m, n)) next_task tasks of
    1.34 -        [] => ()
    1.35 -      | exns => raise Exn.EXCEPTIONS (exns, ""))
    1.36 +    else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
    1.37    end;
    1.38  
    1.39  end;