15 |
15 |
16 signature THY_LOAD = |
16 signature THY_LOAD = |
17 sig |
17 sig |
18 include BASIC_THY_LOAD |
18 include BASIC_THY_LOAD |
19 val ml_path: string -> Path.T |
19 val ml_path: string -> Path.T |
20 val find_file: Path.T -> (Path.T * File.info) option |
20 val check_file: Path.T -> (Path.T * File.info) option |
21 val check_file: Path.T -> File.info option |
21 val load_file: Path.T -> (Path.T * File.info) |
22 val load_file: Path.T -> File.info |
22 val check_thy: string -> bool -> (Path.T * File.info) list |
23 val check_thy: string -> bool -> File.info |
23 val deps_thy: string -> bool -> (Path.T * File.info) list * (string list * Path.T list) |
24 val deps_thy: string -> bool -> File.info * (string list * Path.T list) |
24 val load_thy: string -> bool -> bool -> (Path.T * File.info) list |
25 val load_thy: string -> bool -> bool -> File.info |
|
26 end; |
25 end; |
27 |
26 |
28 signature PRIVATE_THY_LOAD = |
27 signature PRIVATE_THY_LOAD = |
29 sig |
28 sig |
30 include THY_LOAD |
29 include THY_LOAD |
34 |
33 |
35 structure ThyLoad: PRIVATE_THY_LOAD = |
34 structure ThyLoad: PRIVATE_THY_LOAD = |
36 struct |
35 struct |
37 |
36 |
38 |
37 |
39 (* load path *) |
38 (* maintain load path *) |
40 |
39 |
41 val load_path = ref [Path.current]; |
40 val load_path = ref [Path.current]; |
42 fun change_path f = load_path := f (! load_path); |
41 fun change_path f = load_path := f (! load_path); |
43 |
42 |
44 fun show_path () = map Path.pack (! load_path); |
43 fun show_path () = map Path.pack (! load_path); |
45 fun add_path s = change_path (fn path => path @ [Path.unpack s]); |
44 fun add_path s = change_path (fn path => path @ [Path.unpack s]); |
46 fun del_path s = change_path (filter_out (equal (Path.unpack s))); |
45 fun del_path s = change_path (filter_out (equal (Path.unpack s))); |
47 fun reset_path () = load_path := [Path.current]; |
46 fun reset_path () = load_path := [Path.current]; |
48 |
47 |
49 |
48 |
50 (* find / check file *) |
49 (* file formats *) |
51 |
50 |
52 fun find_file file_src = |
51 val ml_exts = ["", "ML", "sml"]; |
53 let |
52 val ml_path = Path.ext "ML" o Path.basic; |
54 val file = Path.expand file_src; |
53 val thy_path = Path.ext "thy" o Path.basic; |
55 fun find dir = |
|
56 let val full_path = Path.append dir file |
|
57 in apsome (pair full_path) (File.info full_path) end; |
|
58 in get_first find (if Path.is_basic file then ! load_path else [Path.current]) end; |
|
59 |
54 |
60 |
55 |
61 (* process ML files *) |
56 (* check_file *) |
62 |
57 |
63 val check_file = apsome #2 o find_file; |
58 fun check_file src_path = |
|
59 let |
|
60 val path = Path.expand src_path; |
|
61 |
|
62 fun find_ext rel_path ext = |
|
63 let val ext_path = Path.ext ext rel_path |
|
64 in apsome (fn info => (File.full_path ext_path, info)) (File.info ext_path) end; |
|
65 |
|
66 fun find_dir dir = |
|
67 get_first (find_ext (Path.append dir path)) ml_exts; |
|
68 in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end; |
|
69 |
|
70 |
|
71 (* load_file *) |
64 |
72 |
65 fun load_file raw_path = |
73 fun load_file raw_path = |
66 (case find_file raw_path of |
74 (case check_file raw_path of |
67 Some (path, info) => (Use.use_path path; info) |
75 None => error ("Could not find ML file " ^ quote (Path.pack raw_path)) |
68 | None => error ("Could not find ML file " ^ quote (Path.pack raw_path))); |
76 | Some (path, info) => (Symbol.use path; (path, info))); |
69 |
77 |
70 val ml_path = Path.ext "ML" o Path.basic; |
78 |
|
79 (* check_thy *) |
|
80 |
|
81 fun check_thy name ml = |
|
82 (case check_file (thy_path name) of |
|
83 None => error ("Could not find theory file for " ^ quote name) |
|
84 | Some thy_info => thy_info :: |
|
85 (case if ml then check_file (ml_path name) else None of |
|
86 None => [] |
|
87 | Some info => [info])); |
71 |
88 |
72 |
89 |
73 (* process theory files *) |
90 (* process theory files *) |
74 |
|
75 val thy_ext = Path.ext "thy"; |
|
76 |
|
77 fun process_thy f name = |
|
78 let val path = thy_ext (Path.basic name) in |
|
79 (case find_file path of |
|
80 Some (path, info) => (info, f path) |
|
81 | None => error ("Could not find theory file " ^ quote (Path.pack path))) |
|
82 end; |
|
83 |
91 |
84 (*hooks for theory syntax dependent operations*) |
92 (*hooks for theory syntax dependent operations*) |
85 fun undefined _ = raise Match; |
93 fun undefined _ = raise Match; |
86 val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list); |
94 val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list); |
87 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit); |
95 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit); |
88 |
96 |
89 fun check_thy name ml = |
97 fun process_thy f name ml = |
90 let val (thy_info, _) = process_thy (K ()) name in |
98 let val master = check_thy name ml |
91 (case if ml then check_file (ml_path name) else None of |
99 in (master, f (#1 (hd master))) end; |
92 None => thy_info |
|
93 | Some info => File.join_info thy_info info) |
|
94 end; |
|
95 |
100 |
96 fun deps_thy name ml = process_thy (fn path => ! deps_thy_fn name ml path) name; |
101 fun deps_thy name ml = process_thy (! deps_thy_fn name ml) name ml; |
97 fun load_thy name ml time = #1 (process_thy (fn path => ! load_thy_fn name ml time path) name); |
102 fun load_thy name ml time = #1 (process_thy (! load_thy_fn name ml time) name ml); |
98 |
103 |
99 |
104 |
100 end; |
105 end; |
101 |
106 |
102 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad; |
107 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad; |