schedule_seq: handle after_load errors as in schedule_futures;
authorwenzelm
Fri, 06 Mar 2009 22:47:32 +0100
changeset 30319 a549dc15c037
parent 30318 3d03190d2864
child 30320 5f859035331f
schedule_seq: handle after_load errors as in schedule_futures;
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Mar 06 22:32:27 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Mar 06 22:47:32 2009 +0100
@@ -383,7 +383,12 @@
 
 fun schedule_seq tasks =
   Graph.topological_order tasks
-  |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ()));
+  |> List.app (fn name =>
+    (case Graph.get_node tasks name of
+      Task body =>
+        let val after_load = body ()
+        in after_load () handle exn => (kill_thy name; raise exn) end
+    | _ => ()));
 
 in