author | boehmes |
Mon, 06 Dec 2010 16:54:22 +0100 | |
changeset 41058 | 42e0a0bfef73 |
parent 40742 | dc6439c0b8b1 |
child 41412 | 35f30e07fe0d |
permissions | -rw-r--r-- |
6168 | 1 |
(* Title: Pure/Thy/thy_load.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
4 |
Loading files that contribute to a theory, including global load path |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
5 |
management. |
6168 | 6 |
*) |
7 |
||
8 |
signature BASIC_THY_LOAD = |
|
9 |
sig |
|
10 |
val show_path: unit -> string list |
|
11 |
val add_path: string -> unit |
|
10252 | 12 |
val path_add: string -> unit |
6168 | 13 |
val del_path: string -> unit |
6205 | 14 |
val reset_path: unit -> unit |
6168 | 15 |
end; |
16 |
||
17 |
signature THY_LOAD = |
|
18 |
sig |
|
19 |
include BASIC_THY_LOAD |
|
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
20 |
eqtype file_ident |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
21 |
val pretty_file_ident: file_ident -> Pretty.T |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
22 |
val file_ident: Path.T -> file_ident option |
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
23 |
val set_master_path: Path.T -> unit |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
24 |
val get_master_path: unit -> Path.T |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
25 |
val master_directory: theory -> Path.T |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
26 |
val provide: Path.T * (Path.T * file_ident) -> theory -> theory |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
27 |
val check_file: Path.T list -> Path.T -> Path.T * file_ident |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
28 |
val check_thy: Path.T -> string -> Path.T * file_ident |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
29 |
val deps_thy: Path.T -> string -> |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
30 |
{master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list} |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
31 |
val loaded_files: theory -> Path.T list |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
32 |
val all_current: theory -> bool |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
33 |
val provide_file: Path.T -> theory -> theory |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
34 |
val use_ml: Path.T -> unit |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
35 |
val exec_ml: Path.T -> generic_theory -> generic_theory |
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
36 |
val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory |
6168 | 37 |
end; |
38 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
39 |
structure Thy_Load: THY_LOAD = |
6168 | 40 |
struct |
41 |
||
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
42 |
(* file identification *) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
43 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
44 |
local |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
45 |
val file_ident_cache = |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
46 |
Synchronized.var "file_ident_cache" |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
47 |
(Symtab.empty: {time_stamp: string, id: string} Symtab.table); |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
48 |
in |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
49 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
50 |
fun check_cache (path, time) = |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
51 |
(case Symtab.lookup (Synchronized.value file_ident_cache) path of |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
52 |
NONE => NONE |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
53 |
| SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE); |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
54 |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
55 |
fun update_cache (path, (time, id)) = |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
56 |
Synchronized.change file_ident_cache |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
57 |
(Symtab.update (path, {time_stamp = time, id = id})); |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
58 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
59 |
end; |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
60 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
61 |
datatype file_ident = File_Ident of string; |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
62 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
63 |
fun pretty_file_ident (File_Ident s) = Pretty.str (quote s); |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
64 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
65 |
fun file_ident path = |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
66 |
let val physical_path = perhaps (try OS.FileSys.fullPath) (File.platform_path path) in |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
67 |
(case try (Time.toString o OS.FileSys.modTime) physical_path of |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
68 |
NONE => NONE |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
69 |
| SOME mod_time => SOME (File_Ident |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
70 |
(case getenv "ISABELLE_FILE_IDENT" of |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
71 |
"" => physical_path ^ ": " ^ mod_time |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
72 |
| cmd => |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
73 |
(case check_cache (physical_path, mod_time) of |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
74 |
SOME id => id |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
75 |
| NONE => |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
76 |
let |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
77 |
val (id, rc) = (*potentially slow*) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
78 |
bash_output |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
79 |
("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ File.shell_quote physical_path); |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
80 |
in |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
81 |
if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
82 |
else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
83 |
end)))) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
84 |
end; |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
85 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
86 |
|
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
87 |
(* manage source files *) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
88 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
89 |
type files = |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
90 |
{master_dir: Path.T, (*master directory of theory source*) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
91 |
required: Path.T list, (*source path*) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
92 |
provided: (Path.T * (Path.T * file_ident)) list}; (*source path, physical path, identifier*) |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
93 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
94 |
fun make_files (master_dir, required, provided): files = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
95 |
{master_dir = master_dir, required = required, provided = provided}; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
96 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
97 |
structure Files = Theory_Data |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
98 |
( |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
99 |
type T = files; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
100 |
val empty = make_files (Path.current, [], []); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
101 |
fun extend _ = empty; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
102 |
fun merge _ = empty; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
103 |
); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
104 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
105 |
fun map_files f = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
106 |
Files.map (fn {master_dir, required, provided} => |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
107 |
make_files (f (master_dir, required, provided))); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
108 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
109 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
110 |
val master_directory = #master_dir o Files.get; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
111 |
|
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
112 |
fun master dir = map_files (fn _ => (dir, [], [])); |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
113 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
114 |
fun require src_path = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
115 |
map_files (fn (master_dir, required, provided) => |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
116 |
if member (op =) required src_path then |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
117 |
error ("Duplicate source file dependency: " ^ Path.implode src_path) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
118 |
else (master_dir, src_path :: required, provided)); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
119 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
120 |
fun provide (src_path, path_id) = |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
121 |
map_files (fn (master_dir, required, provided) => |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
122 |
if AList.defined (op =) provided src_path then |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
123 |
error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path) |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
124 |
else (master_dir, required, (src_path, path_id) :: provided)); |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
125 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
126 |
|
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
127 |
(* maintain default paths *) |
6168 | 128 |
|
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
129 |
local |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
130 |
val load_path = Synchronized.var "load_path" [Path.current]; |
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
131 |
val master_path = Unsynchronized.ref Path.current; |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
132 |
in |
6168 | 133 |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
134 |
fun show_path () = map Path.implode (Synchronized.value load_path); |
23944 | 135 |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
136 |
fun del_path s = Synchronized.change load_path (remove (op =) (Path.explode s)); |
33221 | 137 |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
138 |
fun add_path s = Synchronized.change load_path (update (op =) (Path.explode s)); |
33221 | 139 |
|
140 |
fun path_add s = |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
141 |
Synchronized.change load_path (fn path => |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
142 |
let val p = Path.explode s |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
143 |
in remove (op =) p path @ [p] end); |
33221 | 144 |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
145 |
fun reset_path () = Synchronized.change load_path (K [Path.current]); |
6168 | 146 |
|
23944 | 147 |
fun search_path dir path = |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
148 |
distinct (op =) |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
149 |
(dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current])); |
23944 | 150 |
|
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
151 |
fun set_master_path path = master_path := path; |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
152 |
fun get_master_path () = ! master_path; |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
153 |
|
23944 | 154 |
end; |
155 |
||
6168 | 156 |
|
23872 | 157 |
(* check files *) |
6232 | 158 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
159 |
fun get_file dirs src_path = |
6232 | 160 |
let |
161 |
val path = Path.expand src_path; |
|
23872 | 162 |
val _ = Path.is_current path andalso error "Bad file specification"; |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
163 |
in |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
164 |
dirs |> get_first (fn dir => |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
165 |
let val full_path = File.full_path (Path.append dir path) in |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
166 |
(case file_ident full_path of |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
167 |
NONE => NONE |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
168 |
| SOME id => SOME (full_path, id)) |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
169 |
end) |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
170 |
end; |
6168 | 171 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
172 |
fun check_file dirs file = |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
173 |
(case get_file dirs file of |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
174 |
SOME path_id => path_id |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
175 |
| NONE => error ("Could not find file " ^ quote (Path.implode file) ^ |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
176 |
"\nin " ^ commas_quote (map Path.implode dirs))); |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
177 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
178 |
fun check_thy master_dir name = |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
179 |
let |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
180 |
val thy_file = Thy_Header.thy_path name; |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
181 |
val dirs = search_path master_dir thy_file; |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
182 |
in check_file dirs thy_file end; |
6232 | 183 |
|
184 |
||
23872 | 185 |
(* theory deps *) |
7940 | 186 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
187 |
fun deps_thy master_dir name = |
23872 | 188 |
let |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
189 |
val master as (thy_path, _) = check_thy master_dir name; |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
190 |
val text = File.read thy_path; |
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
191 |
val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text; |
37950
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37949
diff
changeset
|
192 |
val _ = Thy_Header.consistent_name name name'; |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
193 |
val uses = map (Path.explode o #1) uses; |
24065 | 194 |
in {master = master, text = text, imports = imports, uses = uses} end; |
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6363
diff
changeset
|
195 |
|
6168 | 196 |
|
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
197 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
198 |
(* loaded files *) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
199 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
200 |
val loaded_files = map (#1 o #2) o #provided o Files.get; |
6168 | 201 |
|
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
202 |
fun check_loaded thy = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
203 |
let |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
204 |
val {required, provided, ...} = Files.get thy; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
205 |
val provided_paths = map #1 provided; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
206 |
val _ = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
207 |
(case subtract (op =) provided_paths required of |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
208 |
[] => NONE |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
209 |
| bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad)))); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
210 |
val _ = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
211 |
(case subtract (op =) required provided_paths of |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
212 |
[] => NONE |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
213 |
| bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad)))); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
214 |
in () end; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
215 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
216 |
fun all_current thy = |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
217 |
let |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
218 |
val {master_dir, provided, ...} = Files.get thy; |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
219 |
fun current (src_path, (_, id)) = |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
220 |
(case get_file [master_dir] src_path of |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
221 |
NONE => false |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
222 |
| SOME (_, id') => id = id'); |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
223 |
in can check_loaded thy andalso forall current provided end; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
224 |
|
37952 | 225 |
val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE)))); |
226 |
||
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
227 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
228 |
(* provide files *) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
229 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
230 |
fun provide_file src_path thy = |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
231 |
provide (src_path, check_file [master_directory thy] src_path) thy; |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
232 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
233 |
fun use_ml src_path = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
234 |
if is_none (Context.thread_data ()) then |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
235 |
ML_Context.eval_file (#1 (check_file [Path.current] src_path)) |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
236 |
else |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
237 |
let |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
238 |
val thy = ML_Context.the_global_context (); |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
239 |
val (path, id) = check_file [master_directory thy] src_path; |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
240 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
241 |
val _ = ML_Context.eval_file path; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
242 |
val _ = Context.>> Local_Theory.propagate_ml_env; |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
243 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
244 |
val provide = provide (src_path, (path, id)); |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38133
diff
changeset
|
245 |
val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide)); |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
246 |
in () end; |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
247 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
248 |
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); |
6168 | 249 |
|
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
250 |
|
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
251 |
(* begin theory *) |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
252 |
|
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
253 |
fun begin_theory dir name parents uses = |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
254 |
Theory.begin_theory name parents |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
255 |
|> master dir |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
256 |
|> fold (require o fst) uses |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
257 |
|> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
258 |
|> Theory.checkpoint; |
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37952
diff
changeset
|
259 |
|
6168 | 260 |
end; |
261 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
262 |
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load; |
32738 | 263 |
open Basic_Thy_Load; |