author | wenzelm |
Fri, 06 Mar 2009 22:47:32 +0100 | |
changeset 30319 | a549dc15c037 |
parent 30318 | 3d03190d2864 |
child 30320 | 5f859035331f |
--- 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