author | wenzelm |
Sat, 24 Jul 2010 21:22:21 +0200 | |
changeset 37950 | bc285d91041e |
parent 37949 | 48a874444164 |
child 37952 | f6c40213675b |
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 |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
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
|
28 |
{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
|
29 |
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
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
val exec_ml: Path.T -> generic_theory -> generic_theory |
6168 | 35 |
end; |
36 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
37 |
structure Thy_Load: THY_LOAD = |
6168 | 38 |
struct |
39 |
||
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
|
40 |
(* 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
|
41 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
42 |
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
|
43 |
{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
|
44 |
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
|
45 |
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
|
46 |
|
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 |
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
|
48 |
{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
|
49 |
|
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 |
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
|
51 |
( |
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 |
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
|
53 |
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
|
54 |
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
|
55 |
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
|
56 |
); |
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 |
|
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 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
|
59 |
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
|
60 |
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
|
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 |
|
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 |
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
|
64 |
|
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 |
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
|
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 |
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
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
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
|
72 |
|
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 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
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
|
78 |
|
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 |
|
6232 | 80 |
(* maintain load path *) |
6168 | 81 |
|
32738 | 82 |
local val load_path = Unsynchronized.ref [Path.current] in |
6168 | 83 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
17366
diff
changeset
|
84 |
fun show_path () = map Path.implode (! load_path); |
23944 | 85 |
|
33221 | 86 |
fun del_path s = |
87 |
CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s))); |
|
88 |
||
89 |
fun add_path s = |
|
90 |
CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); |
|
91 |
||
92 |
fun path_add s = |
|
93 |
CRITICAL (fn () => |
|
32738 | 94 |
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s]))); |
33221 | 95 |
|
37938
445e5a3244cc
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
wenzelm
parents:
37937
diff
changeset
|
96 |
fun reset_path () = CRITICAL (fn () => load_path := [Path.current]); |
6168 | 97 |
|
23944 | 98 |
fun search_path dir path = |
99 |
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current])); |
|
100 |
||
101 |
end; |
|
102 |
||
6168 | 103 |
|
23872 | 104 |
(* check files *) |
6232 | 105 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
106 |
local |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
107 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
108 |
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
|
109 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
110 |
fun try_file dir src_path = |
6232 | 111 |
let |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
112 |
val prfxs = search_path dir src_path; |
6232 | 113 |
val path = Path.expand src_path; |
23872 | 114 |
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
|
115 |
val result = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
116 |
prfxs |> get_first (fn prfx => |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
117 |
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
|
118 |
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
|
119 |
in |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
120 |
(case result of |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
121 |
SOME res => res |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
122 |
| NONE => raise NOT_FOUND (prfxs, path)) |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
123 |
end; |
6168 | 124 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
125 |
in |
6168 | 126 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
127 |
fun test_file dir file = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
128 |
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
|
129 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
130 |
fun check_file dir file = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
131 |
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
|
132 |
error ("Could not find file " ^ quote (Path.implode path) ^ |
37943 | 133 |
"\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
|
134 |
|
37950
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37949
diff
changeset
|
135 |
fun check_thy dir name = check_file dir (Thy_Header.thy_path name); |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
136 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
137 |
end; |
6232 | 138 |
|
139 |
||
23872 | 140 |
(* theory deps *) |
7940 | 141 |
|
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
142 |
fun deps_thy dir name = |
23872 | 143 |
let |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
144 |
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
|
145 |
val text = File.read path; |
23872 | 146 |
val (name', imports, uses) = |
37903
b7ae269c0d68
replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
wenzelm
parents:
37902
diff
changeset
|
147 |
Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text); |
37950
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37949
diff
changeset
|
148 |
val _ = Thy_Header.consistent_name name name'; |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
149 |
val uses = map (Path.explode o #1) uses; |
24065 | 150 |
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
|
151 |
|
6168 | 152 |
|
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
|
153 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
154 |
(* 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
|
155 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
156 |
val loaded_files = map (#1 o #2) o #provided o Files.get; |
6168 | 157 |
|
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
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
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
|
162 |
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
|
163 |
(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
|
164 |
[] => 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
|
165 |
| 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
|
166 |
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
|
167 |
(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
|
168 |
[] => 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
|
169 |
| 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
|
170 |
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
|
171 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
172 |
fun all_current thy = |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
(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
|
177 |
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
|
178 |
| 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
|
179 |
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
|
180 |
|
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 |
|
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 |
(* 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
|
183 |
|
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 |
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
|
185 |
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
|
186 |
|
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 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
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
|
193 |
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
|
194 |
|
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 |
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
|
196 |
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
|
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 |
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
|
199 |
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
|
200 |
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
|
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 |
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); |
6168 | 203 |
|
204 |
end; |
|
205 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
206 |
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load; |
32738 | 207 |
open Basic_Thy_Load; |