tuned;
authorwenzelm
Mon, 07 Aug 2017 11:34:32 +0200
changeset 66368 26735fab7a8f
parent 66367 b60afdf1177d
child 66369 d003b44674c1
tuned;
src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Aug 07 11:20:19 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Aug 07 11:34:32 2017 +0200
@@ -169,8 +169,6 @@
 
 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
 
-local
-
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
@@ -222,13 +220,6 @@
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);
 
-in
-
-fun schedule_tasks tasks =
-  if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
-
-end;
-
 
 (* eval theory *)
 
@@ -403,7 +394,7 @@
   let
     val (_, tasks) =
       require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
-  in schedule_tasks tasks end;
+  in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
   use_theories