equal
deleted
inserted
replaced
1 (* Title: Pure/Thy/thy_load.ML |
1 (* Title: Pure/Thy/thy_load.ML |
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
4 |
3 |
5 Theory loader primitives, including load path. |
4 Theory loader primitives, including load path. |
6 *) |
5 *) |
7 |
6 |
20 sig |
19 sig |
21 include BASIC_THY_LOAD |
20 include BASIC_THY_LOAD |
22 val ml_exts: string list |
21 val ml_exts: string list |
23 val ml_path: string -> Path.T |
22 val ml_path: string -> Path.T |
24 val thy_path: string -> Path.T |
23 val thy_path: string -> Path.T |
|
24 val split_thy_path: Path.T -> Path.T * string |
25 val check_file: Path.T -> Path.T -> (Path.T * File.ident) option |
25 val check_file: Path.T -> Path.T -> (Path.T * File.ident) option |
26 val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option |
26 val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option |
27 val check_thy: Path.T -> string -> Path.T * File.ident |
27 val check_thy: Path.T -> string -> Path.T * File.ident |
28 val deps_thy: Path.T -> string -> |
28 val deps_thy: Path.T -> string -> |
29 {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list} |
29 {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list} |
59 (* file formats *) |
59 (* file formats *) |
60 |
60 |
61 val ml_exts = ["ML", "sml"]; |
61 val ml_exts = ["ML", "sml"]; |
62 val ml_path = Path.ext "ML" o Path.basic; |
62 val ml_path = Path.ext "ML" o Path.basic; |
63 val thy_path = Path.ext "thy" o Path.basic; |
63 val thy_path = Path.ext "thy" o Path.basic; |
|
64 |
|
65 fun split_thy_path path = |
|
66 (case Path.split_ext path of |
|
67 (path', "thy") => (Path.dir path', Path.implode (Path.base path')) |
|
68 | _ => error ("Bad theory file specification " ^ Path.implode path)); |
64 |
69 |
65 |
70 |
66 (* check files *) |
71 (* check files *) |
67 |
72 |
68 fun check_ext exts paths dir src_path = |
73 fun check_ext exts paths dir src_path = |