# HG changeset patch
# User wenzelm
# Date 1236376052 -3600
# Node ID a549dc15c037e6931201febb592d71de1531bc03
# Parent  3d03190d28642aa6e49aa8d92d4641e558a96a90
schedule_seq: handle after_load errors as in schedule_futures;

diff -r 3d03190d2864 -r a549dc15c037 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