author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 3527  b894f4c13df5 
child 3576  9cd0a0919ba0 
permissions  rwrr 
391  1 
(* Title: Pure/Thy/thy_read.ML 
2 
ID: $Id$ 

559  3 
Author: Carsten Clasohm and Markus Wenzel and Sonia Mahjoub and 
4 
Tobias Nipkow and L C Paulson 

5 
Copyright 1994 TU Muenchen 

391  6 

1242  7 
Functions for reading theory files, and storing and retrieving theories, 
8 
theorems and the global simplifier set. 

391  9 
*) 
10 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

11 
(*Types for theory storage*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

12 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

13 
(*Functions to handle arbitrary data added by the user; type "exn" is used 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

14 
to store data*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

15 
datatype thy_methods = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

16 
ThyMethods of {merge: exn list > exn, put: exn > unit, get: unit > exn}; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

17 

1291  18 
datatype thy_info = 
19 
ThyInfo of {path: string, 

20 
children: string list, parents: string list, 

21 
thy_time: string option, ml_time: string option, 

22 
theory: theory option, thms: thm Symtab.table, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

23 
methods: thy_methods Symtab.table, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

24 
data: exn Symtab.table * exn Symtab.table}; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

25 
(*thy_time, ml_time = None theory file has not been read yet 
1157  26 
= Some "" theory was read but has either been marked 
27 
as outdated or there is no such file for 

28 
this theory (see e.g. 'virtual' theories 

29 
like Pure or theories without a ML file) 

30 
theory = None theory has not been read yet 

1291  31 

32 
parents: While 'children' contains all theories the theory depends 

33 
on (i.e. also ones quoted in the .thy file), 

34 
'parents' only contains the theories which were used to form 

35 
the base of this theory. 

36 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

37 
methods: three methods for each user defined data; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

38 
merge: merges data of ancestor theories 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

39 
put: retrieves data from loaded_thys and stores it somewhere 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

40 
get: retrieves data from somewhere and stores it 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

41 
in loaded_thys 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

42 
Warning: If these functions access reference variables inside 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

43 
READTHY, they have to be redefined each time 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

44 
init_thy_reader is invoked 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

45 
data: user defined data; exn is used to allow arbitrary types; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

46 
first element of pairs contains result that get returned after 
3039
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset

47 
thy file was read, second element after ML file was read; 
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset

48 
if ML files has not been read, second element is identical to 
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset

49 
first one because get_thydata, which is meant to return the 
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset

50 
latest data, always accesses the 2nd element 
1157  51 
*) 
391  52 

412  53 
signature READTHY = 
391  54 
sig 
55 
datatype basetype = Thy of string 

56 
 File of string 

57 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

58 
val loaded_thys : thy_info Symtab.table ref 
391  59 
val loadpath : string list ref 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

60 
val thy_reader_files: string list ref 
391  61 
val delete_tmpfiles: bool ref 
62 

63 
val use_thy : string > unit 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

64 
val time_use_thy : string > unit 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

65 
val use_dir : string > unit 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

66 
val exit_use_dir : string > unit 
391  67 
val update : unit > unit 
68 
val unlink_thy : string > unit 

586
201e115d8031
renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents:
559
diff
changeset

69 
val mk_base : basetype list > string > bool > theory 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

70 
val store_theory : theory * string > unit 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

71 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

72 
val theory_of : string > theory 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

73 
val theory_of_sign : Sign.sg > theory 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

74 
val theory_of_thm : thm > theory 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

75 
val children_of : string > string list 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

76 
val parents_of_name: string > string list 
1664  77 
val thyname_of_sign: Sign.sg > string 
1291  78 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

79 
val store_thm : string * thm > thm 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

80 
val bind_thm : string * thm > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

81 
val qed : string > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

82 
val qed_thm : thm ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

83 
val qed_goal : string > theory > string 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

84 
> (thm list > tactic list) > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

85 
val qed_goalw : string > theory > thm list > string 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

86 
> (thm list > tactic list) > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

87 
val get_thm : theory > string > thm 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

88 
val thms_of : theory > (string * thm) list 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

89 
val delete_thms : string > unit 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

90 

1658
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset

91 
val add_thydata : string > string * thy_methods > unit 
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset

92 
val get_thydata : string > string > exn option 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

93 
val add_thy_reader_file: string > unit 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

94 
val set_thy_reader_file: string > unit 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

95 
val read_thy_reader_files: unit > unit 
1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

96 
val set_current_thy: string > unit 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

97 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

98 
val print_theory : theory > unit 
1291  99 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

100 
val base_path : string ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

101 
val gif_path : string ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

102 
val index_path : string ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

103 
val pure_subchart : string option ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

104 
val make_html : bool ref 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

105 
val init_html : unit > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

106 
val finish_html : unit > unit 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

107 
val section : string > unit 
391  108 
end; 
109 

110 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

111 
functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY = 
391  112 
struct 
1242  113 

114 
open ThmDB Simplifier; 

391  115 

116 
datatype basetype = Thy of string 

117 
 File of string; 

118 

1291  119 
val loaded_thys = 
120 
ref (Symtab.make [("ProtoPure", 

121 
ThyInfo {path = "", 

122 
children = ["Pure", "CPure"], parents = [], 

123 
thy_time = Some "", ml_time = Some "", 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

124 
theory = Some proto_pure_thy, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

125 
thms = Symtab.null, methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

126 
data = (Symtab.null, Symtab.null)}), 
1291  127 
("Pure", 
128 
ThyInfo {path = "", children = [], 

129 
parents = ["ProtoPure"], 

130 
thy_time = Some "", ml_time = Some "", 

131 
theory = Some pure_thy, thms = Symtab.null, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

132 
methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

133 
data = (Symtab.null, Symtab.null)}), 
1291  134 
("CPure", 
135 
ThyInfo {path = "", 

136 
children = [], parents = ["ProtoPure"], 

137 
thy_time = Some "", ml_time = Some "", 

138 
theory = Some cpure_thy, 

139 
thms = Symtab.null, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

140 
methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

141 
data = (Symtab.null, Symtab.null)}) 
1291  142 
]); 
391  143 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

144 
(*Default search path for theory files*) 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

145 
val loadpath = ref ["."]; 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

146 

35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

147 
(*Directory given as parameter to use_thy. This is temporarily added to 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

148 
loadpath while the theory's ancestors are loaded.*) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

149 
val tmp_loadpath = ref [] : string list ref; 
1291  150 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

151 
(*ML files to be read by init_thy_reader; they normally contain redefinitions 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

152 
of functions accessing reference variables inside READTHY*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

153 
val thy_reader_files = ref [] : string list ref; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

154 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

155 
(*Remove temporary files after use*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

156 
val delete_tmpfiles = ref true; 
1291  157 

391  158 

1291  159 
(*Set location of graphics for HTML files 
160 
(When this is executed for the first time we are in $ISABELLE/Pure/Thy. 

161 
This path is converted to $ISABELLE/Tools by removing the last two 

162 
directories and appending "Tools". All subsequently made ReadThy 

163 
structures inherit this value.) 

164 
*) 

165 
val gif_path = ref (tack_on ("/" ^ 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

166 
space_implode "/" (rev (tl (tl (rev (space_explode "/" 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

167 
(OS.FileSys.getDir ()))))))) 
1291  168 
"Tools"); 
169 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

170 
(*Path of Isabelle's main directory*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

171 
val base_path = ref ( 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

172 
"/" ^ space_implode "/" (rev (tl (tl (rev (space_explode "/" (OS.FileSys.getDir ()))))))); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

173 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

174 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

175 
(** HTML variables **) 
1291  176 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

177 
(*Location of .theorylist.txt and index.html (set by init_html)*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

178 
val index_path = ref ""; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

179 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

180 
(*Location of .Pure_sub.html and .CPure_sub.html*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

181 
val pure_subchart = ref (None : string option); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

182 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

183 
(*Controls whether HTML files should be generated*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

184 
val make_html = ref false; 
1291  185 

186 
(*HTML file of theory currently being read 

187 
(Initialized by thyfile2html; used by use_thy and store_thm)*) 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

188 
val cur_htmlfile = ref None : TextIO.outstream option ref; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

189 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

190 
(*Boolean variable which indicates if the title "Theorems proved in foo.ML" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

191 
has already been inserted into the current HTML file*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

192 
val cur_has_title = ref false; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

193 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

194 
(*Name of theory currently being read*) 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

195 
val cur_thyname = ref ""; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

196 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

197 

391  198 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

199 
(*Make name of the TextIO.output ML file for a theory *) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

200 
fun out_name tname = "." ^ tname ^ ".thy.ML"; 
391  201 

202 
(*Read a file specified by thy_file containing theory thy *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

203 
fun read_thy tname thy_file = 
559  204 
let 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

205 
val instream = TextIO.openIn thy_file; 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

206 
val outstream = TextIO.openOut (out_name tname); 
559  207 
in 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

208 
TextIO.output (outstream, ThySyn.parse tname (TextIO.inputAll instream)); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

209 
TextIO.closeOut outstream; 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

210 
TextIO.closeIn instream 
391  211 
end; 
212 

1480  213 
fun file_exists file = (file_info file <> ""); 
391  214 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

215 
(*Get last directory in path (e.g. /usr/proj/isabelle > isabelle) *) 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

216 
fun last_path s = case space_explode "/" s of 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

217 
[] => "" 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

218 
 ds => last_elem ds; 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

219 

391  220 
(*Get thy_info for a loaded theory *) 
559  221 
fun get_thyinfo tname = Symtab.lookup (!loaded_thys, tname); 
391  222 

971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

223 
(*Check if a theory was completly loaded *) 
391  224 
fun already_loaded thy = 
225 
let val t = get_thyinfo thy 

226 
in if is_none t then false 

971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

227 
else let val ThyInfo {thy_time, ml_time, ...} = the t 
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

228 
in is_some thy_time andalso is_some ml_time end 
391  229 
end; 
230 

231 
(*Check if a theory file has changed since its last use. 

232 
Return a pair of boolean values for .thy and for .ML *) 

559  233 
fun thy_unchanged thy thy_file ml_file = 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

234 
case get_thyinfo thy of 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

235 
Some (ThyInfo {thy_time, ml_time, ...}) => 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

236 
let val tn = is_none thy_time; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

237 
val mn = is_none ml_time 
391  238 
in if not tn andalso not mn then 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

239 
((file_info thy_file = the thy_time), 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

240 
(file_info ml_file = the ml_time)) 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

241 
else if not tn andalso mn then 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

242 
(file_info thy_file = the thy_time, false) 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

243 
else 
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

244 
(false, false) 
391  245 
end 
1098
487089cb173e
fixed bug in thy_unchanged that occurred when the .thy file was changed
clasohm
parents:
971
diff
changeset

246 
 None => (false, false) 
391  247 

1291  248 
(*Get all direct descendants of a theory*) 
249 
fun children_of t = 

250 
case get_thyinfo t of Some (ThyInfo {children, ...}) => children 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

251 
 None => []; 
1291  252 

1242  253 
(*Get all direct ancestors of a theory*) 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

254 
fun parents_of_name t = 
1291  255 
case get_thyinfo t of Some (ThyInfo {parents, ...}) => parents 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

256 
 None => []; 
1242  257 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

258 
(*Get all descendants of a theory list *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

259 
fun get_descendants [] = [] 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

260 
 get_descendants (t :: ts) = 
1291  261 
let val children = children_of t 
262 
in children union (get_descendants (children union ts)) end; 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

263 

1242  264 
(*Get theory object for a loaded theory *) 
1291  265 
fun theory_of name = 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

266 
case get_thyinfo name of Some (ThyInfo {theory = Some t, ...}) => t 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

267 
 _ => error ("Theory " ^ name ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

268 
" not stored by loader"); 
1242  269 

1291  270 
(*Get path where theory's files are located*) 
271 
fun path_of tname = 

272 
let val ThyInfo {path, ...} = the (get_thyinfo tname) 

273 
in path end; 

274 

391  275 
(*Find a file using a list of paths if no absolute or relative path is 
276 
specified.*) 

277 
fun find_file "" name = 

1291  278 
let fun find_it (cur :: paths) = 
279 
if file_exists (tack_on cur name) then 

280 
(if cur = "." then name else tack_on cur name) 

559  281 
else 
1291  282 
find_it paths 
391  283 
 find_it [] = "" 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

284 
in find_it (!tmp_loadpath @ !loadpath) end 
391  285 
 find_file path name = 
286 
if file_exists (tack_on path name) then tack_on path name 

287 
else ""; 

288 

289 
(*Get absolute pathnames for a new or already loaded theory *) 

290 
fun get_filenames path name = 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

291 
let fun new_filename () = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

292 
let val found = find_file path (name ^ ".thy"); 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

293 
val absolute_path = absolute_path (OS.FileSys.getDir ()); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

294 
val thy_file = absolute_path found; 
391  295 
val (thy_path, _) = split_filename thy_file; 
296 
val found = find_file path (name ^ ".ML"); 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

297 
val ml_file = if thy_file = "" then absolute_path found 
391  298 
else if file_exists (tack_on thy_path (name ^ ".ML")) 
299 
then tack_on thy_path (name ^ ".ML") 

300 
else ""; 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

301 
val searched_dirs = if path = "" then (!tmp_loadpath @ !loadpath) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

302 
else [path] 
391  303 
in if thy_file = "" andalso ml_file = "" then 
304 
error ("Could not find file \"" ^ name ^ ".thy\" or \"" 

305 
^ name ^ ".ML\" for theory \"" ^ name ^ "\"\n" 

306 
^ "in the following directories: \"" ^ 

307 
(space_implode "\", \"" searched_dirs) ^ "\"") 

308 
else (); 

559  309 
(thy_file, ml_file) 
391  310 
end; 
311 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

312 
val tinfo = get_thyinfo name; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

313 
in if is_some tinfo andalso path = "" then 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

314 
let val ThyInfo {path = abs_path, ...} = the tinfo; 
391  315 
val (thy_file, ml_file) = if abs_path = "" then new_filename () 
316 
else (find_file abs_path (name ^ ".thy"), 

317 
find_file abs_path (name ^ ".ML")) 

318 
in if thy_file = "" andalso ml_file = "" then 

1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

319 
(warning ("File \"" ^ (tack_on path name) 
391  320 
^ ".thy\"\ncontaining theory \"" ^ name 
321 
^ "\" no longer exists."); 

322 
new_filename () 

323 
) 

324 
else (thy_file, ml_file) 

325 
end 

326 
else new_filename () 

327 
end; 

328 

329 
(*Remove theory from all child lists in loaded_thys *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

330 
fun unlink_thy tname = 
1291  331 
let fun remove (ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

332 
theory, thms, methods, data}) = 
1291  333 
ThyInfo {path = path, children = children \ tname, parents = parents, 
1242  334 
thy_time = thy_time, ml_time = ml_time, theory = theory, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

335 
thms = thms, methods = methods, data = data} 
559  336 
in loaded_thys := Symtab.map remove (!loaded_thys) end; 
391  337 

338 
(*Remove a theory from loaded_thys *) 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

339 
fun remove_thy tname = 
559  340 
loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname) 
341 
(Symtab.dest (!loaded_thys))); 

391  342 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

343 
(*Change thy_time and ml_time for an existent item *) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

344 
fun set_info tname thy_time ml_time = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

345 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
1291  346 
Some (ThyInfo {path, children, parents, theory, thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

347 
methods, data, ...}) => 
1291  348 
ThyInfo {path = path, children = children, parents = parents, 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

349 
thy_time = thy_time, ml_time = ml_time, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

350 
theory = theory, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

351 
methods = methods, data = data} 
1291  352 
 None => error ("set_info: theory " ^ tname ^ " not found"); 
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

353 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; 
391  354 

355 
(*Mark theory as changed since last read if it has been completly read *) 

559  356 
fun mark_outdated tname = 
971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

357 
let val t = get_thyinfo tname; 
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

358 
in if is_none t then () 
1291  359 
else 
360 
let val ThyInfo {thy_time, ml_time, ...} = the t 

361 
in set_info tname (if is_none thy_time then None else Some "") 

362 
(if is_none ml_time then None else Some "") 

363 
end 

971
f4815812665b
fixed bug: parent theory wasn't loaded if .thy file was completly read before
clasohm
parents:
922
diff
changeset

364 
end; 
391  365 

1530  366 
(*Remove theorems associated with a theory from theory and theorem database*) 
367 
fun delete_thms tname = 

368 
let 

369 
val tinfo = case get_thyinfo tname of 

370 
Some (ThyInfo {path, children, parents, thy_time, ml_time, theory, 

371 
methods, data, ...}) => 

372 
ThyInfo {path = path, children = children, parents = parents, 

373 
thy_time = thy_time, ml_time = ml_time, 

374 
theory = theory, thms = Symtab.null, 

375 
methods = methods, data = data} 

1554  376 
 None => error ("Theory " ^ tname ^ " not stored by loader"); 
1530  377 

378 
val ThyInfo {theory, ...} = tinfo; 

379 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys); 

380 
case theory of 

381 
Some t => delete_thm_db t 

382 
 None => () 

383 
end; 

384 

1291  385 
(*Make head of HTML dependency charts 
386 
Parameters are: 

387 
file: HTML file 

388 
tname: theory name 

389 
suffix: suffix of complementary chart 

390 
(sup if this head is for a subchart, sub if it is for a supchart; 

391 
empty for Pure and CPure subcharts) 

392 
gif_path: relative path to directory containing GIFs 

1313  393 
index_path: relative path to directory containing main theory chart 
1291  394 
*) 
1317  395 
fun mk_charthead file tname title repeats gif_path index_path package = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

396 
TextIO.output (file, 
1291  397 
"<HTML><HEAD><TITLE>" ^ title ^ " of " ^ tname ^ 
398 
"</TITLE></HEAD>\n<H2>" ^ title ^ " of theory " ^ tname ^ 

399 
"</H2>\nThe name of every theory is linked to its theory file<BR>\n" ^ 

400 
"<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ 

401 
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ 

402 
\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ 

403 
\\" ALT = /\\></A> stands for supertheories (parent theories)\n" ^ 

1317  404 
(if not repeats then "" else 
405 
"<BR><TT>...</TT> stands for repeated subtrees") ^ 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

406 
"<P>\n<A HREF = \"" ^ tack_on index_path "index.html\ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

407 
\\">Back</A> to the index of " ^ package ^ "\n<HR>\n<PRE>"); 
1291  408 

409 
(*Convert .thy file to HTML and make chart of its supertheories*) 

410 
fun thyfile2html tpath tname = 

411 
let 

412 
val gif_path = relative_path tpath (!gif_path); 

1408  413 

414 
(*Determine name of current logic; if index_path is no subdirectory of 

415 
base_path then we take the last directory of index_path*) 

1317  416 
val package = 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

417 
if (!index_path) = "" then 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

418 
error "index_path is empty. Please use 'init_html()' instead of \ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

419 
\'make_html := true'" 
1408  420 
else if (!index_path) subdir_of (!base_path) then 
421 
relative_path (!base_path) (!index_path) 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

422 
else last_path (!index_path); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

423 
val rel_index_path = relative_path tpath (!index_path); 
1291  424 

425 
(*Make list of all theories and all theories that own a .thy file*) 

426 
fun list_theories [] theories thy_files = (theories, thy_files) 

427 
 list_theories ((tname, ThyInfo {thy_time, ...}) :: ts) 

428 
theories thy_files = 

429 
list_theories ts (tname :: theories) 

430 
(if is_some thy_time andalso the thy_time <> "" then 

431 
tname :: thy_files 

432 
else thy_files); 

433 

434 
val (theories, thy_files) = 

435 
list_theories (Symtab.dest (!loaded_thys)) [] []; 

436 

437 
(*Do the conversion*) 

438 
fun gettext thy_file = 

439 
let 

440 
(*Convert special HTML characters ('&', '>', and '<')*) 

441 
val file = 

442 
explode (execute ("sed e 's/\\&/\\&/g' e 's/>/\\>/g' \ 

443 
\e 's/</\\</g' " ^ thy_file)); 

444 

445 
(*Isolate first (possibly nested) comment; 

446 
skip all leading whitespaces*) 

447 
val (comment, file') = 

448 
let fun first_comment ("*" :: ")" :: cs) co 1 = (co ^ "*)", cs) 

449 
 first_comment ("*" :: ")" :: cs) co d = 

450 
first_comment cs (co ^ "*)") (d1) 

451 
 first_comment ("(" :: "*" :: cs) co d = 

452 
first_comment cs (co ^ "(*") (d+1) 

453 
 first_comment (" " :: cs) "" 0 = first_comment cs "" 0 

454 
 first_comment ("\n" :: cs) "" 0 = first_comment cs "" 0 

455 
 first_comment ("\t" :: cs) "" 0 = first_comment cs "" 0 

456 
 first_comment cs "" 0 = ("", cs) 

457 
 first_comment (c :: cs) co d = 

458 
first_comment cs (co ^ implode [c]) d 

459 
 first_comment [] co _ = 

460 
error ("Unexpected end of file " ^ tname ^ ".thy."); 

461 
in first_comment file "" 0 end; 

462 

463 
(*Process line defining theory's ancestors; 

464 
convert valid theory names to links to their HTML file*) 

465 
val (ancestors, body) = 

466 
let 

467 
fun make_links l result = 

468 
let val (pre, letter) = take_prefix (not o is_letter) l; 

469 

470 
val (id, rest) = 

471 
take_prefix (is_quasi_letter orf is_digit) letter; 

472 

473 
val id = implode id; 

474 

475 
(*Make a HTML link out of a theory name*) 

476 
fun make_link t = 

477 
let val path = path_of t; 

478 
in "<A HREF = \"" ^ 

1323  479 
tack_on (relative_path tpath path) ("." ^ t) ^ 
1291  480 
".html\">" ^ t ^ "</A>" end; 
481 
in if not (id mem theories) then (result, implode l) 

482 
else if id mem thy_files then 

483 
make_links rest (result ^ implode pre ^ make_link id) 

484 
else make_links rest (result ^ implode pre ^ id) 

485 
end; 

486 

487 
val (pre, rest) = take_prefix (fn c => c <> "=") file'; 

488 

489 
val (ancestors, body) = 

490 
if null rest then 

491 
error ("Missing \"=\" in file " ^ tname ^ ".thy.\n\ 

492 
\(Make sure that the last line ends with a linebreak.)") 

493 
else 

494 
make_links rest ""; 

495 
in (implode pre ^ ancestors, body) end; 

496 
in "<HTML><HEAD><TITLE>" ^ tname ^ ".thy</TITLE></HEAD>\n\n<BODY>\n" ^ 

497 
"<H2>" ^ tname ^ ".thy</H2>\n<A HREF = \"" ^ 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

498 
tack_on rel_index_path "index.html\ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

499 
\\">Back</A> to the index of " ^ package ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

500 
"\n<HR>\n\n<PRE>\n" ^ comment ^ ancestors ^ body ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

501 
"</PRE>\n" 
1291  502 
end; 
503 

504 
(** Make chart of supertheories **) 

505 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

506 
val sup_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sup.html")); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

507 
val sub_out = TextIO.openOut (tack_on tpath ("." ^ tname ^ "_sub.html")); 
1291  508 

509 
(*Theories that already have been listed in this chart*) 

510 
val listed = ref []; 

511 

512 
val wanted_theories = 

513 
filter (fn s => s mem thy_files orelse s = "Pure" orelse s = "CPure") 

514 
theories; 

515 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

516 
(*Make tree of theory dependencies*) 
1291  517 
fun list_ancestors tname level continued = 
518 
let 

519 
fun mk_entry [] = () 

520 
 mk_entry (t::ts) = 

521 
let 

522 
val is_pure = t = "Pure" orelse t = "CPure"; 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

523 
val path = if is_pure then (the (!pure_subchart)) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

524 
else path_of t; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

525 
val rel_path = relative_path tpath path; 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

526 
val repeated = t mem (!listed) andalso 
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

527 
not (null (parents_of_name t)); 
1291  528 

529 
fun mk_offset [] cur = 

530 
if level < cur then error "Error in mk_offset" 

531 
else implode (replicate (level  cur) " ") 

532 
 mk_offset (l::ls) cur = 

533 
implode (replicate (l  cur) " ") ^ " " ^ 

534 
mk_offset ls (l+1); 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

535 
in TextIO.output (sup_out, 
1291  536 
" " ^ mk_offset continued 0 ^ 
1323  537 
"\\__" ^ (if is_pure then t else 
538 
"<A HREF=\"" ^ tack_on rel_path ("." ^ t) ^ 

539 
".html\">" ^ t ^ "</A>") ^ 

1317  540 
(if repeated then "..." else " ") ^ 
1323  541 
"<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ 
1317  542 
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  543 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>" ^ 
544 
(if is_pure then "" 

1323  545 
else "<A HREF = \"" ^ tack_on rel_path ("." ^ t) ^ 
1317  546 
"_sup.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  547 
tack_on gif_path "blue_arrow.gif\ 
1317  548 
\\" ALT = /\\></A>") ^ 
549 
"\n"); 

550 
if repeated then () 

551 
else (listed := t :: (!listed); 

1291  552 
list_ancestors t (level+1) (if null ts then continued 
553 
else continued @ [level]); 

554 
mk_entry ts) 

555 
end; 

556 

557 
val relatives = 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

558 
filter (fn s => s mem wanted_theories) (parents_of_name tname); 
1291  559 
in mk_entry relatives end; 
560 
in if is_some (!cur_htmlfile) then 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

561 
(TextIO.closeOut (the (!cur_htmlfile)); 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

562 
warning "Last theory's HTML file has not been closed.") 
1291  563 
else (); 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

564 
cur_htmlfile := Some (TextIO.openOut (tack_on tpath ("." ^ tname ^ ".html"))); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

565 
cur_has_title := false; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

566 
TextIO.output (the (!cur_htmlfile), gettext (tack_on tpath tname ^ ".thy")); 
1291  567 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

568 
mk_charthead sup_out tname "Ancestors" true gif_path rel_index_path 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

569 
package; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

570 
TextIO.output(sup_out, 
1323  571 
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ 
572 
\<A HREF = \"." ^ tname ^ 

1317  573 
"_sub.html\"><IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
1291  574 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\n"); 
575 
list_ancestors tname 0 []; 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

576 
TextIO.output (sup_out, "</PRE><HR></BODY></HTML>"); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

577 
TextIO.closeOut sup_out; 
1291  578 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

579 
mk_charthead sub_out tname "Children" false gif_path rel_index_path 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

580 
package; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

581 
TextIO.output(sub_out, 
1323  582 
"<A HREF=\"." ^ tname ^ ".html\">" ^ tname ^ "</A> \ 
583 
\<A HREF = \"." ^ tname ^ "_sup.html\"><IMG SRC = \"" ^ 

1317  584 
tack_on gif_path "blue_arrow.gif\" BORDER=0 ALT = \\/></A>\n"); 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

585 
TextIO.closeOut sub_out 
1291  586 
end; 
587 

1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

588 
(*Invoke every put method stored in a theory's methods table to initialize 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

589 
the state of user defined variables*) 
1656  590 
fun put_thydata first tname = 
1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

591 
let val (methods, data) = 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

592 
case get_thyinfo tname of 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

593 
Some (ThyInfo {methods, data, ...}) => 
1656  594 
(methods, Symtab.dest ((if first then fst else snd) data)) 
1603
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

595 
 None => error ("Theory " ^ tname ^ " not stored by loader"); 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

596 

44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

597 
fun put_data (id, date) = 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

598 
case Symtab.lookup (methods, id) of 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

599 
Some (ThyMethods {put, ...}) => put date 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

600 
 None => error ("No method defined for theory data \"" ^ 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

601 
id ^ "\""); 
44bc1417b07c
moved init_data to new public function set_current_thy
clasohm
parents:
1602
diff
changeset

602 
in seq put_data data end; 
1291  603 

1656  604 
val set_current_thy = put_thydata false; 
605 

559  606 
(*Read .thy and .ML files that haven't been read yet or have changed since 
391  607 
they were last read; 
559  608 
loaded_thys is a thy_info list ref containing all theories that have 
391  609 
completly been read by this and preceeding use_thy calls. 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

610 
tmp_loadpath is temporarily added to loadpath while the ancestors of a 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

611 
theory that the user specified as e.g. "ex/Nat" are loaded. Because of 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

612 
raised exceptions we cannot guarantee that it's value is always valid. 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

613 
Therefore this has to be assured by the first parameter of use_thy1 which 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

614 
is "true" if use_thy gets invoked by mk_base and "false" else. 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

615 
*) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

616 
fun use_thy1 tmp_loadpath_valid name = 
1242  617 
let 
618 
val (path, tname) = split_filename name; 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

619 
val dummy = (tmp_loadpath := 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

620 
(if not tmp_loadpath_valid then (if path = "" then [] else [path]) 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

621 
else !tmp_loadpath)); 
1242  622 
val (thy_file, ml_file) = get_filenames path tname; 
623 
val (abs_path, _) = if thy_file = "" then split_filename ml_file 

624 
else split_filename thy_file; 

625 
val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file; 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

626 
val old_parents = parents_of_name tname; 
391  627 

1242  628 
(*Set absolute path for loaded theory *) 
629 
fun set_path () = 

1291  630 
let val ThyInfo {children, parents, thy_time, ml_time, theory, thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

631 
methods, data, ...} = 
1242  632 
the (Symtab.lookup (!loaded_thys, tname)); 
633 
in loaded_thys := Symtab.update ((tname, 

1291  634 
ThyInfo {path = abs_path, 
635 
children = children, parents = parents, 

1242  636 
thy_time = thy_time, ml_time = ml_time, 
637 
theory = theory, thms = thms, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

638 
methods = methods, data = data}), 
1242  639 
!loaded_thys) 
640 
end; 

641 

642 
(*Mark all direct descendants of a theory as changed *) 

643 
fun mark_children thy = 

1291  644 
let val children = children_of thy; 
1242  645 
val present = filter (is_some o get_thyinfo) children; 
646 
val loaded = filter already_loaded present; 

647 
in if loaded <> [] then 

648 
writeln ("The following children of theory " ^ (quote thy) 

649 
^ " are now outofdate: " 

650 
^ (quote (space_implode "\",\"" loaded))) 

651 
else (); 

652 
seq mark_outdated present 

653 
end; 

391  654 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

655 
(*Invoke every get method stored in the methods table and store result in 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

656 
data table*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

657 
fun save_data thy_only = 
1291  658 
let val ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

659 
theory, thms, methods, data} = the (get_thyinfo tname); 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

660 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

661 
fun get_data [] data = data 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

662 
 get_data ((id, ThyMethods {get, ...}) :: ms) data = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

663 
get_data ms (Symtab.update ((id, get ()), data)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

664 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

665 
val new_data = get_data (Symtab.dest methods) Symtab.null; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

666 

3039
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset

667 
val data' = (if thy_only then new_data else fst data, new_data) 
bbf4e3738ef0
get_thydata accesses the second component of the data field. This component
nipkow
parents:
2406
diff
changeset

668 
(* 2nd component must be up to date *) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

669 
in loaded_thys := Symtab.update 
1291  670 
((tname, ThyInfo {path = path, 
671 
children = children, parents = parents, 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

672 
thy_time = thy_time, ml_time = ml_time, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

673 
theory = theory, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

674 
methods = methods, data = data'}), 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

675 
!loaded_thys) 
1242  676 
end; 
677 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

678 
(*Add theory to file listing all loaded theories (for index.html) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

679 
and to the subcharts of its parents*) 
1480  680 
local exception MK_HTML in 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

681 
fun mk_html () = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

682 
let val new_parents = parents_of_name tname \\ old_parents; 
1291  683 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

684 
fun robust_seq (proc: 'a > unit) : 'a list > unit = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

685 
let fun seqf [] = () 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

686 
 seqf (x :: xs) = (proc x handle _ => (); seqf xs) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

687 
in seqf end; 
1291  688 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

689 
(*Add child to parents' subtheory charts*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

690 
fun add_to_parents t = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

691 
let val path = if t = "Pure" orelse t = "CPure" then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

692 
(the (!pure_subchart)) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

693 
else path_of t; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

694 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

695 
val gif_path = relative_path path (!gif_path); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

696 
val rel_path = relative_path path abs_path; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

697 
val tpath = tack_on rel_path ("." ^ tname); 
1291  698 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

699 
val fname = tack_on path ("." ^ t ^ "_sub.html"); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

700 
val out = if file_exists fname then 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

701 
TextIO.openAppend fname handle e => 
1602
699ad6611c1e
fixed incompatibility of add_to_parents with SML109's new Io exceptions
clasohm
parents:
1598
diff
changeset

702 
(warning ("Unable to write to file " ^ 
699ad6611c1e
fixed incompatibility of add_to_parents with SML109's new Io exceptions
clasohm
parents:
1598
diff
changeset

703 
fname); raise e) 
1480  704 
else raise MK_HTML; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

705 
in TextIO.output (out, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

706 
" \n \\__<A HREF=\"" ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

707 
tack_on rel_path ("." ^ tname) ^ ".html\">" ^ tname ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

708 
"</A> <A HREF = \"" ^ tpath ^ "_sub.html\">\ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

709 
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

710 
tack_on gif_path "red_arrow.gif\" ALT = \\/></A>\ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

711 
\<A HREF = \"" ^ tpath ^ "_sup.html\">\ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

712 
\<IMG ALIGN=BOTTOM BORDER=0 SRC = \"" ^ 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

713 
tack_on gif_path "blue_arrow.gif\" ALT = /\\></A>\n"); 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

714 
TextIO.closeOut out 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

715 
end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

716 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

717 
val theory_list = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

718 
TextIO.openAppend (tack_on (!index_path) ".theory_list.txt") 
1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

719 
handle _ => (make_html := false; 
3527  720 
warning ("Cannot write to " ^ 
1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

721 
(!index_path) ^ " while making HTML files.\n\ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

722 
\HTML generation has been switched off.\n\ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

723 
\Call init_html() from within a \ 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

724 
\writeable directory to reactivate it."); 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

725 
raise MK_HTML) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

726 
in TextIO.output (theory_list, tname ^ " " ^ abs_path ^ "\n"); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

727 
TextIO.closeOut theory_list; 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

728 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

729 
robust_seq add_to_parents new_parents 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

730 
end 
1554  731 
end; 
732 

733 
(*Make sure that loaded_thys contains an entry for tname*) 

734 
fun init_thyinfo () = 

735 
let val tinfo = ThyInfo {path = "", children = [], parents = [], 

736 
thy_time = None, ml_time = None, 

737 
theory = None, thms = Symtab.null, 

738 
methods = Symtab.null, 

739 
data = (Symtab.null, Symtab.null)}; 

740 
in if is_some (get_thyinfo tname) then () 

741 
else loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) 

742 
end; 

1242  743 
in if thy_uptodate andalso ml_uptodate then () 
744 
else 

1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

745 
(if thy_file = "" then () 
1656  746 
else if thy_uptodate then put_thydata true tname 
391  747 
else 
1242  748 
(writeln ("Reading \"" ^ name ^ ".thy\""); 
1291  749 

1554  750 
init_thyinfo (); 
1530  751 
delete_thms tname; 
1242  752 
read_thy tname thy_file; 
2406  753 
SymbolInput.use (out_name tname); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

754 
save_data true; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

755 

1308  756 
(*Store axioms of theory 
757 
(but only if it's not a copy of an older theory)*) 

1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

758 
let val parents = parents_of_name tname; 
1308  759 
val this_thy = theory_of tname; 
760 
val axioms = 

761 
if length parents = 1 

762 
andalso Sign.eq_sg (sign_of (theory_of (hd parents)), 

763 
sign_of this_thy) then [] 

764 
else axioms_of this_thy; 

765 
in map store_thm_db axioms end; 

766 

1242  767 
if not (!delete_tmpfiles) then () 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

768 
else OS.FileSys.remove (out_name tname); 
1291  769 

770 
if not (!make_html) then () 

771 
else thyfile2html abs_path tname 

1242  772 
); 
1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

773 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

774 
set_info tname (Some (file_info thy_file)) None; 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

775 
(*mark thy_file as successfully loaded*) 
391  776 

1242  777 
if ml_file = "" then () 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

778 
else (writeln ("Reading \"" ^ name ^ ".ML\""); 
2406  779 
SymbolInput.use ml_file); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

780 
save_data false; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

781 

8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

782 
(*Store theory again because it could have been redefined*) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

783 
use_string 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

784 
["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; 
391  785 

1313  786 
(*Add theory to list of all loaded theories (for index.html) 
1291  787 
and add it to its parents' subcharts*) 
788 
if !make_html then 

789 
let val path = path_of tname; 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

790 
in if path = "" then (*first time theory has been read*) 
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

791 
(mk_html() handle MK_HTML => ()) 
1291  792 
else () 
793 
end 

794 
else (); 

795 

1242  796 
(*Now set the correct info*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

797 
set_info tname (Some (file_info thy_file)) (Some (file_info ml_file)); 
1242  798 
set_path (); 
799 

800 
(*Mark theories that have to be reloaded*) 

1291  801 
mark_children tname; 
802 

803 
(*Close HTML file*) 

804 
case !cur_htmlfile of 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

805 
Some out => (TextIO.output (out, "<HR></BODY></HTML>\n"); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

806 
TextIO.closeOut out; 
1291  807 
cur_htmlfile := None) 
808 
 None => () 

1242  809 
) 
810 
end; 

391  811 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

812 
val use_thy = use_thy1 false; 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

813 

391  814 
fun time_use_thy tname = timeit(fn()=> 
559  815 
(writeln("\n**** Starting Theory " ^ tname ^ " ****"); 
391  816 
use_thy tname; 
817 
writeln("\n**** Finished Theory " ^ tname ^ " ****")) 

818 
); 

819 

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

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

821 
all theories that depend on them.*) 
391  822 
fun update () = 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

823 
let (*List theories in the order they have to be loaded in.*) 
391  824 
fun load_order [] result = result 
825 
 load_order thys result = 

1291  826 
let fun next_level [] = [] 
827 
 next_level (t :: ts) = 

828 
let val children = children_of t 

829 
in children union (next_level ts) end; 

559  830 

1291  831 
val descendants = next_level thys; 
832 
in load_order descendants ((result \\ descendants) @ descendants) 

833 
end; 

391  834 

835 
fun reload_changed (t :: ts) = 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

836 
let val abspath = case get_thyinfo t of 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

837 
Some (ThyInfo {path, ...}) => path 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

838 
 None => ""; 
391  839 

1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

840 
val (thy_file, ml_file) = get_filenames abspath t; 
391  841 
val (thy_uptodate, ml_uptodate) = 
842 
thy_unchanged t thy_file ml_file; 

843 
in if thy_uptodate andalso ml_uptodate then () 

844 
else use_thy t; 

845 
reload_changed ts 

846 
end 

847 
 reload_changed [] = (); 

848 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

849 
(*Remove all theories that are no descendants of ProtoPure. 
391  850 
If there are still children in the deleted theory's list 
851 
schedule them for reloading *) 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

852 
fun collect_garbage no_garbage = 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

853 
let fun collect ((tname, ThyInfo {children, ...}) :: ts) = 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

854 
if tname mem no_garbage then collect ts 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

855 
else (writeln ("Theory \"" ^ tname ^ 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

856 
"\" is no longer linked with ProtoPure  removing it."); 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

857 
remove_thy tname; 
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

858 
seq mark_outdated children) 
391  859 
 collect [] = () 
559  860 
in collect (Symtab.dest (!loaded_thys)) end; 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

861 
in tmp_loadpath := []; 
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

862 
collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] [])); 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
871
diff
changeset

863 
reload_changed (load_order ["Pure", "CPure"] []) 
391  864 
end; 
865 

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

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

867 
Base members are only loaded if they are missing.*) 
586
201e115d8031
renamed base_on into mk_base and moved it to the beginning of the generated
clasohm
parents:
559
diff
changeset

868 
fun mk_base bases child mk_draft = 
1291  869 
let (*Show the cycle that would be created by add_child*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

870 
fun show_cycle base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

871 
let fun find_it result curr = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

872 
let val tinfo = get_thyinfo curr 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

873 
in if base = curr then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

874 
error ("Cyclic dependency of theories: " 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

875 
^ child ^ ">" ^ base ^ result) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

876 
else if is_some tinfo then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

877 
let val ThyInfo {children, ...} = the tinfo 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

878 
in seq (find_it (">" ^ curr ^ result)) children 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

879 
end 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

880 
else () 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

881 
end 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

882 
in find_it "" child end; 
391  883 

1291  884 
(*Check if a cycle would be created by add_child*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

885 
fun find_cycle base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

886 
if base mem (get_descendants [child]) then show_cycle base 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

887 
else (); 
559  888 

1291  889 
(*Add child to child list of base*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

890 
fun add_child base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

891 
let val tinfo = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

892 
case Symtab.lookup (!loaded_thys, base) of 
1291  893 
Some (ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

894 
theory, thms, methods, data}) => 
1291  895 
ThyInfo {path = path, 
896 
children = child ins children, parents = parents, 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

897 
thy_time = thy_time, ml_time = ml_time, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

898 
theory = theory, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

899 
methods = methods, data = data} 
1291  900 
 None => ThyInfo {path = "", children = [child], parents = [], 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

901 
thy_time = None, ml_time = None, 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

902 
theory = None, thms = Symtab.null, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

903 
methods = Symtab.null, 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

904 
data = (Symtab.null, Symtab.null)}; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

905 
in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end; 
559  906 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

907 
(*Load a base theory if not already done 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

908 
and no cycle would be created *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

909 
fun load base = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

910 
let val thy_loaded = already_loaded base 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

911 
(*test this before child is added *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

912 
in 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

913 
if child = base then 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

914 
error ("Cyclic dependency of theories: " ^ child 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

915 
^ ">" ^ child) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

916 
else 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

917 
(find_cycle base; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

918 
add_child base; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

919 
if thy_loaded then () 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

920 
else (writeln ("Autoloading theory " ^ (quote base) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

921 
^ " (used by " ^ (quote child) ^ ")"); 
1704
35045774bc1e
changed use_thy's behaviour so that if the user specifies a path for a theory
clasohm
parents:
1670
diff
changeset

922 
use_thy1 true base) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

923 
) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

924 
end; 
391  925 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

926 
(*Load all needed files and make a list of all real theories *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

927 
fun load_base (Thy b :: bs) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

928 
(load b; 
1291  929 
b :: load_base bs) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

930 
 load_base (File b :: bs) = 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

931 
(load b; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

932 
load_base bs) (*don't add it to mergelist *) 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

933 
 load_base [] = []; 
391  934 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

935 
val dummy = unlink_thy child; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

936 
val mergelist = load_base bases; 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

937 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

938 
val base_thy = (writeln ("Loading theory " ^ (quote child)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

939 
merge_thy_list mk_draft (map theory_of mergelist)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

940 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

941 
val datas = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

942 
let fun get_data t = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

943 
let val ThyInfo {data, ...} = the (get_thyinfo t) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

944 
in snd data end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

945 
in map (Symtab.dest o get_data) mergelist end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

946 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

947 
val methods = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

948 
let fun get_methods t = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

949 
let val ThyInfo {methods, ...} = the (get_thyinfo t) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

950 
in methods end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

951 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

952 
val ms = map get_methods mergelist; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

953 
in if null ms then Symtab.null 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

954 
else foldl (Symtab.merge (fn (x,y) => true)) (hd ms, tl ms) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

955 
end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

956 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

957 
(*merge two sorted association lists*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

958 
fun merge_two ([], d2) = d2 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

959 
 merge_two (d1, []) = d1 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

960 
 merge_two (l1 as ((p1 as (id1 : string, d1)) :: d1s), 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

961 
l2 as ((p2 as (id2, d2)) :: d2s)) = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

962 
if id1 < id2 then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

963 
p1 :: merge_two (d1s, l2) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

964 
else 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

965 
p2 :: merge_two (l1, d2s); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

966 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

967 
(*Merge multiple occurence of data; also call put for each merged list*) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

968 
fun merge_multi [] None = [] 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

969 
 merge_multi [] (Some (id, ds)) = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

970 
let val ThyMethods {merge, put, ...} = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

971 
the (Symtab.lookup (methods, id)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

972 
in put (merge ds); [id] end 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

973 
 merge_multi ((id, d) :: ds) None = merge_multi ds (Some (id, [d])) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

974 
 merge_multi ((id, d) :: ds) (Some (id2, d2s)) = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

975 
if id = id2 then 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

976 
merge_multi ds (Some (id2, d :: d2s)) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

977 
else 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

978 
let val ThyMethods {merge, put, ...} = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

979 
the (Symtab.lookup (methods, id2)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

980 
in put (merge d2s); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

981 
id2 :: merge_multi ds (Some (id, [d])) 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

982 
end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

983 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

984 
val merged = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

985 
if null datas then [] 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

986 
else merge_multi (foldl merge_two (hd datas, tl datas)) None; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

987 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

988 
val dummy = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

989 
let val unmerged = map fst (Symtab.dest methods) \\ merged; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

990 

ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

991 
fun put_empty id = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

992 
let val ThyMethods {merge, put, ...} = 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

993 
the (Symtab.lookup (methods, id)); 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

994 
in put (merge []) end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

995 
in seq put_empty unmerged end; 
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

996 

1291  997 
val dummy = 
998 
let val tinfo = case Symtab.lookup (!loaded_thys, child) of 

999 
Some (ThyInfo {path, children, thy_time, ml_time, theory, thms, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1000 
data, ...}) => 
1291  1001 
ThyInfo {path = path, 
1002 
children = children, parents = mergelist, 

1003 
thy_time = thy_time, ml_time = ml_time, 

1004 
theory = theory, thms = thms, 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1005 
methods = methods, data = data} 
1291  1006 
 None => error ("set_parents: theory " ^ child ^ " not found"); 
1007 
in loaded_thys := Symtab.update ((child, tinfo), !loaded_thys) end; 

1008 

1386
cf066d9b4c4f
fixed bug: cur_thyname was overwritten because of early assignment
clasohm
parents:
1378
diff
changeset

1009 
in cur_thyname := child; 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1010 
base_thy 
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1011 
end; 
391  1012 

1291  1013 
(*Change theory object for an existent item of loaded_thys*) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1014 
fun store_theory (thy, tname) = 
559  1015 
let val tinfo = case Symtab.lookup (!loaded_thys, tname) of 
1291  1016 
Some (ThyInfo {path, children, parents, thy_time, ml_time, thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1017 
methods, data, ...}) => 
1291  1018 
ThyInfo {path = path, children = children, parents = parents, 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1019 
thy_time = thy_time, ml_time = ml_time, 
1242  1020 
theory = Some thy, thms = thms, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1021 
methods = methods, data = data} 
1291  1022 
 None => error ("store_theory: theory " ^ tname ^ " not found"); 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1023 
in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end; 
559  1024 

1025 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1026 
(*** Store and retrieve theorems ***) 
1664  1027 
(*Guess the name of a theory object 
1028 
(First the quick way by looking at the stamps; if that doesn't work, 

1029 
we search loaded_thys for the first theory which fits.) 

1030 
*) 

1031 
fun thyname_of_sign sg = 

1032 
let val ref xname = hd (#stamps (Sign.rep_sg sg)); 

1033 
val opt_info = get_thyinfo xname; 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1034 

559  1035 
fun eq_sg (ThyInfo {theory = None, ...}) = false 
715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1036 
 eq_sg (ThyInfo {theory = Some thy, ...}) = Sign.eq_sg (sg,sign_of thy); 
559  1037 

1038 
val show_sg = Pretty.str_of o Sign.pretty_sg; 

1039 
in 

1664  1040 
if is_some opt_info andalso eq_sg (the opt_info) then xname 
559  1041 
else 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1042 
(case Symtab.find_first (eq_sg o snd) (!loaded_thys) of 
1664  1043 
Some (name, _) => name 
559  1044 
 None => error ("Theory " ^ show_sg sg ^ " not stored by loader")) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1045 
end; 
391  1046 

1664  1047 
(*Guess to which theory a signature belongs and return it's thy_info*) 
1048 
fun thyinfo_of_sign sg = 

1049 
let val name = thyname_of_sign sg; 

1050 
in (name, the (get_thyinfo name)) end; 

1051 

559  1052 

715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1053 
(*Try to get the theory object corresponding to a given signature*) 
559  1054 
fun theory_of_sign sg = 
1055 
(case thyinfo_of_sign sg of 

1056 
(_, ThyInfo {theory = Some thy, ...}) => thy 

1057 
 _ => sys_error "theory_of_sign"); 

476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1058 

715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1059 
(*Try to get the theory object corresponding to a given theorem*) 
559  1060 
val theory_of_thm = theory_of_sign o #sign o rep_thm; 
1061 

1062 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1063 
(** Store theorems **) 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1064 

1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1065 
(*Makes HTML title for list of theorems; as this list may be empty and we 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1066 
don't want a title in that case, mk_theorems_title is only invoked when 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1067 
something is added to the list*) 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1068 
fun mk_theorems_title out = 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1069 
if not (!cur_has_title) then 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1070 
(cur_has_title := true; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1071 
TextIO.output (out, "<HR><H2>Theorems proved in <A HREF = \"" ^ 
1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1072 
(!cur_thyname) ^ ".ML\">" ^ (!cur_thyname) ^ 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1073 
".ML</A>:</H2>\n")) 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1074 
else (); 
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1075 

1291  1076 
(*Store a theorem in the thy_info of its theory, 
1077 
and in the theory's HTML file*) 

559  1078 
fun store_thm (name, thm) = 
1079 
let 

1291  1080 
val (thy_name, ThyInfo {path, children, parents, thy_time, ml_time, 
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1081 
theory, thms, methods, data}) = 
1529  1082 
thyinfo_of_sign (#sign (rep_thm thm)) 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset

1083 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1084 
val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false) 
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset

1085 
handle Symtab.DUPLICATE s => 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1086 
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

1087 
(warning ("Theory database already contains copy of\ 
774
ea19f22ed23c
added warning for already stored theorem to store_thm
clasohm
parents:
759
diff
changeset

1088 
\ theorem " ^ quote name); 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1089 
(thms, true)) 
1236
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset

1090 
else error ("Duplicate theorem name " ^ quote s 
b54d51df9065
added check for duplicate theorems in theorem database;
clasohm
parents:
1223
diff
changeset

1091 
^ " used in theory database")); 
1291  1092 

1093 
fun thm_to_html () = 

1094 
let fun escape [] = "" 

1095 
 escape ("<"::s) = "<" ^ escape s 

1096 
 escape (">"::s) = ">" ^ escape s 

1097 
 escape ("&"::s) = "&" ^ escape s 

1098 
 escape (c::s) = c ^ escape s; 

1099 
in case !cur_htmlfile of 

1100 
Some out => 

1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset

1101 
(mk_theorems_title out; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1102 
TextIO.output (out, "<DD><EM>" ^ name ^ "</EM>\n<PRE>" ^ 
2030  1103 
escape 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1104 
(explode 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1105 
(string_of_thm (#1 (freeze_thaw thm)))) ^ 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1106 
"</PRE><P>\n") 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1107 
) 
1291  1108 
 None => () 
1109 
end; 

1529  1110 

1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1111 
(*Label this theorem*) 
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1112 
val thm' = Thm.name_thm (name, thm) 
559  1113 
in 
1114 
loaded_thys := Symtab.update 

1291  1115 
((thy_name, ThyInfo {path = path, children = children, parents = parents, 
1242  1116 
thy_time = thy_time, ml_time = ml_time, 
1117 
theory = theory, thms = thms', 

1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset

1118 
methods = methods, data = data}), 
1242  1119 
!loaded_thys); 
1291  1120 
thm_to_html (); 
1529  1121 
if duplicate then thm' else store_thm_db (name, thm') 
559  1122 
end; 
1123 

715
f76ad10f5802
added call of store_theory after thy file has been read
clasohm
parents:
586
diff
changeset

1124 
(*Store result of proof in loaded_thys and as ML value*) 
758  1125 

1126 
val qed_thm = ref flexpair_def(*dummy*); 

1127 

1128 
fun bind_thm (name, thm) = 

1529  1129 
(qed_thm := store_thm (name, (standard thm)); 
1291  1130 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
758  1131 

559  1132 
fun qed name = 
1529  1133 
(qed_thm := store_thm (name, result ()); 
1291  1134 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1135 

746  1136 
fun qed_goal name thy agoal tacsf = 
1529  1137 
(qed_thm := store_thm (name, prove_goal thy agoal tacsf); 
1291  1138 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
746  1139 

1140 
fun qed_goalw name thy rths agoal tacsf = 

1529  1141 
(qed_thm := store_thm (name, prove_goalw thy rths agoal tacsf); 
1291  1142 
use_string ["val " ^ name ^ " = !qed_thm;"]); 
559  1143 

783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1144 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1145 
(** Retrieve theorems **) 
559  1146 

783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1147 
(*Get all theorems belonging to a given theory*) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1148 
fun thmtab_of_thy thy = 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1149 
let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy); 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1150 
in thms end; 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1151 

1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1152 
fun thmtab_of_name name = 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1153 
let val ThyInfo {thms, ...} = the (get_thyinfo name); 
559  1154 
in thms end; 
476
836cad329311
added check for concistency of filename and theory name;
clasohm
parents:
426
diff
changeset

1155 

1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1156 
(*Get a stored theorem specified by theory and name. *) 
559  1157 
fun get_thm thy name = 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1158 
let fun get [] [] searched = 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1159 
raise THEORY ("get_thm: no theorem " ^ quote name, [thy]) 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1160 
 get [] ng searched = 
871  1161 
get (ng \\ searched) [] searched 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1162 
 get (t::ts) ng searched = 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1163 
(case Symtab.lookup (thmtab_of_name t, name) of 
1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset

1164 
Some thm => thm 
1403
cdfa3ffcead2
renamed parents_of to parents_of_name to avoid name clash with function
clasohm
parents:
1386
diff
changeset

1165 
 None => get ts (ng union (parents_of_name t)) (t::searched)); 
783
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1166 

08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1167 
val (tname, _) = thyinfo_of_sign (sign_of thy); 
08f1785a4384
changed get_thm to search all parent theories if the theorem is not found
clasohm
parents:
778
diff
changeset

1168 
in get [tname] [] [] end; 
559  1169 

1529  1170 
(*Get stored theorems of a theory (original derivations) *) 
1262
8f40ff1299d8
added removal of theorems if theory is to be reloaded; changed functions for
clasohm
parents:
1244
diff
changeset

1171 
val thms_of = Symtab.dest o thmtab_of_thy; 
559  1172 

778  1173 

1291  1174 

1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1175 

71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset

1176 
(*** Misc HTML functions ***) 
1291  1177 

1178 
(*Init HTML generator by setting paths and creating new files*) 

1179 
fun init_html () = 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1180 
let val cwd = OS.FileSys.getDir(); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1181 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1182 
val theory_list = TextIO.closeOut (TextIO.openOut ".theory_list.txt"); 
1291  1183 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1184 
val rel_gif_path = relative_path cwd (!gif_path); 
1368  1185 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1186 
(*Make new HTML files for Pure and CPure*) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1187 
fun init_pure_html () = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1188 
let val pure_out = TextIO.openOut ".Pure_sub.html"; 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1189 
val cpure_out = TextIO.openOut ".CPure_sub.html"; 
1408  1190 
val package = 
1191 
if cwd subdir_of (!base_path) then 

1192 
relative_path (!base_path) cwd 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

1193 
else last_path cwd; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1194 
in mk_charthead pure_out "Pure" "Children" false rel_gif_path "" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1195 
package; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1196 
mk_charthead cpure_out "CPure" "Children" false rel_gif_path "" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1197 
package; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1198 
TextIO.output (pure_out, "Pure\n"); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1199 
TextIO.output (cpure_out, "CPure\n"); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1200 
TextIO.closeOut pure_out; 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1201 
TextIO.closeOut cpure_out; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1202 
pure_subchart := Some cwd 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1203 
end; 
1291  1204 
in make_html := true; 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1205 
index_path := cwd; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1206 

1405
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1207 
(*Make sure that base_path contains the physical path and no 
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1208 
symbolic links*) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1209 
OS.FileSys.chDir (!base_path); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1210 
base_path := OS.FileSys.getDir(); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1211 
OS.FileSys.chDir cwd; 
1405
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1212 

1408  1213 
if cwd subdir_of (!base_path) then () 
1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1554
diff
changeset

1214 
else warning "The current working directory seems to be no \ 
1408  1215 
\subdirectory of\nIsabelle's main directory. \ 
1216 
\Please ensure that base_path's value is correct.\n"; 

1405
e9ca85a3713c
init_html now makes sure that base_path contains a physical path and no
clasohm
parents:
1403
diff
changeset

1217 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1218 
writeln ("Setting path for index.html to " ^ quote cwd ^ 
1291  1219 
"\nGIF path has been set to " ^ quote (!gif_path)); 
1220 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1221 
if is_none (!pure_subchart) then init_pure_html() 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1222 
else () 
1291  1223 
end; 
1224 

1313  1225 
(*Generate index.html*) 
1368  1226 
fun finish_html () = if not (!make_html) then () else 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1227 
let val tlist_path = tack_on (!index_path) ".theory_list.txt"; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1228 
val theory_list = TextIO.openIn tlist_path; 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1229 
val theories = space_explode "\n" (TextIO.inputAll theory_list); 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1230 
val dummy = (TextIO.closeIn theory_list; OS.FileSys.remove tlist_path); 
1291  1231 

1313  1232 
val gif_path = relative_path (!index_path) (!gif_path); 
1291  1233 

1234 
(*Make entry for main chart of all theories.*) 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1235 
fun main_entry t = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1236 
let 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1237 
val (name, path) = take_prefix (not_equal " ") (explode t); 
1291  1238 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1239 
val tname = implode name 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1240 
val tpath = tack_on (relative_path (!index_path) (implode (tl path))) 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1241 
("." ^ tname); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1242 
in "<A HREF = \"" ^ tpath ^ "_sub.html\"><IMG SRC = \"" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1243 
tack_on gif_path "red_arrow.gif\" BORDER=0 ALT = \\/></A>" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1244 
"<A HREF = \"" ^ tpath ^ "_sup.html\"><IMG SRC = \"" ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1245 
tack_on gif_path "blue_arrow.gif\ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1246 
\\" BORDER=0 ALT = /\\></A> <A HREF = \"" ^ tpath ^ 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1247 
".html\">" ^ tname ^ "</A><BR>\n" 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1248 
end; 
1291  1249 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset

1250 
val out = TextIO.openOut (tack_on (!index_path) "index.html"); 
1408  1251 

1252 
(*Find out in which subdirectory of Isabelle's main directory the 

1253 
index.html is placed; if index_path is no subdirectory of base_path 

1254 
then take the last directory of index_path*) 

1255 
val inside_isabelle = (!index_path) subdir_of (!base_path); 

1256 
val subdir = 

1257 
if inside_isabelle then relative_path (!base_path) (!index_path) 

1589
fd6a571cb2b0
added warning and automatic deactivation of HTML generation if we cannot write
clasohm
parents:
1580
diff
changeset

1258 
else last_path (!index_path); 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1259 
val subdirs = space_explode "/" subdir; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1260 

1408  1261 
(*Look for index.html in superdirectories; stop when Isabelle's 
1262 
main directory is reached*) 

1378  1263 
fun find_super_index [] n = ("", n) 
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1264 
 find_super_index (p::ps) n = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1265 
let val index_path = "/" ^ space_implode "/" (rev ps); 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1266 
in if file_exists (index_path ^ "/index.html") then (index_path, n) 
1408  1267 
else if length subdirs  n >= 0 then find_super_index ps (n+1) 
1268 
else ("", n) 

1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1269 
end; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1270 
val (super_index, level_diff) = 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1271 
find_super_index (rev (space_explode "/" (!index_path))) 1; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1272 
val level = length subdirs  level_diff; 
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset

1273 

b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
