author  clasohm 
Sun, 24 Apr 1994 11:24:12 +0200  
changeset 341  257fcb40bacc 
parent 340  d2c66d1399c9 
child 379  c1e3c8508fd2 
permissions  rwrr 
0  1 
(* Title: Pure/Thy/read 
2 
ID: $Id$ 

3 
Author: Sonia Mahjoub / Tobias Nipkow / L C Paulson 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

4 
Copyright 1993 TU Muenchen 
0  5 

6 
Reading and writing the theory definition files. 

7 

8 
For theory XXX, the input file is called XXX.thy 

9 
the output file is called .XXX.thy.ML 

10 
and it then tries to read XXX.ML 

11 
*) 

12 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

13 
datatype thy_info = ThyInfo of {name: string, path: string, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

14 
children: string list, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

15 
thy_info: string option, ml_info: string option, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

16 
theory: Thm.theory option}; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

17 

0  18 
signature READTHY = 
19 
sig 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

20 
datatype basetype = Thy of string 
81  21 
 File of string 
74  22 

126
0b0055b3ccfe
added loaded_thys to signature and removed list_/set_loaded
clasohm
parents:
123
diff
changeset

23 
val loaded_thys : thy_info list ref 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

24 
val loadpath : string list ref 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

25 
val delete_tmpfiles: bool ref 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

26 

74  27 
val use_thy : string > unit 
28 
val update : unit > unit 

0  29 
val time_use_thy : string > unit 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

30 
val unlink_thy : string > unit 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

31 
val base_on : basetype list > string > Thm.theory 
74  32 
val store_theory : string > Thm.theory > unit 
0  33 
end; 
34 

35 

74  36 
functor ReadthyFUN (structure ThySyn: THYSYN) : READTHY = 
0  37 
struct 
38 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

39 
datatype basetype = Thy of string 
81  40 
 File of string; 
41 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

42 
val loaded_thys = ref [ThyInfo {name = "Pure", path = "", children = [], 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

43 
thy_info = Some "", ml_info = Some "", 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

44 
theory = Some Thm.pure_thy}]; 
74  45 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

46 
val loadpath = ref ["."]; (*default search path for theory files *) 
74  47 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

48 
val delete_tmpfiles = ref true; (*remove temporary files after use *) 
74  49 

50 
(*Make name of the output ML file for a theory *) 

0  51 
fun out_name thy = "." ^ thy ^ ".thy.ML"; 
52 

74  53 
(*Read a file specified by thy_file containing theory thy *) 
54 
fun read_thy thy thy_file = 

55 
let val instream = open_in thy_file; 

56 
val outstream = open_out (out_name thy) 

0  57 
in output (outstream, ThySyn.read (explode(input(instream, 999999)))); 
58 
close_out outstream; 

59 
close_in instream 

60 
end; 

61 

62 
fun file_exists file = 

63 
let val instream = open_in file in close_in instream; true end 

64 
handle Io _ => false; 

65 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

