src/Pure/Thy/thy_info.ML
changeset 44247 270366301bd7
parent 44225 a8f921e6484f
child 44302 0a1934c5c104
equal deleted inserted replaced
44246:380a4677c55d 44247:270366301bd7
   205             | bad =>
   205             | bad =>
   206                 error (loader_msg ("failed to load " ^ quote name ^
   206                 error (loader_msg ("failed to load " ^ quote name ^
   207                   " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
   207                   " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
   208     | Finished thy => Future.value (thy, Future.value (), I)))
   208     | Finished thy => Future.value (thy, Future.value (), I)))
   209   #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
   209   #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
   210   #> rev #> Exn.release_all) #> ignore;
   210   #> rev #> Par_Exn.release_all) #> ignore;
   211 
   211 
   212 in
   212 in
   213 
   213 
   214 fun schedule_tasks tasks =
   214 fun schedule_tasks tasks =
   215   if not (Multithreading.enabled ()) then schedule_seq tasks
   215   if not (Multithreading.enabled ()) then schedule_seq tasks