author | wenzelm |
Wed, 29 Dec 2010 18:18:42 +0100 | |
changeset 41414 | 00b2b6716ed8 |
parent 41412 | 35f30e07fe0d |
child 41548 | bd0bebf93fa6 |
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 THY_LOAD = |
|
9 |
sig |
|
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
10 |
eqtype file_ident |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
11 |
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
|
12 |
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
|
13 |
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
|
14 |
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
|
15 |
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
|
16 |
val provide: Path.T * (Path.T * file_ident) -> theory -> theory |
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
17 |
val legacy_show_path: unit -> string list |
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
18 |
val legacy_add_path: string -> unit |
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
19 |
val legacy_path_add: string -> unit |
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
20 |
val legacy_del_path: string -> unit |
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
21 |
val legacy_reset_path: unit -> unit |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
{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
|
26 |
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
|
27 |
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
|
28 |
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
|
29 |
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
|
30 |
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
|
31 |
val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory |
6168 | 32 |
end; |
33 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
34 |
structure Thy_Load: THY_LOAD = |
6168 | 35 |
struct |
36 |
||
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
37 |
(* file identification *) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
38 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
39 |
local |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
40 |
val file_ident_cache = |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
41 |
Synchronized.var "file_ident_cache" |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
42 |
(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
|
43 |
in |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
44 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
45 |
fun check_cache (path, time) = |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
46 |
(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
|
47 |
NONE => NONE |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
48 |
| 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
|
49 |
|
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
50 |
fun update_cache (path, (time, id)) = |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
51 |
Synchronized.change file_ident_cache |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
52 |
(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
|
53 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
54 |
end; |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
55 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
56 |
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
|
57 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
58 |
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
|
59 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
60 |
fun file_ident path = |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
61 |
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
|
62 |
(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
|
63 |
NONE => NONE |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
64 |
| SOME mod_time => SOME (File_Ident |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
65 |
(case getenv "ISABELLE_FILE_IDENT" of |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
66 |
"" => physical_path ^ ": " ^ mod_time |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
67 |
| cmd => |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
68 |
(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
|
69 |
SOME id => id |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
70 |
| NONE => |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
71 |
let |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
72 |
val (id, rc) = (*potentially slow*) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
73 |
bash_output |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
74 |
("\"$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
|
75 |
in |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
76 |
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
|
77 |
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
|
78 |
end)))) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
79 |
end; |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
80 |
|
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
81 |
|
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
|
82 |
(* 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
|
83 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
84 |
type files = |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
85 |
{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
|
86 |
required: Path.T list, (*source path*) |
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
87 |
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
|
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 |
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
|
90 |
{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
|
91 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
92 |
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
|
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 |
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
|
95 |
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
|
96 |
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
|
97 |
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
|
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 |
|
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 |
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
|
101 |
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
|
102 |
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
|
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 |
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
|
106 |
|
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
|
107 |
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
|
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 |
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
|
110 |
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
|
111 |
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
|
112 |
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
|
113 |
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
|
114 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
115 |
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
|
116 |
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
|
117 |
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
|
118 |
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
|
119 |
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
|
120 |
|
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 |
|
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
|
122 |
(* maintain default paths *) |
6168 | 123 |
|
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
|
124 |
local |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
125 |
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
|
126 |
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
|
127 |
in |
6168 | 128 |
|
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
129 |
fun legacy_show_path () = map Path.implode (Synchronized.value load_path); |
23944 | 130 |
|
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
131 |
fun legacy_del_path s = Synchronized.change load_path (remove (op =) (Path.explode s)); |
33221 | 132 |
|
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
133 |
fun legacy_add_path s = Synchronized.change load_path (update (op =) (Path.explode s)); |
33221 | 134 |
|
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
135 |
fun legacy_path_add s = |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
136 |
Synchronized.change load_path (fn path => |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
137 |
let val p = Path.explode s |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
138 |
in remove (op =) p path @ [p] end); |
33221 | 139 |
|
41414
00b2b6716ed8
theory loader: implicit load path is considered legacy;
wenzelm
parents:
41412
diff
changeset
|
140 |
fun legacy_reset_path () = Synchronized.change load_path (K [Path.current]); |
6168 | 141 |
|
23944 | 142 |
fun search_path dir path = |
40742
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
143 |
distinct (op =) |
dc6439c0b8b1
prefer Synchronized.var over CRITICAL/Unsynchronized.ref;
wenzelm
parents:
40741
diff
changeset
|
144 |
(dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current])); |
23944 | 145 |
|
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
|
146 |
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
|
147 |
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
|
148 |
|
23944 | 149 |
end; |
150 |
||
6168 | 151 |
|
23872 | 152 |
(* check files *) |
6232 | 153 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
154 |
fun get_file dirs src_path = |
6232 | 155 |
let |
156 |
val path = Path.expand src_path; |
|
23872 | 157 |
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
|
158 |
in |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
159 |
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
|
160 |
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
|
161 |
(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
|
162 |
NONE => NONE |
41412
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
163 |
| SOME id => SOME (dir, (full_path, id))) |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
164 |
end) |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
165 |
end; |
6168 | 166 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
167 |
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
|
168 |
(case get_file dirs file of |
41412
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
169 |
SOME (_, path_id) => |
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
170 |
(if is_some (get_file [hd dirs] file) then () |
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
171 |
else |
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
172 |
legacy_feature ("File " ^ quote (Path.implode file) ^ |
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
173 |
" located via secondary search path: " ^ |
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
174 |
quote (Path.implode (#1 (the (get_file (tl dirs) file))))); |
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
175 |
path_id) |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
176 |
| 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
|
177 |
"\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
|
178 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
179 |
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
|
180 |
let |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
181 |
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
|
182 |
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
|
183 |
in check_file dirs thy_file end; |
6232 | 184 |
|
185 |
||
23872 | 186 |
(* theory deps *) |
7940 | 187 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
188 |
fun deps_thy master_dir name = |
23872 | 189 |
let |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
190 |
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
|
191 |
val text = File.read thy_path; |
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
192 |
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
|
193 |
val _ = Thy_Header.consistent_name name name'; |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
194 |
val uses = map (Path.explode o #1) uses; |
24065 | 195 |
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
|
196 |
|
6168 | 197 |
|
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
|
198 |
|
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 |
(* 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
|
200 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
201 |
val loaded_files = map (#1 o #2) o #provided o Files.get; |
6168 | 202 |
|
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
|
203 |
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
|
204 |
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
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
(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
|
209 |
[] => 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
|
210 |
| 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
|
211 |
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
|
212 |
(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
|
213 |
[] => 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
|
214 |
| 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
|
215 |
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
|
216 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
217 |
fun all_current thy = |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
218 |
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
|
219 |
val {master_dir, provided, ...} = Files.get thy; |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
220 |
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
|
221 |
(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
|
222 |
NONE => false |
41412
35f30e07fe0d
check_file: secondary load path is legacy feature;
wenzelm
parents:
40742
diff
changeset
|
223 |
| 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
|
224 |
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
|
225 |
|
37952 | 226 |
val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE)))); |
227 |
||
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
|
228 |
|
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 |
(* 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
|
230 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
231 |
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
|
232 |
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
|
233 |
|
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 |
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
|
235 |
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
|
236 |
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
|
237 |
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
|
238 |
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
|
239 |
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
|
240 |
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
|
241 |
|
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 _ = 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
|
243 |
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
|
244 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
245 |
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
|
246 |
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
|
247 |
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
|
248 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
249 |
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); |
6168 | 250 |
|
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
|
251 |
|
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 |
(* 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
|
253 |
|
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 |
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
|
255 |
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
|
256 |
|> 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
|
257 |
|> 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
|
258 |
|> 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
|
259 |
|> 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
|
260 |
|
6168 | 261 |
end; |
262 |