13 val set_master_path: Path.T -> unit |
13 val set_master_path: Path.T -> unit |
14 val get_master_path: unit -> Path.T |
14 val get_master_path: unit -> Path.T |
15 val master_directory: theory -> Path.T |
15 val master_directory: theory -> Path.T |
16 val imports_of: theory -> string list |
16 val imports_of: theory -> string list |
17 val provide: Path.T * (Path.T * file_ident) -> theory -> theory |
17 val provide: Path.T * (Path.T * file_ident) -> theory -> theory |
18 val legacy_show_path: unit -> string list |
18 val check_file: Path.T -> Path.T -> Path.T * file_ident |
19 val legacy_add_path: string -> unit |
|
20 val legacy_path_add: string -> unit |
|
21 val legacy_del_path: string -> unit |
|
22 val legacy_reset_path: unit -> unit |
|
23 val check_file: Path.T list -> Path.T -> Path.T * file_ident |
|
24 val check_thy: Path.T -> string -> Path.T * file_ident |
19 val check_thy: Path.T -> string -> Path.T * file_ident |
25 val deps_thy: Path.T -> string -> |
20 val deps_thy: Path.T -> string -> |
26 {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list} |
21 {master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list} |
27 val loaded_files: theory -> Path.T list |
22 val loaded_files: theory -> Path.T list |
28 val all_current: theory -> bool |
23 val all_current: theory -> bool |
120 if AList.defined (op =) provided src_path then |
115 if AList.defined (op =) provided src_path then |
121 error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path) |
116 error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path) |
122 else (master_dir, imports, required, (src_path, path_id) :: provided)); |
117 else (master_dir, imports, required, (src_path, path_id) :: provided)); |
123 |
118 |
124 |
119 |
125 (* maintain default paths *) |
120 (* stateful master path *) |
126 |
121 |
127 local |
122 local |
128 val load_path = Synchronized.var "load_path" [Path.current]; |
|
129 val master_path = Unsynchronized.ref Path.current; |
123 val master_path = Unsynchronized.ref Path.current; |
130 in |
124 in |
131 |
125 |
132 fun legacy_show_path () = map Path.implode (Synchronized.value load_path); |
|
133 |
|
134 fun legacy_del_path s = Synchronized.change load_path (remove (op =) (Path.explode s)); |
|
135 |
|
136 fun legacy_add_path s = Synchronized.change load_path (update (op =) (Path.explode s)); |
|
137 |
|
138 fun legacy_path_add s = |
|
139 Synchronized.change load_path (fn path => |
|
140 let val p = Path.explode s |
|
141 in remove (op =) p path @ [p] end); |
|
142 |
|
143 fun legacy_reset_path () = Synchronized.change load_path (K [Path.current]); |
|
144 |
|
145 fun search_path dir path = |
|
146 distinct (op =) |
|
147 (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current])); |
|
148 |
|
149 fun set_master_path path = master_path := path; |
126 fun set_master_path path = master_path := path; |
150 fun get_master_path () = ! master_path; |
127 fun get_master_path () = ! master_path; |
151 |
128 |
152 end; |
129 end; |
153 |
130 |
154 |
131 |
155 (* check files *) |
132 (* check files *) |
156 |
133 |
157 fun get_file dirs src_path = |
134 fun get_file dir src_path = |
158 let |
135 let |
159 val path = Path.expand src_path; |
136 val path = Path.expand src_path; |
160 val _ = Path.is_current path andalso error "Bad file specification"; |
137 val _ = Path.is_current path andalso error "Bad file specification"; |
|
138 val full_path = File.full_path (Path.append dir path); |
161 in |
139 in |
162 dirs |> get_first (fn dir => |
140 (case file_ident full_path of |
163 let val full_path = File.full_path (Path.append dir path) in |
141 NONE => NONE |
164 (case file_ident full_path of |
142 | SOME id => SOME (full_path, id)) |
165 NONE => NONE |
|
166 | SOME id => SOME (dir, (full_path, id))) |
|
167 end) |
|
168 end; |
143 end; |
169 |
144 |
170 fun check_file dirs file = |
145 fun check_file dir file = |
171 (case get_file dirs file of |
146 (case get_file dir file of |
172 SOME (_, path_id) => |
147 SOME path_id => path_id |
173 (if is_some (get_file [hd dirs] file) then () |
|
174 else |
|
175 legacy_feature ("File " ^ quote (Path.implode file) ^ |
|
176 " located via secondary search path: " ^ |
|
177 quote (Path.implode (#1 (the (get_file (tl dirs) file))))); |
|
178 path_id) |
|
179 | NONE => error ("Could not find file " ^ quote (Path.implode file) ^ |
148 | NONE => error ("Could not find file " ^ quote (Path.implode file) ^ |
180 "\nin " ^ commas_quote (map Path.implode dirs))); |
149 "\nin " ^ quote (Path.implode dir))); |
181 |
150 |
182 fun check_thy master_dir name = |
151 fun check_thy dir name = |
183 let |
152 check_file dir (Thy_Header.thy_path name); |
184 val thy_file = Thy_Header.thy_path name; |
|
185 val dirs = search_path master_dir thy_file; |
|
186 in check_file dirs thy_file end; |
|
187 |
153 |
188 |
154 |
189 (* theory deps *) |
155 (* theory deps *) |
190 |
156 |
191 fun deps_thy master_dir name = |
157 fun deps_thy master_dir name = |
219 |
185 |
220 fun all_current thy = |
186 fun all_current thy = |
221 let |
187 let |
222 val {master_dir, provided, ...} = Files.get thy; |
188 val {master_dir, provided, ...} = Files.get thy; |
223 fun current (src_path, (_, id)) = |
189 fun current (src_path, (_, id)) = |
224 (case get_file [master_dir] src_path of |
190 (case get_file master_dir src_path of |
225 NONE => false |
191 NONE => false |
226 | SOME (_, (_, id')) => id = id'); |
192 | SOME (_, id') => id = id'); |
227 in can check_loaded thy andalso forall current provided end; |
193 in can check_loaded thy andalso forall current provided end; |
228 |
194 |
229 val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE)))); |
195 val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE)))); |
230 |
196 |
231 |
197 |
232 (* provide files *) |
198 (* provide files *) |
233 |
199 |
234 fun provide_file src_path thy = |
200 fun provide_file src_path thy = |
235 provide (src_path, check_file [master_directory thy] src_path) thy; |
201 provide (src_path, check_file (master_directory thy) src_path) thy; |
236 |
202 |
237 fun use_ml src_path = |
203 fun use_ml src_path = |
238 if is_none (Context.thread_data ()) then |
204 if is_none (Context.thread_data ()) then |
239 ML_Context.eval_file (#1 (check_file [Path.current] src_path)) |
205 ML_Context.eval_file (#1 (check_file Path.current src_path)) |
240 else |
206 else |
241 let |
207 let |
242 val thy = ML_Context.the_global_context (); |
208 val thy = ML_Context.the_global_context (); |
243 val (path, id) = check_file [master_directory thy] src_path; |
209 val (path, id) = check_file (master_directory thy) src_path; |
244 |
210 |
245 val _ = ML_Context.eval_file path; |
211 val _ = ML_Context.eval_file path; |
246 val _ = Context.>> Local_Theory.propagate_ml_env; |
212 val _ = Context.>> Local_Theory.propagate_ml_env; |
247 |
213 |
248 val provide = provide (src_path, (path, id)); |
214 val provide = provide (src_path, (path, id)); |