changeset 30319 | a549dc15c037 |
parent 29437 | a96236886804 |
child 30819 | 17bd1cf53d8e |
--- 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