author | wenzelm |
Thu, 22 Jul 2010 23:29:39 +0200 | |
changeset 37943 | 3cbd7fa164b1 |
parent 37939 | 965537d86fcc |
child 37949 | 48a874444164 |
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 |
|
6205 | 20 |
val ml_path: string -> Path.T |
7901 | 21 |
val thy_path: string -> Path.T |
29418 | 22 |
val split_thy_path: Path.T -> Path.T * string |
37937 | 23 |
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
|
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} |
23885
09254a1622e3
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23876
diff
changeset
|
29 |
val load_ml: Path.T -> Path.T -> Path.T * File.ident |
6168 | 30 |
end; |
31 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
32 |
structure Thy_Load: THY_LOAD = |
6168 | 33 |
struct |
34 |
||
6232 | 35 |
(* maintain load path *) |
6168 | 36 |
|
32738 | 37 |
local val load_path = Unsynchronized.ref [Path.current] in |
6168 | 38 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
17366
diff
changeset
|
39 |
fun show_path () = map Path.implode (! load_path); |
23944 | 40 |
|
33221 | 41 |
fun del_path s = |
42 |
CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s))); |
|
43 |
||
44 |
fun add_path s = |
|
45 |
CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); |
|
46 |
||
47 |
fun path_add s = |
|
48 |
CRITICAL (fn () => |
|
32738 | 49 |
(del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s]))); |
33221 | 50 |
|
37938
445e5a3244cc
eliminated obsolete/unused with_path(s) -- hardly usable because of CRITICAL;
wenzelm
parents:
37937
diff
changeset
|
51 |
fun reset_path () = CRITICAL (fn () => load_path := [Path.current]); |
6168 | 52 |
|
23944 | 53 |
fun search_path dir path = |
54 |
distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current])); |
|
55 |
||
56 |
end; |
|
57 |
||
6168 | 58 |
|
6232 | 59 |
(* file formats *) |
6168 | 60 |
|
6232 | 61 |
val ml_path = Path.ext "ML" o Path.basic; |
62 |
val thy_path = Path.ext "thy" o Path.basic; |
|
6168 | 63 |
|
29418 | 64 |
fun split_thy_path path = |
65 |
(case Path.split_ext path of |
|
66 |
(path', "thy") => (Path.dir path', Path.implode (Path.base path')) |
|
67 |
| _ => error ("Bad theory file specification " ^ Path.implode path)); |
|
68 |
||
37937 | 69 |
fun consistent_name name name' = |
70 |
if name = name' then () |
|
71 |
else error ("Filename " ^ quote (Path.implode (thy_path name)) ^ |
|
72 |
" does not agree with theory name " ^ quote name'); |
|
73 |
||
6168 | 74 |
|
23872 | 75 |
(* check files *) |
6232 | 76 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
77 |
local |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
78 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
79 |
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
|
80 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
81 |
fun try_file dir src_path = |
6232 | 82 |
let |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
83 |
val prfxs = search_path dir src_path; |
6232 | 84 |
val path = Path.expand src_path; |
23872 | 85 |
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
|
86 |
val result = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
87 |
prfxs |> get_first (fn prfx => |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
in |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
91 |
(case result of |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
92 |
SOME res => res |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
93 |
| NONE => raise NOT_FOUND (prfxs, path)) |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
94 |
end; |
6168 | 95 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
96 |
in |
6168 | 97 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
98 |
fun test_file dir file = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
99 |
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
|
100 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
101 |
fun check_file dir file = |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
102 |
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
|
103 |
error ("Could not find file " ^ quote (Path.implode path) ^ |
37943 | 104 |
"\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
|
105 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
106 |
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
|
107 |
|
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
108 |
end; |
6232 | 109 |
|
110 |
||
23872 | 111 |
(* theory deps *) |
7940 | 112 |
|
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
113 |
fun deps_thy dir name = |
23872 | 114 |
let |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
115 |
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
|
116 |
val text = File.read path; |
23872 | 117 |
val (name', imports, uses) = |
37903
b7ae269c0d68
replaced Source.of_list_limited by slightly more economic Source.of_string_limited;
wenzelm
parents:
37902
diff
changeset
|
118 |
Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text); |
37937 | 119 |
val _ = consistent_name name name'; |
24189
1fa9852643a3
simplified ThyLoad.deps_thy etc.: discontinued attached ML files;
wenzelm
parents:
24065
diff
changeset
|
120 |
val uses = map (Path.explode o #1) uses; |
24065 | 121 |
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
|
122 |
|
6168 | 123 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
124 |
(* ML files *) |
6168 | 125 |
|
23885
09254a1622e3
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23876
diff
changeset
|
126 |
fun load_ml dir raw_path = |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
127 |
let |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
128 |
val (path, id) = check_file dir raw_path; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
129 |
val _ = ML_Context.eval_file path; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37938
diff
changeset
|
130 |
in (path, id) end; |
6168 | 131 |
|
132 |
end; |
|
133 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33221
diff
changeset
|
134 |
structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load; |
32738 | 135 |
open Basic_Thy_Load; |