author  wenzelm 
Thu, 22 Jul 2010 23:29:39 +0200  
changeset 37943  3cbd7fa164b1 
parent 37939  965537d86fcc 
child 37949  48a874444164 
permissions  rwrr 
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; 