# 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