author | wenzelm |
Fri, 18 Jul 1997 13:35:36 +0200 | |
changeset 3527 | b894f4c13df5 |
parent 3039 | bbf4e3738ef0 |
child 3576 | 9cd0a0919ba0 |
permissions | -rw-r--r-- |
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 .theory-list.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 sub-chart, sub if it is for a sup-chart; |
|
391 |
empty for Pure and CPure sub-charts) |
|
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 super-theories*) |
|
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 ^ "*)") (d-1) |
|
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 super-theories **) |
|
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 out-of-date: " |
|
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 sub-charts 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' sub-theory 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' sub-charts*) |
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
changeset
|
1274 |
(*Add link to current directory to 'super' index.html*) |
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1275 |
fun link_directory () = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1276 |
let val old_index = TextIO.openIn (super_index ^ "/index.html"); |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1277 |
val content = rev (explode (TextIO.inputAll old_index)); |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1278 |
val dummy = TextIO.closeIn old_index; |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1279 |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1280 |
val out = TextIO.openAppend (super_index ^ "/index.html"); |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1281 |
val rel_path = space_implode "/" (drop (level, subdirs)); |
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1282 |
in |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1283 |
TextIO.output (out, |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1284 |
(if nth_elem (3, content) <> "!" then "" |
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1285 |
else "\n<HR><H3>Subdirectories:</H3>\n") ^ |
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1286 |
"<H3><A HREF = \"" ^ rel_path ^ "/index.html\">" ^ rel_path ^ |
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1287 |
"</A></H3>\n"); |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1288 |
TextIO.closeOut out |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1289 |
end; |
1408 | 1290 |
|
1291 |
(*If index_path is no subdirectory of base_path then the title should |
|
1292 |
not contain the string "Isabelle/"*) |
|
1293 |
val title = (if inside_isabelle then "Isabelle/" else "") ^ subdir; |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1294 |
in TextIO.output (out, |
1408 | 1295 |
"<HTML><HEAD><TITLE>" ^ title ^ "</TITLE></HEAD>\n\ |
1296 |
\<BODY><H2>" ^ title ^ "</H2>\n\ |
|
1291 | 1297 |
\The name of every theory is linked to its theory file<BR>\n\ |
1298 |
\<IMG SRC = \"" ^ tack_on gif_path "red_arrow.gif\ |
|
1299 |
\\" ALT = \\/></A> stands for subtheories (child theories)<BR>\n\ |
|
1300 |
\<IMG SRC = \"" ^ tack_on gif_path "blue_arrow.gif\ |
|
1378 | 1301 |
\\" ALT = /\\></A> stands for supertheories (parent theories)" ^ |
1302 |
(if super_index = "" then "" else |
|
1303 |
("<P>\n<A HREF = \"" ^ relative_path (!index_path) super_index ^ |
|
1304 |
"/index.html\">Back</A> to the index of " ^ |
|
1408 | 1305 |
(if not inside_isabelle then |
1306 |
hd (tl (rev (space_explode "/" (!index_path)))) |
|
1307 |
else if level = 0 then "Isabelle logics" |
|
1378 | 1308 |
else space_implode "/" (take (level, subdirs))))) ^ |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1309 |
"\n" ^ |
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1310 |
(if file_exists (tack_on (!index_path) "README.html") then |
1332 | 1311 |
"<BR>View the <A HREF = \"README.html\">ReadMe</A> file.\n" |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1312 |
else if file_exists (tack_on (!index_path) "README") then |
1332 | 1313 |
"<BR>View the <A HREF = \"README\">ReadMe</A> file.\n" |
1314 |
else "") ^ |
|
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1315 |
"<HR>" ^ implode (map main_entry theories) ^ "<!-->"); |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1316 |
TextIO.closeOut out; |
1408 | 1317 |
if super_index = "" orelse (inside_isabelle andalso level = 0) then () |
1318 |
else link_directory () |
|
1291 | 1319 |
end; |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1320 |
|
1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset
|
1321 |
(*Append section heading to HTML file*) |
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset
|
1322 |
fun section s = |
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset
|
1323 |
case !cur_htmlfile of |
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset
|
1324 |
Some out => (mk_theorems_title out; |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1325 |
TextIO.output (out, "<H3>" ^ s ^ "</H3>\n")) |
1538
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset
|
1326 |
| None => (); |
31ad553d018b
added function "section" for HTML section headings
clasohm
parents:
1530
diff
changeset
|
1327 |
|
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1328 |
|
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1329 |
(*** Print theory ***) |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1330 |
|
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1331 |
fun print_thms thy = |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1332 |
let |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1333 |
val thms = thms_of thy; |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1334 |
fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1, |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1335 |
Pretty.quote (pretty_thm th)]; |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1336 |
in |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1337 |
Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms)) |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1338 |
end; |
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1339 |
|
1598
6f4d995590fd
For the new version of name_thm. Now the same theorem
paulson
parents:
1589
diff
changeset
|
1340 |
fun print_theory thy = (Display.print_theory thy; print_thms thy); |
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1341 |
|
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1342 |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1343 |
(*** Misc functions ***) |
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1344 |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1345 |
(*Add data handling methods to theory*) |
1658
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1346 |
fun add_thydata tname (new_methods as (id, ThyMethods {get, ...})) = |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1347 |
let val ThyInfo {path, children, parents, thy_time, ml_time, theory, |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1348 |
thms, methods, data} = |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1349 |
case get_thyinfo tname of |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1350 |
Some ti => ti |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1351 |
| None => error ("Theory " ^ tname ^ " not stored by loader"); |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1352 |
in loaded_thys := Symtab.update ((tname, ThyInfo {path = path, |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1353 |
children = children, parents = parents, thy_time = thy_time, |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1354 |
ml_time = ml_time, theory = theory, thms = thms, |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1355 |
methods = Symtab.update (new_methods, methods), data = data}), |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1356 |
!loaded_thys) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1357 |
end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1358 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1359 |
(*Add file to thy_reader_files list*) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1360 |
fun set_thy_reader_file file = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1361 |
let val file' = absolute_path (OS.FileSys.getDir ()) file; |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1362 |
in thy_reader_files := file' :: (!thy_reader_files) end; |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1363 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1364 |
(*Add file and also 'use' it*) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1365 |
fun add_thy_reader_file file = (set_thy_reader_file file; use file); |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1366 |
|
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1367 |
(*Read all files contained in thy_reader_files list*) |
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1368 |
fun read_thy_reader_files () = seq use (!thy_reader_files); |
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1369 |
|
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1370 |
|
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1371 |
(*Retrieve data associated with theory*) |
1658
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1372 |
fun get_thydata tname id = |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1373 |
let val d2 = case get_thyinfo tname of |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1374 |
Some (ThyInfo {data, ...}) => snd data |
0eb69773354f
add_thydata and get_thydata now take a string as their first argument
clasohm
parents:
1656
diff
changeset
|
1375 |
| None => error ("Theory " ^ tname ^ " not stored by loader"); |
1457
ad856378ad62
added facility to associate arbitrary data with theories
clasohm
parents:
1408
diff
changeset
|
1376 |
in Symtab.lookup (d2, id) end; |
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1377 |
|
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1378 |
|
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1379 |
(*Temporarily enter a directory and load its ROOT.ML file; |
1359
71124bd19b40
added functions for storing and retrieving information about datatypes
clasohm
parents:
1348
diff
changeset
|
1380 |
also do some work for HTML generation*) |
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1381 |
local |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1382 |
|
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1383 |
fun gen_use_dir use_cmd dirname = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1384 |
let val old_dir = OS.FileSys.getDir (); |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1385 |
in OS.FileSys.chDir dirname; |
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1386 |
if !make_html then init_html() else (); |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1387 |
use_cmd "ROOT.ML"; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1388 |
finish_html(); |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2188
diff
changeset
|
1389 |
OS.FileSys.chDir old_dir |
1670
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1390 |
end; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1391 |
|
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1392 |
in |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1393 |
|
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1394 |
val use_dir = gen_use_dir use; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1395 |
val exit_use_dir = gen_use_dir exit_use; |
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1396 |
|
d706a6dce930
use_dir and exit_use_dir now change the CWD only temporarily
clasohm
parents:
1664
diff
changeset
|
1397 |
end |
1348
b9305143fa91
index.html files are now made separatly for each subdirectory
clasohm
parents:
1332
diff
changeset
|
1398 |
|
391 | 1399 |
end; |