kill failed theories in reverse order -- avoids cascaded warnings;
authorwenzelm
Tue Jan 05 00:04:29 2010 +0100 (2010-01-05 ago)
changeset 342602524c1bbd087
parent 34259 2ba492b8b6e8
child 34261 8e36b3ac6083
child 34270 e45104d2d175
kill failed theories in reverse order -- avoids cascaded warnings;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Mon Jan 04 23:20:35 2010 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Jan 05 00:04:29 2010 +0100
     1.3 @@ -389,14 +389,16 @@
     1.4  
     1.5      val futures = fold fork tasks Symtab.empty;
     1.6  
     1.7 -    val exns = tasks |> maps (fn (name, _) =>
     1.8 +    val failed = tasks |> maps (fn (name, _) =>
     1.9        let
    1.10          val after_load = Future.join (the (Symtab.lookup futures name));
    1.11          val _ = join_thy name;
    1.12          val _ = after_load ();
    1.13 -      in [] end handle exn => (kill_thy name; [exn]));
    1.14 +      in [] end handle exn => [(name, exn)]) |> rev;
    1.15  
    1.16 -  in ignore (Exn.release_all (map Exn.Exn (rev exns))) end) ();
    1.17 +    val _ = List.app (kill_thy o #1) failed;
    1.18 +    val _ = Exn.release_all (map (Exn.Exn o #2) failed);
    1.19 +  in () end) ();
    1.20  
    1.21  fun schedule_seq tasks =
    1.22    Graph.topological_order tasks