deps: keep thy source text, avoid reloading;
authorwenzelm
Sun Jul 29 22:42:02 2007 +0200 (2007-07-29)
changeset 24068245b7e68a3bc
parent 24067 69b51bc5ce06
child 24069 8a15a04e36f6
deps: keep thy source text, avoid reloading;
schedule: pick the first task with maximal imm_succs;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jul 29 22:42:00 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jul 29 22:42:02 2007 +0200
     1.3 @@ -94,15 +94,16 @@
     1.4  type deps =
     1.5    {outdated: bool,              (*entry considered outdated*)
     1.6      master: master option,      (*master dependencies for thy + attached ML file*)
     1.7 +    text: string list,          (*source text for thy*)
     1.8      parents: string list,       (*source specification of parents (partially qualified)*)
     1.9      files:                      (*auxiliary files: source path, physical path + identifier*)
    1.10        (Path.T * (Path.T * File.ident) option) list};
    1.11  
    1.12 -fun make_deps outdated master parents files : deps =
    1.13 -  {outdated = outdated, master = master, parents = parents, files = files};
    1.14 +fun make_deps outdated master text parents files : deps =
    1.15 +  {outdated = outdated, master = master, text = text, parents = parents, files = files};
    1.16  
    1.17 -fun init_deps master parents files =
    1.18 -  SOME (make_deps true master parents (map (rpair NONE) files));
    1.19 +fun init_deps master text parents files =
    1.20 +  SOME (make_deps true master text parents (map (rpair NONE) files));
    1.21  
    1.22  fun master_idents (NONE: master option) = []
    1.23    | master_idents (SOME ((_, thy_id), NONE)) = [thy_id]
    1.24 @@ -159,7 +160,6 @@
    1.25  fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
    1.26  
    1.27  fun is_finished name = is_none (get_deps name);
    1.28 -fun get_files name = (case get_deps name of SOME {files, ...} => files | _ => []);
    1.29  
    1.30  fun loaded_files name =
    1.31    (case get_deps name of
    1.32 @@ -229,8 +229,8 @@
    1.33  fun outdate_thy name =
    1.34    if is_finished name orelse is_outdated name then ()
    1.35    else CRITICAL (fn () =>
    1.36 -   (change_deps name (Option.map (fn {outdated = _, master, parents, files} =>
    1.37 -    make_deps true master parents files)); perform Outdate name));
    1.38 +   (change_deps name (Option.map (fn {outdated = _, master, text, parents, files} =>
    1.39 +    make_deps true master text parents files)); perform Outdate name));
    1.40  
    1.41  fun check_unfinished name =
    1.42    if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE)
    1.43 @@ -261,11 +261,11 @@
    1.44  
    1.45  local
    1.46  
    1.47 -fun provide path name info (deps as SOME {outdated, master, parents, files}) =
    1.48 +fun provide path name info (deps as SOME {outdated, master, text, parents, files}) =
    1.49       (if AList.defined (op =) files path then ()
    1.50        else warning (loader_msg "undeclared dependency of theory" [name] ^
    1.51          " on file: " ^ quote (Path.implode path));
    1.52 -      SOME (make_deps outdated master parents (AList.update (op =) (path, SOME info) files)))
    1.53 +      SOME (make_deps outdated master text parents (AList.update (op =) (path, SOME info) files)))
    1.54    | provide _ _ _ NONE = NONE;
    1.55  
    1.56  fun run_file path =
    1.57 @@ -306,20 +306,27 @@
    1.58        if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators)
    1.59        else priority ("Registering theory " ^ quote name);
    1.60  
    1.61 -    val _ = touch_thy name;
    1.62 -    val master =
    1.63 -      if really then ThyLoad.load_thy dir name ml (time orelse ! Output.timing)
    1.64 -      else #1 (ThyLoad.deps_thy dir name ml);
    1.65 +    val (master_path, text, files) =
    1.66 +      (case get_deps name of
    1.67 +        SOME {master = SOME ((master_path, _), _), text = text as _ :: _, files, ...} =>
    1.68 +          (master_path, text, files)
    1.69 +      | _ => error (loader_msg "corrupted dependency information" [name]));
    1.70  
    1.71 -    val files = get_files name;
    1.72 +    val _ = touch_thy name;
    1.73 +    val _ =
    1.74 +      if really then
    1.75 +        ThyLoad.load_thy dir name (Position.path master_path) text ml (time orelse ! Output.timing)
    1.76 +      else ();
    1.77 +
    1.78      val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
    1.79 +    val _ =
    1.80 +      if null missing_files then ()
    1.81 +      else warning (loader_msg "unresolved dependencies of theory" [name] ^
    1.82 +        " on file(s): " ^ commas_quote missing_files);
    1.83    in
    1.84 -    if null missing_files then ()
    1.85 -    else warning (loader_msg "unresolved dependencies of theory" [name] ^
    1.86 -      " on file(s): " ^ commas_quote missing_files);
    1.87      CRITICAL (fn () =>
    1.88       (change_deps name
    1.89 -        (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files));
    1.90 +        (Option.map (fn {master, parents, files, ...} => make_deps false master [] parents files));
    1.91        perform Update name))
    1.92    end;
    1.93  
    1.94 @@ -340,21 +347,22 @@
    1.95    (case lookup_deps name of
    1.96      SOME NONE => (true, NONE, get_parents name)
    1.97    | NONE =>
    1.98 -      let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml
    1.99 -      in (false, init_deps (SOME master) parents files, parents) end
   1.100 -  | SOME (deps as SOME {outdated, master, parents, files}) =>
   1.101 +      let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name ml
   1.102 +      in (false, init_deps (SOME master) text parents files, parents) end
   1.103 +  | SOME (deps as SOME {outdated, master, text, parents, files}) =>
   1.104        if not strict andalso can get_theory name then (true, deps, parents)
   1.105        else
   1.106          let val master' = SOME (ThyLoad.check_thy dir name ml) in
   1.107            if master_idents master <> master_idents master'
   1.108            then
   1.109 -            let val (parents', files') = #2 (ThyLoad.deps_thy dir name ml)
   1.110 -            in (false, init_deps master' parents' files', parents') end
   1.111 +            let val {text = text', imports = parents', uses = files', ...} =
   1.112 +              ThyLoad.deps_thy dir name ml;
   1.113 +            in (false, init_deps master' text' parents' files', parents') end
   1.114            else
   1.115              let
   1.116                val checked_files = map (check_ml master') files;
   1.117                val current = not outdated andalso forall (is_some o snd) checked_files;
   1.118 -              val deps' = SOME (make_deps (not current) master' parents checked_files);
   1.119 +              val deps' = SOME (make_deps (not current) master' text parents checked_files);
   1.120              in (current, deps', parents) end
   1.121          end);
   1.122  
   1.123 @@ -406,17 +414,23 @@
   1.124    Graph.topological_order tasks
   1.125    |> List.app (fn name => (case Graph.get_node tasks name of Task.Task f => f () | _ => ()));
   1.126  
   1.127 +fun max_task (task as (_, (Task.Task _, _))) NONE = SOME task
   1.128 +  | max_task (task as (_, (Task.Task _, m))) (task' as SOME (_, (_, m'))) =
   1.129 +      if m > m' then SOME task else task'
   1.130 +  | max_task _ task' = task';
   1.131 +
   1.132  fun next_task G =
   1.133    let
   1.134 -    val tasks = map (fn name => (name, Graph.get_node G name)) (Graph.minimals G);
   1.135 -    val finished = filter (Task.is_finished o snd) tasks;
   1.136 +    val tasks = Graph.minimals G |> map (fn name =>
   1.137 +      (name, (Graph.get_node G name, length (Graph.imm_succs G name))))
   1.138 +    val finished = filter (Task.is_finished o fst o snd) tasks;
   1.139    in
   1.140      if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
   1.141      else if null tasks then ((Task.Finished, I), G)
   1.142      else
   1.143 -      (case find_first (not o Task.is_running o snd) tasks of
   1.144 +      (case fold max_task tasks NONE of
   1.145          NONE => ((Task.Running, I), G)
   1.146 -      | SOME (name, task) =>
   1.147 +      | SOME (name, (task, _)) =>
   1.148            ((task, Graph.del_nodes [name]), Graph.map_node name (K Task.Running) G))
   1.149    end;
   1.150  
   1.151 @@ -492,7 +506,7 @@
   1.152  
   1.153      val deps =
   1.154        if known_thy name then get_deps name
   1.155 -      else init_deps NONE parents (map #1 uses);
   1.156 +      else init_deps NONE [] parents (map #1 uses);
   1.157      val _ = change_thys (new_deps name parent_names (deps, NONE));
   1.158  
   1.159      val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;