1.1 --- a/src/Pure/Thy/thy_info.ML Tue Jul 31 00:56:32 2007 +0200
1.2 +++ b/src/Pure/Thy/thy_info.ML Tue Jul 31 00:56:34 2007 +0200
1.3 @@ -26,23 +26,23 @@
1.4 val lookup_theory: string -> theory option
1.5 val get_theory: string -> theory
1.6 val the_theory: string -> theory -> theory
1.7 + val loaded_files: string -> Path.T list
1.8 val get_parents: string -> string list
1.9 - val loaded_files: string -> Path.T list
1.10 + val pretty_theory: theory -> Pretty.T
1.11 val touch_child_thys: string -> unit
1.12 val touch_all_thys: unit -> unit
1.13 val load_file: bool -> Path.T -> unit
1.14 val use: string -> unit
1.15 val time_use: string -> unit
1.16 - val pretend_use_thy_only: string -> unit
1.17 val use_thys: string list -> unit
1.18 val use_thy: string -> unit
1.19 val time_use_thy: string -> unit
1.20 val update_thy: string -> unit
1.21 val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
1.22 val end_theory: theory -> theory
1.23 + val register_thy: string -> unit
1.24 + val register_theory: theory -> unit
1.25 val finish: unit -> unit
1.26 - val register_theory: theory -> unit
1.27 - val pretty_theory: theory -> Pretty.T
1.28 end;
1.29
1.30 structure ThyInfo: THY_INFO =
1.31 @@ -217,6 +217,24 @@
1.32
1.33 (** thy operations **)
1.34
1.35 +(* check state *)
1.36 +
1.37 +fun check_unfinished fail name =
1.38 + if known_thy name andalso is_finished name then
1.39 + fail (loader_msg "cannot update finished theory" [name])
1.40 + else ();
1.41 +
1.42 +fun check_files name =
1.43 + let
1.44 + val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
1.45 + val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
1.46 + val _ =
1.47 + if null missing_files then ()
1.48 + else warning (loader_msg "unresolved dependencies of theory" [name] ^
1.49 + " on file(s): " ^ commas_quote missing_files);
1.50 + in files end;
1.51 +
1.52 +
1.53 (* maintain 'outdated' flag *)
1.54
1.55 local
1.56 @@ -249,14 +267,6 @@
1.57 end;
1.58
1.59
1.60 -(* check 'finished' state *)
1.61 -
1.62 -fun check_unfinished fail name =
1.63 - if known_thy name andalso is_finished name then
1.64 - fail (loader_msg "cannot update finished theory" [name])
1.65 - else ();
1.66 -
1.67 -
1.68 (* load_file *)
1.69
1.70 local
1.71 @@ -300,29 +310,17 @@
1.72 fun required_by _ [] = ""
1.73 | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
1.74
1.75 -fun load_thy really ml time initiators dir name =
1.76 +fun load_thy ml time initiators dir name =
1.77 let
1.78 - val _ =
1.79 - if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators)
1.80 - else priority ("Registering theory " ^ quote name);
1.81 -
1.82 - val (master_path, text, files) =
1.83 + val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
1.84 + val (pos, text, files) =
1.85 (case get_deps name of
1.86 - SOME {master = SOME ((master_path, _), _), text = text as _ :: _, files, ...} =>
1.87 - (master_path, text, files)
1.88 + SOME {master = SOME ((master_path, _), _), text, files, ...} =>
1.89 + (Position.path master_path, text, files)
1.90 | _ => error (loader_msg "corrupted dependency information" [name]));
1.91 -
1.92 val _ = touch_thy name;
1.93 - val _ =
1.94 - if really then
1.95 - ThyLoad.load_thy dir name (Position.path master_path) text ml (time orelse ! Output.timing)
1.96 - else ();
1.97 -
1.98 - val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
1.99 - val _ =
1.100 - if null missing_files then ()
1.101 - else warning (loader_msg "unresolved dependencies of theory" [name] ^
1.102 - " on file(s): " ^ commas_quote missing_files);
1.103 + val _ = ThyLoad.load_thy dir name pos text ml (time orelse ! Output.timing);
1.104 + val _ = check_files name;
1.105 in
1.106 CRITICAL (fn () =>
1.107 (change_deps name
1.108 @@ -368,10 +366,10 @@
1.109
1.110 in
1.111
1.112 -fun require_thys really ml time strict keep_strict initiators dir strs tasks =
1.113 - fold_map (require_thy really ml time strict keep_strict initiators dir) strs tasks
1.114 +fun require_thys ml time strict keep_strict initiators dir strs tasks =
1.115 + fold_map (require_thy ml time strict keep_strict initiators dir) strs tasks
1.116 |>> forall I
1.117 -and require_thy really ml time strict keep_strict initiators dir str tasks =
1.118 +and require_thy ml time strict keep_strict initiators dir str tasks =
1.119 let
1.120 val path = Path.expand (Path.explode str);
1.121 val name = Path.implode (Path.base path);
1.122 @@ -389,16 +387,16 @@
1.123 val parent_names = map base_name parents;
1.124
1.125 val (parents_current, (tasks_graph', tasks_len')) =
1.126 - require_thys true true time (strict andalso keep_strict) keep_strict
1.127 + require_thys true time (strict andalso keep_strict) keep_strict
1.128 (name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
1.129
1.130 val all_current = current andalso parents_current;
1.131 - val thy = if all_current orelse not really then SOME (get_theory name) else NONE;
1.132 + val thy = if all_current then SOME (get_theory name) else NONE;
1.133 val _ = change_thys (new_deps name parent_names (deps, thy));
1.134
1.135 val tasks_graph'' = tasks_graph' |> new_deps name parent_names
1.136 (if all_current then Task.Finished
1.137 - else Task.Task (fn () => load_thy really ml time initiators dir' name));
1.138 + else Task.Task (fn () => load_thy ml time initiators dir' name));
1.139 val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
1.140 in (all_current, (tasks_graph'', tasks_len'')) end)
1.141 end;
1.142 @@ -459,13 +457,12 @@
1.143
1.144 in
1.145
1.146 -val quiet_update_thys = gen_use_thy' (require_thys true true false true true);
1.147 -val pretend_use_thy_only = gen_use_thy' (require_thy false false false true false) Path.current;
1.148 -val use_thys = gen_use_thy' (require_thys true true false true false) Path.current;
1.149 +val quiet_update_thys = gen_use_thy' (require_thys true false true true);
1.150 +val use_thys = gen_use_thy' (require_thys true false true false) Path.current;
1.151
1.152 -val use_thy = gen_use_thy (require_thy true true false true false);
1.153 -val time_use_thy = gen_use_thy (require_thy true true true true false);
1.154 -val update_thy = gen_use_thy (require_thy true true false true true);
1.155 +val use_thy = gen_use_thy (require_thy true false true false);
1.156 +val time_use_thy = gen_use_thy (require_thy true true true false);
1.157 +val update_thy = gen_use_thy (require_thy true false true true);
1.158
1.159 end;
1.160
1.161 @@ -524,12 +521,21 @@
1.162 in theory' end;
1.163
1.164
1.165 -(* finish all theories *)
1.166 +(* register existing theories *)
1.167
1.168 -fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
1.169 -
1.170 -
1.171 -(* register existing theories *)
1.172 +fun register_thy name =
1.173 + let
1.174 + val _ = priority ("Registering theory " ^ quote name);
1.175 + val _ = get_theory name;
1.176 + val _ = touch_thy name;
1.177 + val files = check_files name;
1.178 + val master = #master (ThyLoad.deps_thy Path.current name false);
1.179 + in
1.180 + CRITICAL (fn () =>
1.181 + (change_deps name
1.182 + (Option.map (fn {parents, ...} => make_deps false (SOME master) [] parents files));
1.183 + perform Update name))
1.184 + end;
1.185
1.186 fun register_theory theory =
1.187 let
1.188 @@ -558,6 +564,12 @@
1.189
1.190 val _ = register_theory ProtoPure.thy;
1.191
1.192 +
1.193 +(* finish all theories *)
1.194 +
1.195 +fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
1.196 +
1.197 +
1.198 (*final declarations of this structure*)
1.199 val theory = get_theory;
1.200 val names = get_names;