1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Jul 24 22:53:48 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Jul 24 22:53:49 2007 +0200
     1.3 @@ -362,18 +362,18 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun require_thys really ml time strict keep_strict initiators dir strs tasks_visited =
     1.8 -  fold_map (require_thy really ml time strict keep_strict initiators dir) strs tasks_visited
     1.9 +fun require_thys really ml time strict keep_strict initiators dir strs tasks =
    1.10 +  fold_map (require_thy really ml time strict keep_strict initiators dir) strs tasks
    1.11    |>> forall I
    1.12 -and require_thy really ml time strict keep_strict initiators dir str (tasks, visited) =
    1.13 +and require_thy really ml time strict keep_strict initiators dir str tasks =
    1.14    let
    1.15      val path = Path.expand (Path.explode str);
    1.16      val name = Path.implode (Path.base path);
    1.17      val dir' = Path.append dir (Path.dir path);
    1.18      val _ = member (op =) initiators name andalso error (cycle_msg initiators);
    1.19    in
    1.20 -    (case AList.lookup (op =) visited name of
    1.21 -      SOME current => (current, (tasks, visited))
    1.22 +    (case try (Graph.get_node (fst tasks)) name of
    1.23 +      SOME task => (is_none task, tasks)
    1.24      | NONE =>
    1.25          let
    1.26            val (current, deps, parents) = check_deps ml strict dir' name
    1.27 @@ -382,42 +382,53 @@
    1.28                  required_by "\n" initiators);
    1.29            val parent_names = map base_name parents;
    1.30  
    1.31 -          val (parents_current, (tasks', visited')) =
    1.32 +          val (parents_current, (tasks_graph', tasks_len')) =
    1.33              require_thys true true time (strict andalso keep_strict) keep_strict
    1.34 -              (name :: initiators) (Path.append dir (master_dir' deps))
    1.35 -              parents (tasks, visited);
    1.36 +              (name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
    1.37  
    1.38            val all_current = current andalso parents_current;
    1.39            val thy = if all_current orelse not really then SOME (get_theory name) else NONE;
    1.40            val _ = change_thys (new_deps name parent_names (deps, thy));
    1.41  
    1.42 -          val tasks'' = tasks' |> new_deps name parent_names
    1.43 -            (fn () => if all_current then () else load_thy really ml time initiators dir' name);
    1.44 -          val visited'' = (name, all_current) :: visited';
    1.45 -        in (all_current, (tasks'', visited'')) end)
    1.46 +          val tasks_graph'' = tasks_graph' |> new_deps name parent_names
    1.47 +           (if all_current then NONE
    1.48 +            else SOME (fn () => load_thy really ml time initiators dir' name));
    1.49 +          val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
    1.50 +        in (all_current, (tasks_graph'', tasks_len'')) end)
    1.51    end;
    1.52  
    1.53  end;
    1.54  
    1.55  
    1.56 -(* variations on use_thy *)
    1.57 +(* use_thy etc. -- scheduling required theories *)
    1.58  
    1.59  local
    1.60  
    1.61  fun schedule_seq tasks =
    1.62 -  Graph.topological_order tasks |> List.app (fn name => Graph.get_node tasks name ());
    1.63 +  Graph.topological_order tasks
    1.64 +  |> List.app (fn name => the_default I (Graph.get_node tasks name) ());
    1.65  
    1.66 -fun schedule_tasks tasks =
    1.67 -  let val m = ! Multithreading.number_of_threads in
    1.68 -    if m <= 1 then schedule_seq tasks
    1.69 +fun next_task (SOME f :: fs, G) = (SOME f, (fs, G))
    1.70 +  | next_task (NONE :: fs, G) = next_task (fs, G)
    1.71 +  | next_task ([], G) =
    1.72 +      (case Graph.minimals G of
    1.73 +        [] => (NONE, ([], G))
    1.74 +      | ms => next_task (map (Graph.get_node G) ms, Graph.del_nodes ms G));
    1.75 +
    1.76 +fun schedule_tasks (tasks, n) =
    1.77 +  let val m = ! Multithreading.max_threads in
    1.78 +    if m <= 1 orelse n <= 1 then schedule_seq tasks
    1.79      else if Multithreading.self_critical () then
    1.80       (warning (loader_msg "no multithreading within critical section" []);
    1.81        schedule_seq tasks)
    1.82 -    else sys_error "No multithreading scheduler yet"
    1.83 +    else
    1.84 +      (case Multithreading.schedule (Int.min (m, n)) next_task ([], tasks) of
    1.85 +        [] => ()
    1.86 +      | exns => raise Exn.EXCEPTIONS (exns, ""))
    1.87    end;
    1.88  
    1.89  fun gen_use_thy' req dir arg = Output.toplevel_errors (fn () =>
    1.90 -  let val (_, (tasks, _)) = req [] dir arg (Graph.empty, [])
    1.91 +  let val (_, tasks) = req [] dir arg (Graph.empty, 0)
    1.92    in schedule_tasks tasks end) ();
    1.93  
    1.94  fun gen_use_thy req str =