author | wenzelm |
Sat, 24 Jul 2010 12:14:53 +0200 | |
changeset 37949 | 48a874444164 |
parent 37943 | 3cbd7fa164b1 |
child 37950 | bc285d91041e |
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 |
|
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
|
20 |
val master_directory: theory -> Path.T |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
21 |
val init: 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
|
22 |
val require: 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
|
23 |
val provide: Path.T * (Path.T * File.ident) -> theory -> theory |
6205 | 24 |
val ml_path: string -> Path.T |
7901 | 25 |
val thy_path: string -> Path.T |
29418 | 26 |
val split_thy_path: Path.T -> Path.T * string |
37937 | 27 |
val consistent_name: string -> string -> unit |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
28 |
val test_file: Path.T -> Path.T -> (Path.T * File.ident) option |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
29 |
val check_file: Path.T -> Path.T -> Path.T * File.ident |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
30 |
val check_thy: Path.T -> string -> Path.T * File.ident |
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
31 |
val deps_thy: Path.T -> string -> |
37902
4e7864f3643d
deps_thy/load_thy: store compact text to reduce space by factor 12;
wenzelm
parents:
37216
diff
changeset
|
32 |
{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
|
33 |
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
|
34 |
val check_loaded: theory -> 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 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
|
36 |
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
|
37 |
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
|
38 |
val exec_ml: Path.T -> generic_theory -> generic_theory |
6168 | 39 |
end; |
40 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
41 |
structure Thy_Load: THY_LOAD = |
6168 | 42 |
struct |
43 |
||
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
|
44 |
(* 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
|
45 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
46 |
type 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
|
47 |
{master_dir: Path.T, (*master directory of theory source*) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
48 |
required: Path.T list, (*source 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
|
49 |
provided: (Path.T * (Path.T * File.ident)) list}; (*source path, physical path, identifier*) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
50 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
51 |
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
|
52 |
{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
|
53 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
54 |
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
|
55 |
( |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
61 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
66 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
67 |
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
|
68 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
69 |
fun init master_dir = map_files (fn _ => (master_dir, [], [])); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
70 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
71 |
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
|
72 |
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
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
77 |
fun provide (src_path, path_info) = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
error ("Duplicate resolution of 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
|
81 |
else (master_dir, required, (src_path, path_info) :: 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
|
82 |
|
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 |
|
6232 | 84 |
(* maintain load path *) |
6168 | 85 |
|
32738 | 86 |
local val load_path = Unsynchronized.ref [Path.current] in |
6168 | 87 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
17366
diff
changeset
|
88 |
fun show_path () = map Path.implode (! load_path); |
23944 | 89 |
|
33221 | 90 |
fun del_path s = |
91 |
CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s))); |
|
92 |
||
93 |
fun add_path s = |
|
94 |
CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); |
|
95 |
||
96 |
fun path_add s = |
|
97 |
CRITICAL (fn () => |
|
32738 | 98 |
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s]))); |
33221 | 99 |
|
37938
445e5a3244cc
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
wenzelm
parents:
37937
diff
changeset
|
100 |
fun reset_path () = CRITICAL (fn () => load_path := [Path.current]); |
6168 | 101 |
|
23944 | 102 |
fun search_path dir path = |
103 |
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current])); |
|
104 |
||
105 |
end; |
|
106 |
||
6168 | 107 |
|
6232 | 108 |
(* file formats *) |
6168 | 109 |
|
6232 | 110 |
val ml_path = Path.ext "ML" o Path.basic; |
111 |
val thy_path = Path.ext "thy" o Path.basic; |
|
6168 | 112 |
|
29418 | 113 |
fun split_thy_path path = |
114 |
(case Path.split_ext path of |
|
115 |
(path', "thy") => (Path.dir path', Path.implode (Path.base path')) |
|
116 |
| _ => error ("Bad theory file specification " ^ Path.implode path)); |
|
117 |
||
37937 | 118 |
fun consistent_name name name' = |
119 |
if name = name' then () |
|
120 |
else error ("Filename " ^ quote (Path.implode (thy_path name)) ^ |
|
121 |
" does not agree with theory name " ^ quote name'); |
|
122 |
||
6168 | 123 |
|
23872 | 124 |
(* check files *) |
6232 | 125 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
126 |
local |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
127 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
128 |
exception NOT_FOUND of Path.T list * Path.T; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
129 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
130 |
fun try_file dir src_path = |
6232 | 131 |
let |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
132 |
val prfxs = search_path dir src_path; |
6232 | 133 |
val path = Path.expand src_path; |
23872 | 134 |
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
|
135 |
val result = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
136 |
prfxs |> get_first (fn prfx => |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
137 |
let val full_path = File.full_path (Path.append prfx path) |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
138 |
in Option.map (pair full_path) (File.ident full_path) end); |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
139 |
in |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
140 |
(case result of |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
141 |
SOME res => res |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
142 |
| NONE => raise NOT_FOUND (prfxs, path)) |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
143 |
end; |
6168 | 144 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
145 |
in |
6168 | 146 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
147 |
fun test_file dir file = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
148 |
SOME (try_file dir file) handle NOT_FOUND _ => NONE; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
149 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
150 |
fun check_file dir file = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
151 |
try_file dir file handle NOT_FOUND (prfxs, path) => |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
152 |
error ("Could not find file " ^ quote (Path.implode path) ^ |
37943 | 153 |
"\nin " ^ commas_quote (map Path.implode prfxs)); |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
154 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
155 |
fun check_thy dir name = check_file dir (thy_path name); |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
156 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
157 |
end; |
6232 | 158 |
|
159 |
||
23872 | 160 |
(* theory deps *) |
7940 | 161 |
|
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
162 |
fun deps_thy dir name = |
23872 | 163 |
let |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
164 |
val master as (path, _) = check_thy dir name; |
37902
4e7864f3643d
deps_thy/load_thy: store compact text to reduce space by factor 12;
wenzelm
parents:
37216
diff
changeset
|
165 |
val text = File.read path; |
23872 | 166 |
val (name', imports, uses) = |
37903
b7ae269c0d68
replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
wenzelm
parents:
37902
diff
changeset
|
167 |
Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text); |
37937 | 168 |
val _ = consistent_name name name'; |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
169 |
val uses = map (Path.explode o #1) uses; |
24065 | 170 |
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
|
171 |
|
6168 | 172 |
|
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
|
173 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
174 |
(* 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
|
175 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
176 |
val loaded_files = map (#1 o #2) o #provided o Files.get; |
6168 | 177 |
|
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
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
|
183 |
(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
|
184 |
[] => 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
|
185 |
| 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
|
186 |
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
|
187 |
(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
|
188 |
[] => 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
|
189 |
| 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
|
190 |
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
|
191 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
192 |
fun all_current thy = |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
193 |
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
|
194 |
val {master_dir, 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
|
195 |
fun current (src_path, path_info) = |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
196 |
(case test_file master_dir src_path 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
|
197 |
NONE => false |
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 |
| SOME path_info' => eq_snd (op =) (path_info, path_info')); |
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 |
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
|
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 |
|
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 |
(* 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
|
203 |
|
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 |
fun provide_file src_path 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 |
provide (src_path, check_file (master_directory thy) src_path) 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 |
|
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 |
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
|
208 |
if is_none (Context.thread_data ()) 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
|
209 |
ML_Context.eval_file (#1 (check_file Path.current 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
|
210 |
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
|
211 |
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
|
212 |
val thy = ML_Context.the_global_context (); |
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 |
val (path, info) = check_file (master_directory thy) 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
|
214 |
|
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 |
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
|
216 |
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
|
217 |
|
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 provide = provide (src_path, (path, info)); |
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 _ = Context.>> (Context.mapping provide (Local_Theory.theory provide)); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
220 |
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
|
221 |
|
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 |
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); |
6168 | 223 |
|
224 |
end; |
|
225 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
226 |
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load; |
32738 | 227 |
open Basic_Thy_Load; |