author | wenzelm |
Sun, 11 Nov 2001 21:38:54 +0100 | |
changeset 12151 | fb0fb0209c87 |
parent 12123 | 739eba13e2cd |
child 12311 | ce5f9e61c037 |
permissions | -rw-r--r-- |
6203 | 1 |
(* Title: Pure/Thy/present.ML |
2 |
ID: $Id$ |
|
9416 | 3 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
8808 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6203 | 5 |
|
9416 | 6 |
Theory presentation: HTML, graph files, (PDF)LaTeX documents. |
6203 | 7 |
*) |
8 |
||
9 |
signature BASIC_PRESENT = |
|
10 |
sig |
|
11057 | 11 |
val no_document: ('a -> 'b) -> 'a -> 'b |
7727 | 12 |
val section: string -> unit |
6203 | 13 |
end; |
14 |
||
15 |
signature PRESENT = |
|
16 |
sig |
|
7727 | 17 |
include BASIC_PRESENT |
9452 | 18 |
val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
19 |
path: string, parents: string list} list -> Path.T -> unit |
|
11911
6533ceee4cd7
build option enables most basic browser info (for proper recording of session);
wenzelm
parents:
11856
diff
changeset
|
20 |
val init: bool -> bool -> string -> bool -> string list -> string -> Path.T option |
11580 | 21 |
-> Url.T option * bool -> bool -> unit |
7727 | 22 |
val finish: unit -> unit |
23 |
val init_theory: string -> unit |
|
8192 | 24 |
val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
25 |
val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit |
|
9136 | 26 |
val theory_output: string -> string -> unit |
7727 | 27 |
val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
12151 | 28 |
val multi_result: string * (string * thm list) list -> unit |
7727 | 29 |
val results: string -> string -> thm list -> unit |
30 |
val theorem: string -> thm -> unit |
|
31 |
val theorems: string -> thm list -> unit |
|
8088 | 32 |
val chapter: string -> unit |
7727 | 33 |
val subsection: string -> unit |
34 |
val subsubsection: string -> unit |
|
35 |
val setup: (theory -> theory) list |
|
9416 | 36 |
val get_info: theory -> {name: string, session: string list, is_local: bool} |
6203 | 37 |
end; |
38 |
||
7685 | 39 |
structure Present: PRESENT = |
40 |
struct |
|
41 |
||
7727 | 42 |
|
43 |
(** paths **) |
|
44 |
||
45 |
val output_path = Path.variable "ISABELLE_BROWSER_INFO"; |
|
46 |
||
47 |
val tex_ext = Path.ext "tex"; |
|
48 |
val tex_path = tex_ext o Path.basic; |
|
49 |
val html_ext = Path.ext "html"; |
|
50 |
val html_path = html_ext o Path.basic; |
|
51 |
val index_path = Path.basic "index.html"; |
|
11856 | 52 |
val readme_html_path = Path.basic "README.html"; |
53 |
val readme_path = Path.basic "README"; |
|
7727 | 54 |
val doc_path = Path.basic "document"; |
8196 | 55 |
val doc_indexN = "session"; |
11856 | 56 |
val graph_path = Path.basic "session.graph"; |
57 |
val graph_pdf_path = Path.basic "session_graph.pdf"; |
|
58 |
val graph_eps_path = Path.basic "session_graph.eps"; |
|
7727 | 59 |
|
60 |
val session_path = Path.basic ".session"; |
|
61 |
val session_entries_path = Path.unpack ".session/entries"; |
|
62 |
val pre_index_path = Path.unpack ".session/pre-index"; |
|
63 |
||
9044 | 64 |
fun mk_rel_path [] ys = Path.make ys |
65 |
| mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent) |
|
9416 | 66 |
| mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else |
9044 | 67 |
Path.appends (replicate (length ps) Path.parent @ [Path.make qs]); |
7727 | 68 |
|
11856 | 69 |
fun show_path path = Path.pack (Path.append (File.pwd ()) path); |
70 |
||
7727 | 71 |
|
72 |
(** additional theory data **) |
|
73 |
||
74 |
structure BrowserInfoArgs = |
|
75 |
struct |
|
76 |
val name = "Pure/browser_info"; |
|
9416 | 77 |
type T = {name: string, session: string list, is_local: bool}; |
7727 | 78 |
|
9416 | 79 |
val empty = {name = "Pure", session = [], is_local = false}; |
7727 | 80 |
val copy = I; |
12123 | 81 |
val finish = I; |
9452 | 82 |
fun prep_ext _ = {name = "", session = [], is_local = false}; |
7727 | 83 |
fun merge _ = empty; |
84 |
fun print _ _ = (); |
|
85 |
end; |
|
86 |
||
87 |
structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs); |
|
88 |
||
89 |
fun get_info thy = |
|
90 |
if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty |
|
91 |
else BrowserInfoData.get thy; |
|
92 |
||
93 |
||
94 |
||
95 |
(** graphs **) |
|
96 |
||
97 |
type graph_node = |
|
98 |
{name: string, ID: string, dir: string, unfold: bool, |
|
99 |
path: string, parents: string list}; |
|
100 |
||
9416 | 101 |
fun write_graph gr path = |
102 |
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
|
103 |
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
|
104 |
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); |
|
7727 | 105 |
|
9416 | 106 |
fun ID_of sess s = space_implode "/" (sess @ [s]); |
7727 | 107 |
|
9416 | 108 |
(*retrieve graph data from initial theory loader database*) |
109 |
fun init_graph remote_path curr_sess = map (fn name => |
|
7727 | 110 |
let |
9416 | 111 |
val {name = sess_name, session, is_local} = get_info (ThyInfo.theory name); |
112 |
val path' = Path.append (Path.make session) (html_path name); |
|
7727 | 113 |
in |
9416 | 114 |
{name = name, ID = ID_of session name, dir = sess_name, |
115 |
path = |
|
116 |
if null session then "" else |
|
117 |
if is_some remote_path andalso not is_local then |
|
118 |
Url.pack (Url.append (the remote_path) (Url.file |
|
119 |
(Path.append (Path.make session) (html_path name)))) |
|
120 |
else Path.pack (Path.append (mk_rel_path curr_sess session) (html_path name)), |
|
121 |
unfold = false, |
|
122 |
parents = |
|
123 |
map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) (ThyInfo.get_preds name)} |
|
7727 | 124 |
end) (ThyInfo.names ()); |
125 |
||
9416 | 126 |
fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) = |
7727 | 127 |
filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
128 |
||
129 |
||
130 |
||
131 |
(** global browser info state **) |
|
132 |
||
133 |
(* type theory_info *) |
|
134 |
||
135 |
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T}; |
|
136 |
||
137 |
fun make_theory_info (tex_source, html_source, html) = |
|
138 |
{tex_source = tex_source, html_source = html_source, html = html}: theory_info; |
|
139 |
||
140 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty); |
|
141 |
||
142 |
fun map_theory_info f {tex_source, html_source, html} = |
|
143 |
make_theory_info (f (tex_source, html_source, html)); |
|
144 |
||
145 |
||
146 |
(* type browser_info *) |
|
147 |
||
11856 | 148 |
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list, |
149 |
tex_index: Buffer.T, html_index: Buffer.T, graph: graph_node list}; |
|
7727 | 150 |
|
11856 | 151 |
fun make_browser_info (theories, files, tex_index, html_index, graph) = |
152 |
{theories = theories, files = files, tex_index = tex_index, html_index = html_index, |
|
9416 | 153 |
graph = graph}: browser_info; |
7727 | 154 |
|
11856 | 155 |
val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []); |
7727 | 156 |
|
9416 | 157 |
fun init_browser_info remote_path curr_sess = make_browser_info |
11856 | 158 |
(Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess); |
7727 | 159 |
|
11856 | 160 |
fun map_browser_info f {theories, files, tex_index, html_index, graph} = |
161 |
make_browser_info (f (theories, files, tex_index, html_index, graph)); |
|
7727 | 162 |
|
163 |
||
164 |
(* state *) |
|
165 |
||
166 |
val browser_info = ref empty_browser_info; |
|
11057 | 167 |
fun change_browser_info f = browser_info := map_browser_info f (! browser_info); |
7727 | 168 |
|
11057 | 169 |
val suppress_tex_source = ref false; |
170 |
fun no_document f x = Library.setmp suppress_tex_source true f x; |
|
7727 | 171 |
|
172 |
fun init_theory_info name info = |
|
11856 | 173 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
174 |
(Symtab.update ((name, info), theories), files, tex_index, html_index, graph)); |
|
7727 | 175 |
|
176 |
fun change_theory_info name f = |
|
11856 | 177 |
change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) => |
7727 | 178 |
(case Symtab.lookup (theories, name) of |
179 |
None => (warning ("Browser info: cannot access theory document " ^ quote name); info) |
|
11856 | 180 |
| Some info => (Symtab.update ((name, map_theory_info f info), theories), files, |
9416 | 181 |
tex_index, html_index, graph))); |
7727 | 182 |
|
183 |
||
11856 | 184 |
fun add_file file = |
185 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
|
186 |
(theories, file :: files, tex_index, html_index, graph)); |
|
187 |
||
7727 | 188 |
fun add_tex_index txt = |
11856 | 189 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
190 |
(theories, files, Buffer.add txt tex_index, html_index, graph)); |
|
7727 | 191 |
|
192 |
fun add_html_index txt = |
|
11856 | 193 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
194 |
(theories, files, tex_index, Buffer.add txt html_index, graph)); |
|
7727 | 195 |
|
196 |
fun add_graph_entry e = |
|
11856 | 197 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
198 |
(theories, files, tex_index, html_index, ins_graph_entry e graph)); |
|
7727 | 199 |
|
11057 | 200 |
fun add_tex_source name txt = |
201 |
if ! suppress_tex_source then () |
|
202 |
else change_theory_info name (fn (tex_source, html_source, html) => |
|
203 |
(Buffer.add txt tex_source, html_source, html)); |
|
7727 | 204 |
|
205 |
fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) => |
|
206 |
(tex_source, Buffer.add txt html_source, html)); |
|
207 |
||
208 |
fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) => |
|
209 |
(tex_source, html_source, Buffer.add txt html)); |
|
210 |
||
211 |
||
212 |
||
213 |
(** global session state **) |
|
214 |
||
215 |
(* session_info *) |
|
216 |
||
217 |
type session_info = |
|
218 |
{name: string, parent: string, session: string, path: string list, html_prefix: Path.T, |
|
11856 | 219 |
info: bool, doc_format: string, doc_graph: bool, doc_prefix1: Path.T option, |
220 |
doc_prefix2: Path.T option, remote_path: Url.T option, verbose: bool, readme: Path.T option}; |
|
7727 | 221 |
|
9416 | 222 |
fun make_session_info |
11856 | 223 |
(name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_prefix1, |
224 |
doc_prefix2, remote_path, verbose, readme) = |
|
7802 | 225 |
{name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, |
11856 | 226 |
info = info, doc_format = doc_format, doc_graph = doc_graph, doc_prefix1 = doc_prefix1, |
227 |
doc_prefix2 = doc_prefix2, remote_path = remote_path, verbose = verbose, |
|
228 |
readme = readme}: session_info; |
|
7685 | 229 |
|
230 |
||
7727 | 231 |
(* state *) |
232 |
||
233 |
val session_info = ref (None: session_info option); |
|
234 |
||
235 |
fun with_session x f = (case ! session_info of None => x | Some info => f info); |
|
236 |
fun with_context f = f (PureThy.get_name (Context.the_context ())); |
|
237 |
||
238 |
||
239 |
||
240 |
(** HTML output **) |
|
241 |
||
242 |
(* maintain index *) |
|
243 |
||
244 |
val session_entries = |
|
245 |
HTML.session_entries o |
|
246 |
map (fn name => (Url.file (Path.append (Path.basic name) index_path), name)); |
|
247 |
||
248 |
fun get_entries dir = |
|
249 |
split_lines (File.read (Path.append dir session_entries_path)); |
|
250 |
||
251 |
fun put_entries entries dir = |
|
252 |
File.write (Path.append dir session_entries_path) (cat_lines entries); |
|
253 |
||
254 |
||
255 |
fun create_index dir = |
|
256 |
File.read (Path.append dir pre_index_path) ^ |
|
257 |
session_entries (get_entries dir) ^ HTML.end_index |
|
258 |
|> File.write (Path.append dir index_path); |
|
259 |
||
260 |
fun update_index dir name = |
|
261 |
(case try get_entries dir of |
|
262 |
None => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir)) |
|
263 |
| Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); |
|
264 |
||
265 |
||
266 |
(* init session *) |
|
267 |
||
268 |
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
|
269 |
||
9044 | 270 |
fun copy_files path1 path2 = |
271 |
(File.mkdir path2; |
|
9795 | 272 |
File.system_command (*FIXME: quote paths!?*) |
273 |
("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2)); |
|
9044 | 274 |
|
9416 | 275 |
|
11911
6533ceee4cd7
build option enables most basic browser info (for proper recording of session);
wenzelm
parents:
11856
diff
changeset
|
276 |
fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose = |
6533ceee4cd7
build option enables most basic browser info (for proper recording of session);
wenzelm
parents:
11856
diff
changeset
|
277 |
if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then |
11856 | 278 |
(browser_info := empty_browser_info; session_info := None) |
279 |
else |
|
280 |
let |
|
281 |
val parent_name = name_of_session (Library.take (length path - 1, path)); |
|
282 |
val session_name = name_of_session path; |
|
283 |
val sess_prefix = Path.make path; |
|
284 |
val html_prefix = Path.append (Path.expand output_path) sess_prefix; |
|
7727 | 285 |
|
11856 | 286 |
val (doc_prefix1, document_path) = |
287 |
if doc = "" then (None, None) |
|
288 |
else if not (File.exists doc_path) then (conditional verbose (fn () => |
|
289 |
std_error "Warning: missing document directory\n"); (None, None)) |
|
290 |
else (Some (Path.append html_prefix doc_path), Some (Path.ext doc doc_path)); |
|
7727 | 291 |
|
11856 | 292 |
val parent_index_path = Path.append Path.parent index_path; |
293 |
val index_up_lnk = if first_time then |
|
294 |
Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path)) |
|
295 |
else Url.file parent_index_path; |
|
296 |
val readme = |
|
297 |
if File.exists readme_html_path then Some readme_html_path |
|
298 |
else if File.exists readme_path then Some readme_path |
|
299 |
else None; |
|
7727 | 300 |
|
11856 | 301 |
val index_text = HTML.begin_index (index_up_lnk, parent_name) |
302 |
(Url.file index_path, session_name) (apsome Url.file readme) |
|
303 |
(apsome Url.file document_path) (Url.unpack "medium.html"); |
|
304 |
in |
|
305 |
session_info := Some (make_session_info (name, parent_name, session_name, path, html_prefix, |
|
306 |
info, doc, doc_graph, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); |
|
307 |
browser_info := init_browser_info remote_path path; |
|
308 |
add_html_index index_text |
|
309 |
end; |
|
7727 | 310 |
|
311 |
||
11856 | 312 |
(* finish session -- output all generated text *) |
313 |
||
314 |
fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src; |
|
7685 | 315 |
|
11856 | 316 |
fun isatool_document doc_format path = |
317 |
let val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^ File.quote_sysify_path path in |
|
318 |
writeln s; |
|
319 |
if system s <> 0 orelse not (File.exists (Path.ext doc_format path)) then |
|
8646
1a2c5ccebfdb
isatool document: check output file (workaround PolyML problem with RC);
wenzelm
parents:
8499
diff
changeset
|
320 |
error "Failed to build document" |
1a2c5ccebfdb
isatool document: check output file (workaround PolyML problem with RC);
wenzelm
parents:
8499
diff
changeset
|
321 |
else () |
1a2c5ccebfdb
isatool document: check output file (workaround PolyML problem with RC);
wenzelm
parents:
8499
diff
changeset
|
322 |
end; |
7802 | 323 |
|
11856 | 324 |
fun isatool_browser graph = |
325 |
let |
|
326 |
val pdfpath = File.tmp_path graph_pdf_path; |
|
327 |
val epspath = File.tmp_path graph_eps_path; |
|
328 |
val gpath = File.tmp_path graph_path; |
|
329 |
val s = "\"$ISATOOL\" browser -o " ^ File.quote_sysify_path pdfpath ^ " " ^ |
|
330 |
File.quote_sysify_path gpath; |
|
331 |
in |
|
332 |
write_graph graph gpath; |
|
333 |
if system s <> 0 orelse not (File.exists epspath) orelse not (File.exists pdfpath) then |
|
334 |
error "Failed to prepare dependency graph" |
|
335 |
else |
|
336 |
let val pdf = File.read pdfpath and eps = File.read epspath |
|
337 |
in File.rm pdfpath; File.rm epspath; File.rm gpath; (pdf, eps) end |
|
338 |
end; |
|
8196 | 339 |
|
11856 | 340 |
fun finish () = with_session () (fn {name, info, html_prefix, doc_format, doc_graph, |
341 |
doc_prefix1, doc_prefix2, path, verbose, readme, ...} => |
|
7727 | 342 |
let |
11856 | 343 |
val {theories, files, tex_index, html_index, graph} = ! browser_info; |
344 |
val thys = Symtab.dest theories; |
|
9416 | 345 |
val parent_html_prefix = Path.append html_prefix Path.parent; |
7727 | 346 |
|
11856 | 347 |
fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path; |
348 |
fun finish_html (a, {html, ...}: theory_info) = |
|
349 |
Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); |
|
350 |
||
351 |
val opt_graphs = |
|
352 |
if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then |
|
353 |
Some (isatool_browser graph) |
|
354 |
else None; |
|
355 |
||
356 |
fun doc_common path = |
|
357 |
((case opt_graphs of None => () | Some (pdf, eps) => |
|
358 |
(File.write (Path.append path graph_pdf_path) pdf; |
|
359 |
File.write (Path.append path graph_eps_path) eps)); |
|
360 |
write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path; |
|
361 |
seq (finish_tex path) thys); |
|
7727 | 362 |
in |
11856 | 363 |
conditional info (fn () => |
364 |
(File.mkdir (Path.append html_prefix session_path); |
|
365 |
Buffer.write (Path.append html_prefix pre_index_path) html_index; |
|
366 |
File.write (Path.append html_prefix session_entries_path) ""; |
|
367 |
create_index html_prefix; |
|
368 |
if length path > 1 then update_index parent_html_prefix name else (); |
|
369 |
(case readme of None => () | Some path => File.copy path (Path.append html_prefix path)); |
|
370 |
write_graph graph (Path.append html_prefix graph_path); |
|
371 |
copy_files (Path.unpack "~~/lib/browser/awtUtilities/*.class") |
|
372 |
(Path.append html_prefix (Path.basic "awtUtilities")); |
|
373 |
copy_files (Path.unpack "~~/lib/browser/GraphBrowser/*.class") |
|
374 |
(Path.append html_prefix (Path.basic "GraphBrowser")); |
|
375 |
seq (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) |
|
376 |
(HTML.applet_pages name (Url.file index_path, name)); |
|
377 |
seq finish_html thys; |
|
378 |
seq (uncurry File.write) files; |
|
379 |
conditional verbose (fn () => |
|
380 |
std_error ("Browser info at " ^ show_path html_prefix ^ "\n")))); |
|
381 |
||
382 |
(case doc_prefix1 of None => () | Some path => |
|
383 |
(File.mkdir html_prefix; |
|
384 |
File.copy_all doc_path html_prefix; |
|
385 |
doc_common path; |
|
386 |
isatool_document doc_format path; |
|
387 |
conditional verbose (fn () => |
|
388 |
std_error ("Document at " ^ show_path (Path.ext doc_format path) ^ "\n")))); |
|
389 |
||
390 |
(case doc_prefix2 of None => () | Some path => |
|
391 |
(File.mkdir path; |
|
392 |
copy_files (Path.unpack "~~/lib/texinputs/*.sty") path; |
|
393 |
doc_common path; |
|
394 |
conditional verbose (fn () => std_error ("Document sources at " ^ show_path path ^ "\n")))); |
|
395 |
||
7727 | 396 |
browser_info := empty_browser_info; |
397 |
session_info := None |
|
398 |
end); |
|
399 |
||
400 |
||
401 |
(* theory elements *) |
|
402 |
||
403 |
fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info); |
|
404 |
||
405 |
fun verbatim_source name mk_text = |
|
406 |
with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ()))); |
|
407 |
||
8192 | 408 |
fun old_symbol_source name mk_text = |
8499 | 409 |
with_session () (fn _ => add_tex_source name (Latex.old_symbol_source name (mk_text ()))); |
8192 | 410 |
|
9136 | 411 |
fun theory_output name s = |
9917 | 412 |
with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
7727 | 413 |
|
414 |
||
415 |
fun parent_link remote_path curr_session name = |
|
9416 | 416 |
let val {name = _, session, is_local} = get_info (ThyInfo.theory name) |
7727 | 417 |
in (if null session then None else |
418 |
Some (if is_some remote_path andalso not is_local then |
|
9044 | 419 |
Url.append (the remote_path) (Url.file |
420 |
(Path.append (Path.make session) (html_path name))) |
|
421 |
else Url.file (Path.append (mk_rel_path curr_session session) |
|
422 |
(html_path name))), name) |
|
7727 | 423 |
end; |
424 |
||
425 |
fun begin_theory name raw_parents orig_files thy = |
|
9416 | 426 |
with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
7727 | 427 |
let |
428 |
val parents = map (parent_link remote_path path) raw_parents; |
|
429 |
val ml_path = ThyLoad.ml_path name; |
|
430 |
val files = map (apsnd Some) orig_files @ |
|
431 |
(if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []); |
|
432 |
||
433 |
fun prep_file (raw_path, loadit) = |
|
434 |
(case ThyLoad.check_file raw_path of |
|
435 |
Some (path, _) => |
|
436 |
let |
|
437 |
val base = Path.base path; |
|
438 |
val base_html = html_ext base; |
|
439 |
in |
|
11856 | 440 |
add_file (Path.append html_prefix base_html, |
441 |
HTML.ml_file (Url.file base) (File.read path)); |
|
7727 | 442 |
(Some (Url.file base_html), Url.file raw_path, loadit) |
443 |
end |
|
444 |
| None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path)); |
|
445 |
(None, Url.file raw_path, loadit))); |
|
446 |
||
447 |
val files_html = map prep_file files; |
|
448 |
||
449 |
fun prep_html_source (tex_source, html_source, html) = |
|
450 |
let |
|
451 |
val txt = HTML.begin_theory (Url.file index_path, session) |
|
452 |
name parents files_html (Buffer.content html_source) |
|
453 |
in (tex_source, Buffer.empty, Buffer.add txt html) end; |
|
454 |
||
9416 | 455 |
val entry = |
456 |
{name = name, ID = ID_of path name, dir = sess_name, unfold = true, |
|
457 |
path = Path.pack (html_path name), |
|
458 |
parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents}; |
|
7727 | 459 |
|
460 |
in |
|
461 |
change_theory_info name prep_html_source; |
|
9416 | 462 |
add_graph_entry entry; |
7727 | 463 |
add_html_index (HTML.theory_entry (Url.file (html_path name), name)); |
464 |
add_tex_index (Latex.theory_entry name); |
|
9416 | 465 |
BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy |
7727 | 466 |
end); |
467 |
||
468 |
||
12151 | 469 |
fun multi_result res = with_session () (fn _ => with_context add_html (HTML.multi_result res)); |
7727 | 470 |
fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms)); |
471 |
fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm)); |
|
472 |
fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms)); |
|
8088 | 473 |
fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s)); |
7727 | 474 |
fun section s = with_session () (fn _ => with_context add_html (HTML.section s)); |
475 |
fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s)); |
|
476 |
fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s)); |
|
477 |
||
478 |
||
479 |
||
480 |
(** theory setup **) |
|
481 |
||
482 |
val setup = [BrowserInfoData.init]; |
|
7685 | 483 |
|
484 |
||
485 |
end; |
|
486 |
||
6203 | 487 |
|
488 |
structure BasicPresent: BASIC_PRESENT = Present; |
|
489 |
open BasicPresent; |