# HG changeset patch # User wenzelm # Date 1185741722 -7200 # Node ID 245b7e68a3bc91ed78681659e7859fe5e3949c83 # Parent 69b51bc5ce06f126404ed069a3863d961cc822c6 deps: keep thy source text, avoid reloading; schedule: pick the first task with maximal imm_succs; diff -r 69b51bc5ce06 -r 245b7e68a3bc src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Jul 29 22:42:00 2007 +0200 +++ b/src/Pure/Thy/thy_info.ML Sun Jul 29 22:42:02 2007 +0200 @@ -94,15 +94,16 @@ type deps = {outdated: bool, (*entry considered outdated*) master: master option, (*master dependencies for thy + attached ML file*) + text: string list, (*source text for thy*) parents: string list, (*source specification of parents (partially qualified)*) files: (*auxiliary files: source path, physical path + identifier*) (Path.T * (Path.T * File.ident) option) list}; -fun make_deps outdated master parents files : deps = - {outdated = outdated, master = master, parents = parents, files = files}; +fun make_deps outdated master text parents files : deps = + {outdated = outdated, master = master, text = text, parents = parents, files = files}; -fun init_deps master parents files = - SOME (make_deps true master parents (map (rpair NONE) files)); +fun init_deps master text parents files = + SOME (make_deps true master text parents (map (rpair NONE) files)); fun master_idents (NONE: master option) = [] | master_idents (SOME ((_, thy_id), NONE)) = [thy_id] @@ -159,7 +160,6 @@ fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x)); fun is_finished name = is_none (get_deps name); -fun get_files name = (case get_deps name of SOME {files, ...} => files | _ => []); fun loaded_files name = (case get_deps name of @@ -229,8 +229,8 @@ fun outdate_thy name = if is_finished name orelse is_outdated name then () else CRITICAL (fn () => - (change_deps name (Option.map (fn {outdated = _, master, parents, files} => - make_deps true master parents files)); perform Outdate name)); + (change_deps name (Option.map (fn {outdated = _, master, text, parents, files} => + make_deps true master text parents files)); perform Outdate name)); fun check_unfinished name = if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE) @@ -261,11 +261,11 @@ local -fun provide path name info (deps as SOME {outdated, master, parents, files}) = +fun provide path name info (deps as SOME {outdated, master, text, parents, files}) = (if AList.defined (op =) files path then () else warning (loader_msg "undeclared dependency of theory" [name] ^ " on file: " ^ quote (Path.implode path)); - SOME (make_deps outdated master parents (AList.update (op =) (path, SOME info) files))) + SOME (make_deps outdated master text parents (AList.update (op =) (path, SOME info) files))) | provide _ _ _ NONE = NONE; fun run_file path = @@ -306,20 +306,27 @@ if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators) else priority ("Registering theory " ^ quote name); - val _ = touch_thy name; - val master = - if really then ThyLoad.load_thy dir name ml (time orelse ! Output.timing) - else #1 (ThyLoad.deps_thy dir name ml); + val (master_path, text, files) = + (case get_deps name of + SOME {master = SOME ((master_path, _), _), text = text as _ :: _, files, ...} => + (master_path, text, files) + | _ => error (loader_msg "corrupted dependency information" [name])); - val files = get_files name; + val _ = touch_thy name; + val _ = + if really then + ThyLoad.load_thy dir name (Position.path master_path) text ml (time orelse ! Output.timing) + else (); + val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files; + val _ = + if null missing_files then () + else warning (loader_msg "unresolved dependencies of theory" [name] ^ + " on file(s): " ^ commas_quote missing_files); in - if null missing_files then () - else warning (loader_msg "unresolved dependencies of theory" [name] ^ - " on file(s): " ^ commas_quote missing_files); CRITICAL (fn () => (change_deps name - (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files)); + (Option.map (fn {master, parents, files, ...} => make_deps false master [] parents files)); perform Update name)) end; @@ -340,21 +347,22 @@ (case lookup_deps name of SOME NONE => (true, NONE, get_parents name) | NONE => - let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml - in (false, init_deps (SOME master) parents files, parents) end - | SOME (deps as SOME {outdated, master, parents, files}) => + let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name ml + in (false, init_deps (SOME master) text parents files, parents) end + | SOME (deps as SOME {outdated, master, text, parents, files}) => if not strict andalso can get_theory name then (true, deps, parents) else let val master' = SOME (ThyLoad.check_thy dir name ml) in if master_idents master <> master_idents master' then - let val (parents', files') = #2 (ThyLoad.deps_thy dir name ml) - in (false, init_deps master' parents' files', parents') end + let val {text = text', imports = parents', uses = files', ...} = + ThyLoad.deps_thy dir name ml; + in (false, init_deps master' text' parents' files', parents') end else let val checked_files = map (check_ml master') files; val current = not outdated andalso forall (is_some o snd) checked_files; - val deps' = SOME (make_deps (not current) master' parents checked_files); + val deps' = SOME (make_deps (not current) master' text parents checked_files); in (current, deps', parents) end end); @@ -406,17 +414,23 @@ Graph.topological_order tasks |> List.app (fn name => (case Graph.get_node tasks name of Task.Task f => f () | _ => ())); +fun max_task (task as (_, (Task.Task _, _))) NONE = SOME task + | max_task (task as (_, (Task.Task _, m))) (task' as SOME (_, (_, m'))) = + if m > m' then SOME task else task' + | max_task _ task' = task'; + fun next_task G = let - val tasks = map (fn name => (name, Graph.get_node G name)) (Graph.minimals G); - val finished = filter (Task.is_finished o snd) tasks; + val tasks = Graph.minimals G |> map (fn name => + (name, (Graph.get_node G name, length (Graph.imm_succs G name)))) + val finished = filter (Task.is_finished o fst o snd) tasks; in if not (null finished) then next_task (Graph.del_nodes (map fst finished) G) else if null tasks then ((Task.Finished, I), G) else - (case find_first (not o Task.is_running o snd) tasks of + (case fold max_task tasks NONE of NONE => ((Task.Running, I), G) - | SOME (name, task) => + | SOME (name, (task, _)) => ((task, Graph.del_nodes [name]), Graph.map_node name (K Task.Running) G)) end; @@ -492,7 +506,7 @@ val deps = if known_thy name then get_deps name - else init_deps NONE parents (map #1 uses); + else init_deps NONE [] parents (map #1 uses); val _ = change_thys (new_deps name parent_names (deps, NONE)); val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;