author | wenzelm |
Thu, 26 Aug 2010 15:48:08 +0200 | |
changeset 38757 | 2b3e054ae6fc |
parent 38133 | 987680d2e77d |
child 40625 | 2d9222a2239d |
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 |
|
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
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
|
24 |
val provide: Path.T * (Path.T * File.ident) -> theory -> theory |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
25 |
val check_file: Path.T list -> 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 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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> 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 |
|
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
|
65 |
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
|
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 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
73 |
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
|
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) |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
77 |
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
|
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 |
|
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
|
80 |
(* maintain default paths *) |
6168 | 81 |
|
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
|
82 |
local |
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
|
83 |
val load_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
|
84 |
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
|
85 |
in |
6168 | 86 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
17366
diff
changeset
|
87 |
fun show_path () = map Path.implode (! load_path); |
23944 | 88 |
|
33221 | 89 |
fun del_path s = |
90 |
CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s))); |
|
91 |
||
92 |
fun add_path s = |
|
93 |
CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); |
|
94 |
||
95 |
fun path_add s = |
|
96 |
CRITICAL (fn () => |
|
32738 | 97 |
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s]))); |
33221 | 98 |
|
37938
445e5a3244cc
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
wenzelm
parents:
37937
diff
changeset
|
99 |
fun reset_path () = CRITICAL (fn () => load_path := [Path.current]); |
6168 | 100 |
|
23944 | 101 |
fun search_path dir path = |
102 |
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current])); |
|
103 |
||
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
|
104 |
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
|
105 |
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
|
106 |
|
23944 | 107 |
end; |
108 |
||
6168 | 109 |
|
23872 | 110 |
(* check files *) |
6232 | 111 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
112 |
fun get_file dirs src_path = |
6232 | 113 |
let |
114 |
val path = Path.expand src_path; |
|
23872 | 115 |
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
|
116 |
in |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
117 |
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
|
118 |
let val full_path = File.full_path (Path.append dir path) in |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
119 |
(case File.ident full_path of |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
120 |
NONE => NONE |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
121 |
| SOME id => SOME (full_path, id)) |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
122 |
end) |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
123 |
end; |
6168 | 124 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
125 |
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
|
126 |
(case get_file dirs file of |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
127 |
SOME path_id => path_id |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
128 |
| 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
|
129 |
"\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
|
130 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
131 |
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
|
132 |
let |
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
133 |
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
|
134 |
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
|
135 |
in check_file dirs thy_file end; |
6232 | 136 |
|
137 |
||
23872 | 138 |
(* theory deps *) |
7940 | 139 |
|
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
140 |
fun deps_thy master_dir name = |
23872 | 141 |
let |
38133
987680d2e77d
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
wenzelm
parents:
37978
diff
changeset
|
142 |
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
|
143 |
val text = File.read thy_path; |
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
144 |
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
|
145 |
val _ = Thy_Header.consistent_name name name'; |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
146 |
val uses = map (Path.explode o #1) uses; |
24065 | 147 |
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
|
148 |
|
6168 | 149 |
|
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
|
150 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
151 |
(* 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
|
152 |
|
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 |
val loaded_files = map (#1 o #2) o #provided o Files.get; |
6168 | 154 |
|
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
|
155 |
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
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
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
|
160 |
(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
|
161 |
[] => 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
|
162 |
| 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
|
163 |
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
|
164 |
(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
|
165 |
[] => 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
|
166 |
| 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
|
167 |
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
|
168 |
|
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 |
fun all_current thy = |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
170 |
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
|
171 |
val {master_dir, provided, ...} = Files.get thy; |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
172 |
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
|
173 |
(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
|
174 |
NONE => false |
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
175 |
| 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
|
176 |
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
|
177 |
|
37952 | 178 |
val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE)))); |
179 |
||
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
|
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 |
(* 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
|
182 |
|
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 |
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
|
184 |
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
|
185 |
|
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 |
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
|
187 |
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
|
188 |
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
|
189 |
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
|
190 |
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
|
191 |
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
|
192 |
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
|
193 |
|
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 _ = 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
|
195 |
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
|
196 |
|
37978
548f3f165d05
simplified Thy_Header.read -- include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset
|
197 |
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
|
198 |
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
|
199 |
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
|
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 |
fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path); |
6168 | 202 |
|
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
|
203 |
|
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
|
204 |
(* 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
|
205 |
|
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
|
206 |
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
|
207 |
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
|
208 |
|> 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
|
209 |
|> 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
|
210 |
|> 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
|
211 |
|> 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
|
212 |
|
6168 | 213 |
end; |
214 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
215 |
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load; |
32738 | 216 |
open Basic_Thy_Load; |