66 
(*Get thy_info for a loaded theory *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

67 
fun get_thyinfo thy = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

68 
let fun do_search (t :: loaded : thy_info list) = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

69 
let val ThyInfo {name, ...} = t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

70 
in if name = thy then Some t else do_search loaded end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

71 
 do_search [] = None 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

72 
in do_search (!loaded_thys) end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

73 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

74 
(*Replace an item by the result of make_change *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

75 
fun change_thyinfo make_change = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

76 
let fun search (t :: loaded) = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

77 
let val ThyInfo {name, path, children, thy_info, ml_info, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

78 
theory} = t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

79 
val (new_t, continue) = make_change name path children thy_info 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

80 
ml_info theory 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

81 
in if continue then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

82 
new_t :: (search loaded) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

83 
else 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

84 
new_t :: loaded 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

85 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

86 
 search [] = [] 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

87 
in loaded_thys := search (!loaded_thys) end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

88 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

89 
(*Check if a theory was already loaded *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

90 
fun already_loaded thy = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

91 
let val t = get_thyinfo thy 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

92 
in if is_none t then false 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

93 
else let val ThyInfo {thy_info, ml_info, ...} = the t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

94 
in if is_none thy_info orelse is_none ml_info then false 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

95 
else true end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

96 
end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

97 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

98 
(*Check if a theory file has changed since its last use. 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

99 
Return a pair of boolean values for .thy and for .ML *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

100 
fun thy_unchanged thy thy_file ml_file = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

101 
let val t = get_thyinfo thy 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

102 
in if is_some t then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

103 
let val ThyInfo {thy_info, ml_info, ...} = the t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

104 
val tn = is_none thy_info; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

105 
val mn = is_none ml_info 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

106 
in if not tn andalso not mn then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

107 
((file_info thy_file = the thy_info), 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

108 
(file_info ml_file = the ml_info)) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

109 
else if not tn andalso mn then (true, false) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

110 
else (false, false) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

111 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

112 
else (false, false) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

113 
end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

114 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

115 
exception FILE_NOT_FOUND; (*raised by find_file *) 
74  116 

117 
(*Find a file using a list of paths if no absolute or relative path is 

118 
specified.*) 

119 
fun find_file "" name = 

120 
let fun find_it (curr :: paths) = 

121 
if file_exists (tack_on curr name) then 

122 
tack_on curr name 

123 
else 

124 
find_it paths 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

125 
 find_it [] = "" 
74  126 
in find_it (!loadpath) end 
127 
 find_file path name = 

128 
if file_exists (tack_on path name) then tack_on path name 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

129 
else ""; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

130 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

131 
(*Get absolute pathnames for a new or already loaded theory *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

132 
fun get_filenames path name = 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

133 
let fun make_absolute file = 
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

134 
if file = "" then "" else 
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

135 
if hd (explode file) = "/" then file else tack_on (pwd ()) file; 
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

136 

e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

137 
fun new_filename () = 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

138 
let val found = find_file path (name ^ ".thy") 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

139 
handle FILE_NOT_FOUND => ""; 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

140 
val thy_file = make_absolute found; 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

141 
val (thy_path, _) = split_filename thy_file; 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

142 
val found = find_file path (name ^ ".ML"); 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

143 
val ml_file = if thy_file = "" then make_absolute found 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

144 
else if file_exists (tack_on thy_path (name ^ ".ML")) 
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

145 
then tack_on thy_path (name ^ ".ML") 
249
ec0b34154a6e
made error message "file not found" more informative
clasohm
parents:
221
diff
changeset

146 
else ""; 
ec0b34154a6e
made error message "file not found" more informative
clasohm
parents:
221
diff
changeset

147 
val searched_dirs = if path = "" then (!loadpath) else [path] 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

148 
in if thy_file = "" andalso ml_file = "" then 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

149 
error ("Could not find file \"" ^ name ^ ".thy\" or \"" 
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

150 
^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" 
249
ec0b34154a6e
made error message "file not found" more informative
clasohm
parents:
221
diff
changeset

151 
^ "in the following directories: \"" ^ 
ec0b34154a6e
made error message "file not found" more informative
clasohm
parents:
221
diff
changeset

152 
(space_implode "\", \"" searched_dirs) ^ "\"") 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

153 
else (); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

154 
(thy_file, ml_file) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

155 
end; 
74  156 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

157 
val thy = get_thyinfo name 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

158 
in if is_some thy andalso path = "" then 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

159 
let val ThyInfo {path = abs_path, ...} = the thy; 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

160 
val (thy_file, ml_file) = if abs_path = "" then new_filename () 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

161 
else (find_file abs_path (name ^ ".thy"), 
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

162 
find_file abs_path (name ^ ".ML")) 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

163 
in if thy_file = "" andalso ml_file = "" then 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

164 
(writeln ("Warning: File \"" ^ (tack_on path name) 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

165 
^ ".thy\"\ncontaining theory \"" ^ name 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

166 
^ "\" no longer exists."); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

167 
new_filename () 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

168 
) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

169 
else (thy_file, ml_file) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

170 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

171 
else new_filename () 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

172 
end; 
74  173 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

174 
(*Remove theory from all child lists in loaded_thys *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

175 
fun unlink_thy thy = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

176 
let fun remove name path children thy_info ml_info theory = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

177 
(ThyInfo {name = name, path = path, children = children \ thy, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

178 
thy_info = thy_info, ml_info = ml_info, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

179 
theory = theory}, true) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

180 
in change_thyinfo remove end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

181 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

182 
(*Remove a theory from loaded_thys *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

183 
fun remove_thy thy = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

184 
let fun remove (t :: ts) = 
74  185 
let val ThyInfo {name, ...} = t 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

186 
in if name = thy then ts 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

187 
else t :: (remove ts) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

188 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

189 
 remove [] = [] 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

190 
in loaded_thys := remove (!loaded_thys) end; 
74  191 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

192 
(*Change thy_info and ml_info for an existent item *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

193 
fun set_info thy_new ml_new thy = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

194 
let fun change name path children thy_info ml_info theory = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

195 
if name = thy then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

196 
(ThyInfo {name = name, path = path, children = children, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

197 
thy_info = Some thy_new, ml_info = Some ml_new, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

198 
theory = theory}, false) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

199 
else 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

200 
(ThyInfo {name = name, path = path, children = children, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

201 
thy_info = thy_info, ml_info = ml_info, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

202 
theory = theory}, true) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

203 
in change_thyinfo change end; 
74  204 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

205 
(*Mark theory as changed since last read if it has been completly read *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

206 
fun mark_outdated thy = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

207 
if already_loaded thy then set_info "" "" thy 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

208 
else (); 
74  209 

210 
(*Read .thy and .ML files that haven't been read yet or have changed since 

211 
they were last read; 

212 
loaded_thys is a thy_info list ref containing all theories that have 

213 
completly been read by this and preceeding use_thy calls. 

81  214 
If a theory changed since its last use its children are marked as changed *) 
74  215 
fun use_thy name = 
216 
let val (path, thy_name) = split_filename name; 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

217 
val (thy_file, ml_file) = get_filenames path thy_name; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

218 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

219 
else split_filename thy_file; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

220 
val (thy_uptodate, ml_uptodate) = thy_unchanged thy_name 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

221 
thy_file ml_file; 
0  222 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

223 
(*Set absolute path for loaded theory *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

224 
fun set_path () = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

225 
let fun change name path children thy_info ml_info theory = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

226 
if name = thy_name then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

227 
(ThyInfo {name = name, path = abs_path, children = children, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

228 
thy_info = thy_info, ml_info = ml_info, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

229 
theory = theory}, false) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

230 
else 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

231 
(ThyInfo {name = name, path = path, children = children, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

232 
thy_info = thy_info, ml_info = ml_info, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

233 
theory = theory}, true) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

234 
in change_thyinfo change end; 
74  235 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

236 
(*Mark all direct descendants of a theory as changed *) 
81  237 
fun mark_children thy = 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

238 
let val ThyInfo {children, ...} = the (get_thyinfo thy) 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

239 
val loaded = filter already_loaded children 
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

240 
in if loaded <> [] then 
81  241 
(writeln ("The following children of theory " ^ (quote thy) 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

242 
^ " are now outofdate: " 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

243 
^ (quote (space_implode "\",\"" loaded))); 
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

244 
seq mark_outdated loaded 
81  245 
) 
246 
else () 

74  247 
end 
248 

249 
in if thy_uptodate andalso ml_uptodate then () 

250 
else 

251 
( 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

252 
if thy_uptodate orelse thy_file = "" then () 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

253 
else (writeln ("Reading \"" ^ name ^ ".thy\""); 
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

254 
read_thy thy_name thy_file; 
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

255 
use (out_name thy_name) 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

256 
); 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

257 

e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

258 
if ml_file = "" then () 
340
d2c66d1399c9
changed convention for theory file names: they now have to consist of the
clasohm
parents:
269
diff
changeset

259 
else (writeln ("Reading \"" ^ name ^ ".ML\""); 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

260 
use ml_file); 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

261 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

262 
let val outstream = open_out ".tmp.ML" 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

263 
in 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

264 
output (outstream, "store_theory " ^ quote thy_name ^ " " 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

265 
^ thy_name ^ ".thy;\n"); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

266 
close_out outstream 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

267 
end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

268 
use ".tmp.ML"; 
74  269 

269
237d57b956c1
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm
parents:
249
diff
changeset

270 
(*Now set the correct info*) 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

271 
set_info (file_info thy_file) (file_info ml_file) thy_name; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

272 
set_path (); 
74  273 

269
237d57b956c1
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm
parents:
249
diff
changeset

274 
(*Mark theories that have to be reloaded*) 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

275 
mark_children thy_name; 
74  276 

269
237d57b956c1
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm
parents:
249
diff
changeset

277 
(*Remove temporary files*) 
237d57b956c1
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm
parents:
249
diff
changeset

278 
if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 
237d57b956c1
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm
parents:
249
diff
changeset

279 
then () 
341  280 
else delete_file (out_name thy_name); 
269
237d57b956c1
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
clasohm
parents:
249
diff
changeset

281 
delete_file ".tmp.ML" 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

282 
) 
0  283 
end; 
284 

285 
fun time_use_thy tname = timeit(fn()=> 

74  286 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
287 
use_thy tname; 

288 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

289 
); 

290 

291 
(*Load all thy or ML files that have been changed and also 

292 
all theories that depend on them *) 

293 
fun update () = 

294 
let (*List theories in the order they have to be loaded *) 

295 
fun load_order [] result = result 

296 
 load_order thys result = 

297 
let fun next_level (t :: ts) = 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

298 
let val thy = get_thyinfo t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

299 
in if is_some thy then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

300 
let val ThyInfo {children, ...} = the thy 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

301 
in children union (next_level ts) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

302 
end 
204
b9f087b42a44
fixed a bug in update/next_level which occured when a child wasn't loaded
clasohm
parents:
147
diff
changeset

303 
else next_level ts 
74  304 
end 
305 
 next_level [] = []; 

306 

81  307 
val children = next_level thys 
308 
in load_order children ((result \\ children) @ children) end; 

74  309 

310 
fun reload_changed (t :: ts) = 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

311 
let val thy = get_thyinfo t; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

312 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

313 
fun abspath () = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

314 
if is_some thy then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

315 
let val ThyInfo {path, ...} = the thy in path end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

316 
else ""; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

317 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

318 
val (thy_file, ml_file) = get_filenames (abspath ()) t; 
74  319 
val (thy_uptodate, ml_uptodate) = 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

320 
thy_unchanged t thy_file ml_file; 
74  321 
in if thy_uptodate andalso ml_uptodate then () 
322 
else use_thy t; 

323 
reload_changed ts 

324 
end 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

325 
 reload_changed [] = (); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

326 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

327 
(*Remove all theories that are no descendants of Pure. 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

328 
If there are still children in the deleted theory's list 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

329 
schedule them for reloading *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

330 
fun collect_garbage not_garbage = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

331 
let fun collect (t :: ts) = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

332 
let val ThyInfo {name, children, ...} = t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

333 
in if name mem not_garbage then collect ts 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

334 
else (writeln("Theory \"" ^ name 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

335 
^ "\" is no longer linked with Pure  removing it."); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

336 
remove_thy name; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

337 
seq mark_outdated children 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

338 
) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

339 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

340 
 collect [] = () 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

341 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

342 
in collect (!loaded_thys) end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

343 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

344 
in collect_garbage ("Pure" :: (load_order ["Pure"] [])); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

345 
reload_changed (load_order ["Pure"] []) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

346 
end; 
74  347 

348 
(*Merge theories to build a base for a new theory. 

349 
Base members are only loaded if they are missing. *) 

81  350 
fun base_on bases child = 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

351 
let (*List all descendants of a theory list *) 
81  352 
fun list_descendants (t :: ts) = 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

353 
let val tinfo = get_thyinfo t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

354 
in if is_some tinfo then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

355 
let val ThyInfo {children, ...} = the tinfo 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

356 
in children union (list_descendants (ts union children)) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

357 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

358 
else [] 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

359 
end 
81  360 
 list_descendants [] = []; 
74  361 

81  362 
(*Show the cycle that would be created by add_child *) 
363 
fun show_cycle base = 

364 
let fun find_it result curr = 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

365 
let val tinfo = get_thyinfo curr 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

366 
in if base = curr then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

367 
error ("Cyclic dependency of theories: " 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

368 
^ child ^ ">" ^ base ^ result) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

369 
else if is_some tinfo then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

370 
let val ThyInfo {children, ...} = the tinfo 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

371 
in seq (find_it (">" ^ curr ^ result)) children 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

372 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

373 
else () 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

374 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

375 
in find_it "" child end; 
81  376 

377 
(*Check if a cycle will be created by add_child *) 

378 
fun find_cycle base = 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

379 
if base mem (list_descendants [child]) then show_cycle base 
81  380 
else (); 
381 

382 
(*Add child to child list of base *) 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

383 
fun add_child base = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

384 
let fun add (t :: loaded) = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

385 
let val ThyInfo {name, path, children, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

386 
thy_info, ml_info, theory} = t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

387 
in if name = base then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

388 
ThyInfo {name = name, path = path, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

389 
children = child ins children, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

390 
thy_info = thy_info, ml_info = ml_info, 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

391 
theory = theory} :: loaded 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

392 
else 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

393 
t :: (add loaded) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

394 
end 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

395 
 add [] = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

396 
[ThyInfo {name = base, path = "", children = [child], 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

397 
thy_info = None, ml_info = None, theory = None}] 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

398 
in loaded_thys := add (!loaded_thys) end; 
74  399 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

400 
(*Load a base theory if not already done 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

401 
and no cycle would be created *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

402 
fun load base = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

403 
let val thy_present = already_loaded base 
74  404 
(*test this before child is added *) 
405 
in 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

406 
if child = base then 
74  407 
error ("Cyclic dependency of theories: " ^ child 
408 
^ ">" ^ child) 

81  409 
else 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

410 
(find_cycle base; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

411 
add_child base; 
81  412 
if thy_present then () 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

413 
else (writeln ("Autoloading theory " ^ (quote base) 
81  414 
^ " (used by " ^ (quote child) ^ ")"); 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

415 
use_thy base) 
81  416 
) 
417 
end; 

418 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

419 
(*Load all needed files and make a list of all real theories *) 
81  420 
fun load_base (Thy b :: bs) = 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

421 
(load b; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

422 
b :: (load_base bs)) 
81  423 
 load_base (File b :: bs) = 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

424 
(load b; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

425 
load_base bs) (*don't add it to merge_theories' parameter *) 
81  426 
 load_base [] = []; 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

427 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

428 
(*Get theory object for a loaded theory *) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

429 
fun get_theory name = 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

430 
let val ThyInfo {theory, ...} = the (get_thyinfo name) 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

431 
in the theory end; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

432 

0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

433 
val mergelist = (unlink_thy child; 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

434 
load_base bases); 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

435 
val (t :: ts) = if mergelist = [] then ["Pure"] else mergelist 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

436 
(*we have to return something *) 
147
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

437 
in writeln ("Loading theory " ^ (quote child)); 
e8d8fa0ddcef
fixed a bug in get_filenames, changed output of use_thy
clasohm
parents:
126
diff
changeset

438 
foldl Thm.merge_theories (get_theory t, map get_theory ts) end; 
74  439 

440 
(*Change theory object for an existent item of loaded_thys 

441 
or create a new item *) 

442 
fun store_theory thy_name thy = 

443 
let fun make_change (t :: loaded) = 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

444 
let val ThyInfo {name, path, children, thy_info, ml_info, ...} = t 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

445 
in if name = thy_name then 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

446 
ThyInfo {name = name, path = path, children = children, 
74  447 
thy_info = thy_info, ml_info = ml_info, 
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

448 
theory = Some thy} :: loaded 
74  449 
else 
450 
t :: (make_change loaded) 

451 
end 

452 
 make_change [] = 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

453 
[ThyInfo {name = thy_name, path = "", children = [], 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

454 
thy_info = Some "", ml_info = Some "", 
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

455 
theory = Some thy}] 
74  456 
in loaded_thys := make_change (!loaded_thys) end; 
457 

123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset

458 
end 
74  459 