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