1 (* Title: Pure/Thy/thy_load.ML
2 Author: Markus Wenzel, TU Muenchen
4 Theory loader primitives, including load path.
7 signature BASIC_THY_LOAD =
9 val show_path: unit -> string list
10 val add_path: string -> unit
11 val path_add: string -> unit
12 val del_path: string -> unit
13 val with_path: string -> ('a -> 'b) -> 'a -> 'b
14 val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
15 val reset_path: unit -> unit
20 include BASIC_THY_LOAD
21 val ml_exts: string list
22 val ml_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
26 val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
27 val check_thy: Path.T -> string -> Path.T * File.ident
28 val check_name: string -> string -> unit
29 val deps_thy: Path.T -> string ->
30 {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
31 val load_ml: Path.T -> Path.T -> Path.T * File.ident
34 structure Thy_Load: THY_LOAD =
37 (* maintain load path *)
39 local val load_path = Unsynchronized.ref [Path.current] in
41 fun show_path () = map Path.implode (! load_path);
44 CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
47 CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
51 (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
53 fun reset_path () = load_path := [Path.current];
55 fun with_paths ss f x =
57 setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
59 fun with_path s f x = with_paths [s] f x;
61 fun search_path dir path =
62 distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
69 val ml_exts = ["ML", "sml"];
70 val ml_path = Path.ext "ML" o Path.basic;
71 val thy_path = Path.ext "thy" o Path.basic;
73 fun split_thy_path path =
74 (case Path.split_ext path of
75 (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
76 | _ => error ("Bad theory file specification " ^ Path.implode path));
81 fun check_ext exts paths src_path =
83 val path = Path.expand src_path;
84 val _ = Path.is_current path andalso error "Bad file specification";
86 fun try_ext rel_path ext =
87 let val ext_path = Path.expand (Path.ext ext rel_path)
88 in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
89 fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
90 in get_first try_prfx paths end;
92 fun check_file dir path = check_ext [] (search_path dir path) path;
93 fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
95 fun check_thy dir name =
97 val thy_file = thy_path name;
98 val paths = search_path dir thy_file;
100 (case check_ext [] paths thy_file of
101 NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
102 " in " ^ commas_quote (map Path.implode paths))
103 | SOME thy_id => thy_id)
106 fun check_name name name' =
107 if name = name' then ()
108 else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
109 " does not agree with theory name " ^ quote name');
114 fun deps_thy dir name =
116 val master as (path, _) = check_thy dir name;
117 val text = explode (File.read path);
118 val (name', imports, uses) =
119 Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
120 val _ = check_name name name';
121 val uses = map (Path.explode o #1) uses;
122 in {master = master, text = text, imports = imports, uses = uses} end;
127 fun load_ml dir raw_path =
128 (case check_ml dir raw_path of
129 NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
130 | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
134 structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;