src/Pure/Thy/thy_info.ML
changeset 30319 a549dc15c037
parent 29437 a96236886804
child 30819 17bd1cf53d8e
equal deleted inserted replaced
30318:3d03190d2864 30319:a549dc15c037
   381 
   381 
   382   in ignore (Exn.release_all (map Exn.Exn (rev exns))) end;
   382   in ignore (Exn.release_all (map Exn.Exn (rev exns))) end;
   383 
   383 
   384 fun schedule_seq tasks =
   384 fun schedule_seq tasks =
   385   Graph.topological_order tasks
   385   Graph.topological_order tasks
   386   |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () () | _ => ()));
   386   |> List.app (fn name =>
       
   387     (case Graph.get_node tasks name of
       
   388       Task body =>
       
   389         let val after_load = body ()
       
   390         in after_load () handle exn => (kill_thy name; raise exn) end
       
   391     | _ => ()));
   387 
   392 
   388 in
   393 in
   389 
   394 
   390 fun schedule_tasks tasks n =
   395 fun schedule_tasks tasks n =
   391   if not (Multithreading.enabled ()) then schedule_seq tasks
   396   if not (Multithreading.enabled ()) then schedule_seq tasks