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