author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 397  48cb3fa4bc59 
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 

397  262 
use_string ["store_theory " ^ quote thy_name ^ " " ^ thy_name 
263 
^ ".thy;"]; 

74  264 

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

265 
(*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

266 
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

267 
set_path (); 
74  268 

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

269 
(*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

270 
mark_children thy_name; 
74  271 

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

272 
(*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

273 
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

274 
then () 
379
c1e3c8508fd2
use_thy now uses use_string instead of creating a temporary file
clasohm
parents:
341
diff
changeset

275 
else delete_file (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

276 
) 
0  277 
end; 
278 

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

74  280 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
281 
use_thy tname; 

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

283 
); 

284 

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

286 
all theories that depend on them *) 

287 
fun update () = 

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

289 
fun load_order [] result = result 

290 
 load_order thys result = 

291 
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

292 
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

293 
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

294 
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

295 
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

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

297 
else next_level ts 
74  298 
end 
299 
 next_level [] = []; 

300 

81  301 
val children = next_level thys 
302 
in load_order children ((result \\ children) @ children) end; 

74  303 

304 
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

305 
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

306 

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

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

308 
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

309 
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

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

311 

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

312 
val (thy_file, ml_file) = get_filenames (abspath ()) t; 
74  313 
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

314 
thy_unchanged t thy_file ml_file; 
74  315 
in if thy_uptodate andalso ml_uptodate then () 
316 
else use_thy t; 

317 
reload_changed ts 

318 
end 

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

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

320 

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

321 
(*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

322 
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

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

324 
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

325 
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

326 
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

327 
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

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

329 
^ "\" 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

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

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

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

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

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

335 

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

336 
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

337 

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

338 
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

339 
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

340 
end; 
74  341 

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

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

81  344 
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

345 
let (*List all descendants of a theory list *) 
81  346 
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

347 
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

348 
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

349 
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

350 
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

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

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

353 
end 
81  354 
 list_descendants [] = []; 
74  355 

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

358 
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

359 
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

360 
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

361 
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

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

363 
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

364 
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

365 
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

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

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

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

369 
in find_it "" child end; 
81  370 

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

372 
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

373 
if base mem (list_descendants [child]) then show_cycle base 
81  374 
else (); 
375 

376 
(*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

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

378 
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

379 
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

380 
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

381 
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

382 
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

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

384 
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

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

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

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

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

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

390 
[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

391 
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

392 
in loaded_thys := add (!loaded_thys) end; 
74  393 

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

394 
(*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

395 
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

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

397 
let val thy_present = already_loaded base 
74  398 
(*test this before child is added *) 
399 
in 

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

400 
if child = base then 
74  401 
error ("Cyclic dependency of theories: " ^ child 
402 
^ ">" ^ child) 

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

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

405 
add_child base; 
81  406 
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

407 
else (writeln ("Autoloading theory " ^ (quote base) 
81  408 
^ " (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

409 
use_thy base) 
81  410 
) 
411 
end; 

412 

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

413 
(*Load all needed files and make a list of all real theories *) 
81  414 
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

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

416 
b :: (load_base bs)) 
81  417 
 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

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

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

421 

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

422 
(*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

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

424 
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

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

426 

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

427 
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

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

429 
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

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

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

432 
foldl Thm.merge_theories (get_theory t, map get_theory ts) end; 
74  433 

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

435 
or create a new item *) 

436 
fun store_theory thy_name thy = 

437 
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

438 
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

439 
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

440 
ThyInfo {name = name, path = path, children = children, 
74  441 
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

442 
theory = Some thy} :: loaded 
74  443 
else 
444 
t :: (make_change loaded) 

445 
end 

446 
 make_change [] = 

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

447 
[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

448 
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

449 
theory = Some thy}] 
74  450 
in loaded_thys := make_change (!loaded_thys) end; 
451 

379
c1e3c8508fd2
use_thy now uses use_string instead of creating a temporary file
clasohm
parents:
341
diff
changeset

452 
end; 