--- a/src/Pure/Thy/thy_info.ML Tue Jul 31 00:56:32 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Jul 31 00:56:34 2007 +0200
@@ -26,23 +26,23 @@
val lookup_theory: string -> theory option
val get_theory: string -> theory
val the_theory: string -> theory -> theory
+ val loaded_files: string -> Path.T list
val get_parents: string -> string list
- val loaded_files: string -> Path.T list
+ val pretty_theory: theory -> Pretty.T
val touch_child_thys: string -> unit
val touch_all_thys: unit -> unit
val load_file: bool -> Path.T -> unit
val use: string -> unit
val time_use: string -> unit
- val pretend_use_thy_only: string -> unit
val use_thys: string list -> unit
val use_thy: string -> unit
val time_use_thy: string -> unit
val update_thy: string -> unit
val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
val end_theory: theory -> theory
- val finish: unit -> unit
+ val register_thy: string -> unit
val register_theory: theory -> unit
- val pretty_theory: theory -> Pretty.T
+ val finish: unit -> unit
end;
structure ThyInfo: THY_INFO =
@@ -217,6 +217,24 @@
(** thy operations **)
+(* check state *)
+
+fun check_unfinished fail name =
+ if known_thy name andalso is_finished name then
+ fail (loader_msg "cannot update finished theory" [name])
+ else ();
+
+fun check_files name =
+ let
+ val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
+ 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 files end;
+
+
(* maintain 'outdated' flag *)
local
@@ -249,14 +267,6 @@
end;
-(* check 'finished' state *)
-
-fun check_unfinished fail name =
- if known_thy name andalso is_finished name then
- fail (loader_msg "cannot update finished theory" [name])
- else ();
-
-
(* load_file *)
local
@@ -300,29 +310,17 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy really ml time initiators dir name =
+fun load_thy ml time initiators dir name =
let
- val _ =
- if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators)
- else priority ("Registering theory " ^ quote name);
-
- val (master_path, text, files) =
+ val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+ val (pos, text, files) =
(case get_deps name of
- SOME {master = SOME ((master_path, _), _), text = text as _ :: _, files, ...} =>
- (master_path, text, files)
+ SOME {master = SOME ((master_path, _), _), text, files, ...} =>
+ (Position.path master_path, text, files)
| _ => error (loader_msg "corrupted dependency information" [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);
+ val _ = ThyLoad.load_thy dir name pos text ml (time orelse ! Output.timing);
+ val _ = check_files name;
in
CRITICAL (fn () =>
(change_deps name
@@ -368,10 +366,10 @@
in
-fun require_thys really ml time strict keep_strict initiators dir strs tasks =
- fold_map (require_thy really ml time strict keep_strict initiators dir) strs tasks
+fun require_thys ml time strict keep_strict initiators dir strs tasks =
+ fold_map (require_thy ml time strict keep_strict initiators dir) strs tasks
|>> forall I
-and require_thy really ml time strict keep_strict initiators dir str tasks =
+and require_thy ml time strict keep_strict initiators dir str tasks =
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
@@ -389,16 +387,16 @@
val parent_names = map base_name parents;
val (parents_current, (tasks_graph', tasks_len')) =
- require_thys true true time (strict andalso keep_strict) keep_strict
+ require_thys true time (strict andalso keep_strict) keep_strict
(name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
val all_current = current andalso parents_current;
- val thy = if all_current orelse not really then SOME (get_theory name) else NONE;
+ val thy = if all_current then SOME (get_theory name) else NONE;
val _ = change_thys (new_deps name parent_names (deps, thy));
val tasks_graph'' = tasks_graph' |> new_deps name parent_names
(if all_current then Task.Finished
- else Task.Task (fn () => load_thy really ml time initiators dir' name));
+ else Task.Task (fn () => load_thy ml time initiators dir' name));
val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1;
in (all_current, (tasks_graph'', tasks_len'')) end)
end;
@@ -459,13 +457,12 @@
in
-val quiet_update_thys = gen_use_thy' (require_thys true true false true true);
-val pretend_use_thy_only = gen_use_thy' (require_thy false false false true false) Path.current;
-val use_thys = gen_use_thy' (require_thys true true false true false) Path.current;
+val quiet_update_thys = gen_use_thy' (require_thys true false true true);
+val use_thys = gen_use_thy' (require_thys true false true false) Path.current;
-val use_thy = gen_use_thy (require_thy true true false true false);
-val time_use_thy = gen_use_thy (require_thy true true true true false);
-val update_thy = gen_use_thy (require_thy true true false true true);
+val use_thy = gen_use_thy (require_thy true false true false);
+val time_use_thy = gen_use_thy (require_thy true true true false);
+val update_thy = gen_use_thy (require_thy true false true true);
end;
@@ -524,12 +521,21 @@
in theory' end;
-(* finish all theories *)
+(* register existing theories *)
-fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
-
-
-(* register existing theories *)
+fun register_thy name =
+ let
+ val _ = priority ("Registering theory " ^ quote name);
+ val _ = get_theory name;
+ val _ = touch_thy name;
+ val files = check_files name;
+ val master = #master (ThyLoad.deps_thy Path.current name false);
+ in
+ CRITICAL (fn () =>
+ (change_deps name
+ (Option.map (fn {parents, ...} => make_deps false (SOME master) [] parents files));
+ perform Update name))
+ end;
fun register_theory theory =
let
@@ -558,6 +564,12 @@
val _ = register_theory ProtoPure.thy;
+
+(* finish all theories *)
+
+fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
+
+
(*final declarations of this structure*)
val theory = get_theory;
val names = get_names;