author | wenzelm |
Tue, 31 Jul 2007 21:19:24 +0200 | |
changeset 24102 | 969d334040a8 |
parent 23944 | 2ea068548a83 |
child 24150 | ed724867099a |
permissions | -rw-r--r-- |
6203 | 1 |
(* Title: Pure/Thy/present.ML |
2 |
ID: $Id$ |
|
9416 | 3 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
6203 | 4 |
|
9416 | 5 |
Theory presentation: HTML, graph files, (PDF)LaTeX documents. |
6203 | 6 |
*) |
7 |
||
8 |
signature BASIC_PRESENT = |
|
9 |
sig |
|
11057 | 10 |
val no_document: ('a -> 'b) -> 'a -> 'b |
7727 | 11 |
val section: string -> unit |
6203 | 12 |
end; |
13 |
||
14 |
signature PRESENT = |
|
15 |
sig |
|
7727 | 16 |
include BASIC_PRESENT |
14922 | 17 |
val get_info: theory -> {name: string, session: string list, is_local: bool} |
9452 | 18 |
val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
19 |
path: string, parents: string list} list -> Path.T -> unit |
|
20577 | 20 |
val display_graph: {name: string, ID: string, dir: string, unfold: bool, |
21 |
path: string, parents: string list} list -> unit |
|
17082 | 22 |
val init: bool -> bool -> string -> bool -> string list -> string list -> |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
23 |
string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit |
7727 | 24 |
val finish: unit -> unit |
25 |
val init_theory: string -> unit |
|
8192 | 26 |
val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
9136 | 27 |
val theory_output: string -> string -> unit |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
28 |
val begin_theory: Path.T -> (Path.T * bool) list -> theory -> theory |
13532 | 29 |
val add_hook: (string -> (string * thm list) list -> unit) -> unit |
30 |
val results: string -> (string * thm list) list -> unit |
|
7727 | 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 |
|
14922 | 36 |
val drafts: string -> Path.T list -> Path.T |
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"; |
|
17082 | 54 |
val documentN = "document"; |
55 |
val document_path = Path.basic documentN; |
|
8196 | 56 |
val doc_indexN = "session"; |
11856 | 57 |
val graph_path = Path.basic "session.graph"; |
58 |
val graph_pdf_path = Path.basic "session_graph.pdf"; |
|
59 |
val graph_eps_path = Path.basic "session_graph.eps"; |
|
7727 | 60 |
|
61 |
val session_path = Path.basic ".session"; |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
62 |
val session_entries_path = Path.explode ".session/entries"; |
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
63 |
val pre_index_path = Path.explode ".session/pre-index"; |
7727 | 64 |
|
9044 | 65 |
fun mk_rel_path [] ys = Path.make ys |
66 |
| mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent) |
|
9416 | 67 |
| mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else |
9044 | 68 |
Path.appends (replicate (length ps) Path.parent @ [Path.make qs]); |
7727 | 69 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
70 |
fun show_path path = Path.implode (Path.append (File.pwd ()) path); |
11856 | 71 |
|
7727 | 72 |
|
14922 | 73 |
|
7727 | 74 |
(** additional theory data **) |
75 |
||
16426 | 76 |
structure BrowserInfoData = TheoryDataFun |
22846 | 77 |
( |
9416 | 78 |
type T = {name: string, session: string list, is_local: bool}; |
16503 | 79 |
val empty = {name = "", session = [], is_local = false}: T; |
7727 | 80 |
val copy = I; |
16503 | 81 |
fun extend _ = empty; |
16426 | 82 |
fun merge _ _ = empty; |
22846 | 83 |
); |
7727 | 84 |
|
85 |
fun get_info thy = |
|
20664 | 86 |
if member (op =) [Context.ProtoPureN, Context.PureN, Context.CPureN] (Context.theory_name thy) |
16503 | 87 |
then {name = Context.PureN, session = [], is_local = false} |
7727 | 88 |
else BrowserInfoData.get thy; |
89 |
||
90 |
||
91 |
||
92 |
(** graphs **) |
|
93 |
||
94 |
type graph_node = |
|
95 |
{name: string, ID: string, dir: string, unfold: bool, |
|
96 |
path: string, parents: string list}; |
|
97 |
||
9416 | 98 |
fun write_graph gr path = |
99 |
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
|
100 |
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
|
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
14540
diff
changeset
|
101 |
path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr)); |
7727 | 102 |
|
20577 | 103 |
fun display_graph gr = |
104 |
let |
|
105 |
val _ = writeln "Generating graph ..."; |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
106 |
val path = File.tmp_path (Path.explode "tmp.graph"); |
20577 | 107 |
val _ = write_graph gr path; |
108 |
val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &"); |
|
109 |
in () end; |
|
110 |
||
111 |
||
9416 | 112 |
fun ID_of sess s = space_implode "/" (sess @ [s]); |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
113 |
fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy); |
7727 | 114 |
|
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
115 |
|
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
116 |
(*retrieve graph data from initial collection of theories*) |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
117 |
fun init_graph remote_path curr_sess = map (fn thy => |
7727 | 118 |
let |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
119 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
120 |
val {name = sess_name, session, is_local} = get_info thy; |
9416 | 121 |
val path' = Path.append (Path.make session) (html_path name); |
7727 | 122 |
in |
9416 | 123 |
{name = name, ID = ID_of session name, dir = sess_name, |
124 |
path = |
|
125 |
if null session then "" else |
|
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
126 |
if is_some remote_path andalso not is_local then |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
127 |
Url.implode (Url.append (the remote_path) (Url.File |
9416 | 128 |
(Path.append (Path.make session) (html_path name)))) |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
129 |
else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), |
9416 | 130 |
unfold = false, |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
131 |
parents = map ID_of_thy (Theory.parents_of thy)} |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
132 |
end); |
7727 | 133 |
|
9416 | 134 |
fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) = |
7727 | 135 |
filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
136 |
||
137 |
||
138 |
||
139 |
(** global browser info state **) |
|
140 |
||
141 |
(* type theory_info *) |
|
142 |
||
143 |
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T}; |
|
144 |
||
145 |
fun make_theory_info (tex_source, html_source, html) = |
|
146 |
{tex_source = tex_source, html_source = html_source, html = html}: theory_info; |
|
147 |
||
148 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty); |
|
149 |
||
150 |
fun map_theory_info f {tex_source, html_source, html} = |
|
151 |
make_theory_info (f (tex_source, html_source, html)); |
|
152 |
||
153 |
||
154 |
(* type browser_info *) |
|
155 |
||
11856 | 156 |
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list, |
157 |
tex_index: Buffer.T, html_index: Buffer.T, graph: graph_node list}; |
|
7727 | 158 |
|
11856 | 159 |
fun make_browser_info (theories, files, tex_index, html_index, graph) = |
160 |
{theories = theories, files = files, tex_index = tex_index, html_index = html_index, |
|
9416 | 161 |
graph = graph}: browser_info; |
7727 | 162 |
|
11856 | 163 |
val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []); |
7727 | 164 |
|
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
165 |
fun init_browser_info remote_path curr_sess thys = make_browser_info |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
166 |
(Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess thys); |
7727 | 167 |
|
11856 | 168 |
fun map_browser_info f {theories, files, tex_index, html_index, graph} = |
169 |
make_browser_info (f (theories, files, tex_index, html_index, graph)); |
|
7727 | 170 |
|
171 |
||
172 |
(* state *) |
|
173 |
||
174 |
val browser_info = ref empty_browser_info; |
|
23944 | 175 |
fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f)); |
7727 | 176 |
|
11057 | 177 |
val suppress_tex_source = ref false; |
24102 | 178 |
fun no_document f x = setmp_noncritical suppress_tex_source true f x; |
7727 | 179 |
|
180 |
fun init_theory_info name info = |
|
11856 | 181 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
17412 | 182 |
(Symtab.update (name, info) theories, files, tex_index, html_index, graph)); |
7727 | 183 |
|
184 |
fun change_theory_info name f = |
|
11856 | 185 |
change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) => |
17412 | 186 |
(case Symtab.lookup theories name of |
15531 | 187 |
NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info) |
17412 | 188 |
| SOME info => (Symtab.update (name, map_theory_info f info) theories, files, |
9416 | 189 |
tex_index, html_index, graph))); |
7727 | 190 |
|
191 |
||
11856 | 192 |
fun add_file file = |
193 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
|
194 |
(theories, file :: files, tex_index, html_index, graph)); |
|
195 |
||
7727 | 196 |
fun add_tex_index txt = |
11856 | 197 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
198 |
(theories, files, Buffer.add txt tex_index, html_index, graph)); |
|
7727 | 199 |
|
200 |
fun add_html_index txt = |
|
11856 | 201 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
202 |
(theories, files, tex_index, Buffer.add txt html_index, graph)); |
|
7727 | 203 |
|
204 |
fun add_graph_entry e = |
|
11856 | 205 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
206 |
(theories, files, tex_index, html_index, ins_graph_entry e graph)); |
|
7727 | 207 |
|
11057 | 208 |
fun add_tex_source name txt = |
209 |
if ! suppress_tex_source then () |
|
210 |
else change_theory_info name (fn (tex_source, html_source, html) => |
|
211 |
(Buffer.add txt tex_source, html_source, html)); |
|
7727 | 212 |
|
213 |
fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) => |
|
214 |
(tex_source, Buffer.add txt html_source, html)); |
|
215 |
||
216 |
fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) => |
|
217 |
(tex_source, html_source, Buffer.add txt html)); |
|
218 |
||
219 |
||
220 |
||
221 |
(** global session state **) |
|
222 |
||
223 |
(* session_info *) |
|
224 |
||
225 |
type session_info = |
|
226 |
{name: string, parent: string, session: string, path: string list, html_prefix: Path.T, |
|
17082 | 227 |
info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, |
17210 | 228 |
doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option, |
229 |
remote_path: Url.T option, verbose: bool, readme: Path.T option}; |
|
7727 | 230 |
|
9416 | 231 |
fun make_session_info |
17082 | 232 |
(name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents, |
233 |
doc_prefix1, doc_prefix2, remote_path, verbose, readme) = |
|
7802 | 234 |
{name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, |
17082 | 235 |
info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents, |
236 |
doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path, |
|
237 |
verbose = verbose, readme = readme}: session_info; |
|
7685 | 238 |
|
239 |
||
7727 | 240 |
(* state *) |
241 |
||
15531 | 242 |
val session_info = ref (NONE: session_info option); |
7727 | 243 |
|
15531 | 244 |
fun with_session x f = (case ! session_info of NONE => x | SOME info => f info); |
22123
15ddfafc04a9
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21962
diff
changeset
|
245 |
fun with_context f = f (Context.theory_name (ML_Context.the_context ())); |
7727 | 246 |
|
247 |
||
248 |
||
14922 | 249 |
(** document preparation **) |
7727 | 250 |
|
251 |
(* maintain index *) |
|
252 |
||
253 |
val session_entries = |
|
254 |
HTML.session_entries o |
|
14898 | 255 |
map (fn name => (Url.File (Path.append (Path.basic name) index_path), name)); |
7727 | 256 |
|
257 |
fun get_entries dir = |
|
258 |
split_lines (File.read (Path.append dir session_entries_path)); |
|
259 |
||
260 |
fun put_entries entries dir = |
|
261 |
File.write (Path.append dir session_entries_path) (cat_lines entries); |
|
262 |
||
263 |
||
264 |
fun create_index dir = |
|
265 |
File.read (Path.append dir pre_index_path) ^ |
|
266 |
session_entries (get_entries dir) ^ HTML.end_index |
|
267 |
|> File.write (Path.append dir index_path); |
|
268 |
||
269 |
fun update_index dir name = |
|
270 |
(case try get_entries dir of |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
271 |
NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir)) |
19305 | 272 |
| SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); |
7727 | 273 |
|
274 |
||
17082 | 275 |
(* document versions *) |
276 |
||
277 |
fun read_version str = |
|
278 |
(case space_explode "=" str of |
|
279 |
[name] => (name, "") |
|
280 |
| [name, tags] => (name, tags) |
|
281 |
| _ => error ("Malformed document version specification: " ^ quote str)); |
|
282 |
||
283 |
fun read_versions strs = |
|
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18708
diff
changeset
|
284 |
rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs))) |
17082 | 285 |
|> filter_out (equal "-" o #2); |
286 |
||
287 |
||
7727 | 288 |
(* init session *) |
289 |
||
12895 | 290 |
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
291 |
||
17082 | 292 |
fun init build info doc doc_graph doc_versions path name doc_prefix2 |
23944 | 293 |
(remote_path, first_time) verbose thys = CRITICAL (fn () => |
11911
6533ceee4cd7
build option enables most basic browser info (for proper recording of session);
wenzelm
parents:
11856
diff
changeset
|
294 |
if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then |
15531 | 295 |
(browser_info := empty_browser_info; session_info := NONE) |
11856 | 296 |
else |
297 |
let |
|
298 |
val parent_name = name_of_session (Library.take (length path - 1, path)); |
|
299 |
val session_name = name_of_session path; |
|
300 |
val sess_prefix = Path.make path; |
|
301 |
val html_prefix = Path.append (Path.expand output_path) sess_prefix; |
|
7727 | 302 |
|
17082 | 303 |
val (doc_prefix1, documents) = |
304 |
if doc = "" then (NONE, []) |
|
21962 | 305 |
else if not (File.exists document_path) then |
22580 | 306 |
(if verbose then Output.std_error "Warning: missing document directory\n" else (); |
307 |
(NONE, [])) |
|
17082 | 308 |
else (SOME (Path.append html_prefix document_path, html_prefix), |
309 |
read_versions doc_versions); |
|
7727 | 310 |
|
11856 | 311 |
val parent_index_path = Path.append Path.parent index_path; |
312 |
val index_up_lnk = if first_time then |
|
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
313 |
Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path)) |
14898 | 314 |
else Url.File parent_index_path; |
11856 | 315 |
val readme = |
15531 | 316 |
if File.exists readme_html_path then SOME readme_html_path |
317 |
else if File.exists readme_path then SOME readme_path |
|
318 |
else NONE; |
|
7727 | 319 |
|
17082 | 320 |
val docs = |
321 |
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
|
322 |
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; |
|
11856 | 323 |
val index_text = HTML.begin_index (index_up_lnk, parent_name) |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
324 |
(Url.File index_path, session_name) docs (Url.explode "medium.html"); |
11856 | 325 |
in |
15531 | 326 |
session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix, |
17082 | 327 |
info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme)); |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
328 |
browser_info := init_browser_info remote_path path thys; |
11856 | 329 |
add_html_index index_text |
23944 | 330 |
end); |
7727 | 331 |
|
332 |
||
17082 | 333 |
(* isatool wrappers *) |
334 |
||
335 |
fun isatool_document verbose format name tags path result_path = |
|
336 |
let |
|
337 |
val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \ |
|
338 |
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ |
|
339 |
" 2>&1" ^ (if verbose then "" else " >/dev/null"); |
|
340 |
val doc_path = Path.append result_path (Path.ext format (Path.basic name)); |
|
341 |
in |
|
21962 | 342 |
if verbose then writeln s else (); |
17082 | 343 |
system s; |
21962 | 344 |
File.exists doc_path orelse |
345 |
error ("No document: " ^ quote (show_path doc_path)); |
|
17082 | 346 |
doc_path |
347 |
end; |
|
348 |
||
349 |
fun isatool_browser graph = |
|
350 |
let |
|
351 |
val pdf_path = File.tmp_path graph_pdf_path; |
|
352 |
val eps_path = File.tmp_path graph_eps_path; |
|
353 |
val gr_path = File.tmp_path graph_path; |
|
354 |
val s = "browser -o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path; |
|
355 |
in |
|
356 |
write_graph graph gr_path; |
|
357 |
if File.isatool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path) |
|
358 |
then error "Failed to prepare dependency graph" |
|
359 |
else |
|
360 |
let val pdf = File.read pdf_path and eps = File.read eps_path |
|
361 |
in File.rm pdf_path; File.rm eps_path; File.rm gr_path; (pdf, eps) end |
|
362 |
end; |
|
363 |
||
364 |
||
11856 | 365 |
(* finish session -- output all generated text *) |
366 |
||
14922 | 367 |
fun write_tex src name path = |
368 |
Buffer.write (Path.append path (tex_path name)) src; |
|
369 |
||
370 |
fun write_tex_index tex_index path = |
|
371 |
write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path; |
|
372 |
||
7685 | 373 |
|
23944 | 374 |
fun finish () = CRITICAL (fn () => |
375 |
with_session () (fn {name, info, html_prefix, doc_format, doc_graph, |
|
376 |
documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} => |
|
7727 | 377 |
let |
11856 | 378 |
val {theories, files, tex_index, html_index, graph} = ! browser_info; |
379 |
val thys = Symtab.dest theories; |
|
9416 | 380 |
val parent_html_prefix = Path.append html_prefix Path.parent; |
7727 | 381 |
|
11856 | 382 |
fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path; |
383 |
fun finish_html (a, {html, ...}: theory_info) = |
|
384 |
Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); |
|
385 |
||
386 |
val opt_graphs = |
|
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
387 |
if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then |
15531 | 388 |
SOME (isatool_browser graph) |
389 |
else NONE; |
|
11856 | 390 |
|
17210 | 391 |
fun prepare_sources cp path = |
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
392 |
(File.mkdir path; |
17210 | 393 |
if cp then File.copy_dir document_path path else (); |
17177 | 394 |
File.isatool ("latex -o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex"))); |
15531 | 395 |
(case opt_graphs of NONE => () | SOME (pdf, eps) => |
11856 | 396 |
(File.write (Path.append path graph_pdf_path) pdf; |
397 |
File.write (Path.append path graph_eps_path) eps)); |
|
14922 | 398 |
write_tex_index tex_index path; |
15570 | 399 |
List.app (finish_tex path) thys); |
7727 | 400 |
in |
21962 | 401 |
if info then |
11856 | 402 |
(File.mkdir (Path.append html_prefix session_path); |
403 |
Buffer.write (Path.append html_prefix pre_index_path) html_index; |
|
404 |
File.write (Path.append html_prefix session_entries_path) ""; |
|
405 |
create_index html_prefix; |
|
406 |
if length path > 1 then update_index parent_html_prefix name else (); |
|
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
407 |
(case readme of NONE => () | SOME path => File.copy path html_prefix); |
11856 | 408 |
write_graph graph (Path.append html_prefix graph_path); |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
409 |
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; |
15570 | 410 |
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) |
14898 | 411 |
(HTML.applet_pages name (Url.File index_path, name)); |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
412 |
File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix; |
15570 | 413 |
List.app finish_html thys; |
414 |
List.app (uncurry File.write) files; |
|
22580 | 415 |
if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ()) |
21962 | 416 |
else (); |
11856 | 417 |
|
17210 | 418 |
(case doc_prefix2 of NONE => () | SOME (cp, path) => |
419 |
(prepare_sources cp path; |
|
22580 | 420 |
if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ())); |
12895 | 421 |
|
17082 | 422 |
(case doc_prefix1 of NONE => () | SOME (path, result_path) => |
423 |
documents |> List.app (fn (name, tags) => |
|
424 |
let |
|
17210 | 425 |
val _ = prepare_sources true path; |
17082 | 426 |
val doc_path = isatool_document true doc_format name tags path result_path; |
427 |
in |
|
22580 | 428 |
if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else () |
17082 | 429 |
end)); |
11856 | 430 |
|
7727 | 431 |
browser_info := empty_browser_info; |
15531 | 432 |
session_info := NONE |
23944 | 433 |
end)); |
7727 | 434 |
|
435 |
||
436 |
(* theory elements *) |
|
437 |
||
438 |
fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info); |
|
439 |
||
440 |
fun verbatim_source name mk_text = |
|
441 |
with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ()))); |
|
442 |
||
9136 | 443 |
fun theory_output name s = |
9917 | 444 |
with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
7727 | 445 |
|
446 |
||
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
447 |
fun parent_link remote_path curr_session thy = |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
448 |
let |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
449 |
val {name = _, session, is_local} = get_info thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
450 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
451 |
val link = |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
452 |
if null session then NONE |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
453 |
else SOME |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
454 |
(if is_some remote_path andalso not is_local then |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
455 |
Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name))) |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
456 |
else Url.File (Path.append (mk_rel_path curr_session session) (html_path name))); |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
457 |
in (link, name) end; |
7727 | 458 |
|
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
459 |
fun begin_theory dir orig_files thy = |
9416 | 460 |
with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
7727 | 461 |
let |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
462 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
463 |
val parents = Theory.parents_of thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
464 |
val parent_specs = map (parent_link remote_path path) parents; |
7727 | 465 |
val ml_path = ThyLoad.ml_path name; |
15531 | 466 |
val files = map (apsnd SOME) orig_files @ |
23884
1d39ec4fe73f
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23870
diff
changeset
|
467 |
(if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []); |
7727 | 468 |
|
469 |
fun prep_file (raw_path, loadit) = |
|
23884
1d39ec4fe73f
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23870
diff
changeset
|
470 |
(case ThyLoad.check_ml dir raw_path of |
15531 | 471 |
SOME (path, _) => |
7727 | 472 |
let |
473 |
val base = Path.base path; |
|
474 |
val base_html = html_ext base; |
|
475 |
in |
|
11856 | 476 |
add_file (Path.append html_prefix base_html, |
14898 | 477 |
HTML.ml_file (Url.File base) (File.read path)); |
15531 | 478 |
(SOME (Url.File base_html), Url.File raw_path, loadit) |
7727 | 479 |
end |
23884
1d39ec4fe73f
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23870
diff
changeset
|
480 |
| NONE => |
1d39ec4fe73f
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23870
diff
changeset
|
481 |
(warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path)); |
1d39ec4fe73f
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23870
diff
changeset
|
482 |
(NONE, Url.File raw_path, loadit))); |
7727 | 483 |
|
484 |
val files_html = map prep_file files; |
|
485 |
||
486 |
fun prep_html_source (tex_source, html_source, html) = |
|
487 |
let |
|
14898 | 488 |
val txt = HTML.begin_theory (Url.File index_path, session) |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
489 |
name parent_specs files_html (Buffer.content html_source) |
7727 | 490 |
in (tex_source, Buffer.empty, Buffer.add txt html) end; |
491 |
||
9416 | 492 |
val entry = |
493 |
{name = name, ID = ID_of path name, dir = sess_name, unfold = true, |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
494 |
path = Path.implode (html_path name), |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
495 |
parents = map ID_of_thy parents}; |
7727 | 496 |
|
497 |
in |
|
498 |
change_theory_info name prep_html_source; |
|
9416 | 499 |
add_graph_entry entry; |
14898 | 500 |
add_html_index (HTML.theory_entry (Url.File (html_path name), name)); |
7727 | 501 |
add_tex_index (Latex.theory_entry name); |
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
502 |
BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy |
7727 | 503 |
end); |
504 |
||
505 |
||
13532 | 506 |
val hooks = ref ([]: (string -> (string * thm list) list -> unit) list); |
23944 | 507 |
fun add_hook f = CRITICAL (fn () => change hooks (cons f)); |
13532 | 508 |
|
509 |
fun results k xs = |
|
15570 | 510 |
(List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks); |
22123
15ddfafc04a9
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21962
diff
changeset
|
511 |
with_session () (fn _ => with_context add_html |
15ddfafc04a9
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21962
diff
changeset
|
512 |
(HTML.results (ML_Context.the_local_context ()) k xs))); |
13532 | 513 |
|
22123
15ddfafc04a9
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21962
diff
changeset
|
514 |
fun theorem a th = results Thm.theoremK [(a, [th])]; |
15ddfafc04a9
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
21962
diff
changeset
|
515 |
fun theorems a ths = results Thm.theoremK [(a, ths)]; |
8088 | 516 |
fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s)); |
7727 | 517 |
fun section s = with_session () (fn _ => with_context add_html (HTML.section s)); |
518 |
fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s)); |
|
519 |
fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s)); |
|
520 |
||
521 |
||
522 |
||
14922 | 523 |
(** draft document output **) |
524 |
||
525 |
fun drafts doc_format src_paths = |
|
526 |
let |
|
14935 | 527 |
fun prep_draft (tex_index, path) = |
528 |
let |
|
529 |
val base = Path.base path; |
|
14972 | 530 |
val name = |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
531 |
(case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s); |
14935 | 532 |
in |
533 |
if File.exists path then |
|
534 |
(Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path)) |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
535 |
else error ("Bad file: " ^ quote (Path.implode path)) |
14935 | 536 |
end; |
537 |
val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths); |
|
538 |
||
17082 | 539 |
val doc_path = File.tmp_path document_path; |
540 |
val result_path = Path.append doc_path Path.parent; |
|
14922 | 541 |
val _ = File.mkdir doc_path; |
542 |
val root_path = Path.append doc_path (Path.basic "root.tex"); |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
543 |
val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path; |
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
544 |
val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path); |
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
545 |
val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path); |
14922 | 546 |
|
547 |
fun known name = |
|
548 |
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name))) |
|
20664 | 549 |
in member (op =) ss end; |
14922 | 550 |
val known_syms = known "syms.lst"; |
551 |
val known_ctrls = known "ctrls.lst"; |
|
552 |
||
15570 | 553 |
val _ = srcs |> List.app (fn (name, base, txt) => |
14935 | 554 |
Symbol.explode txt |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
555 |
|> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base) |
14935 | 556 |
|> File.write (Path.append doc_path (tex_path name))); |
14922 | 557 |
val _ = write_tex_index tex_index doc_path; |
17082 | 558 |
in isatool_document false doc_format documentN "" doc_path result_path end; |
14922 | 559 |
|
560 |
||
7685 | 561 |
end; |
562 |
||
6203 | 563 |
structure BasicPresent: BASIC_PRESENT = Present; |
564 |
open BasicPresent; |