author | wenzelm |
Sat, 27 Jul 2013 21:43:12 +0200 | |
changeset 52743 | a7d69a11f395 |
parent 52551 | f4fe75218cec |
child 53171 | a5e54d4d9081 |
permissions | -rw-r--r-- |
6203 | 1 |
(* Title: Pure/Thy/present.ML |
9416 | 2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
6203 | 3 |
|
9416 | 4 |
Theory presentation: HTML, graph files, (PDF)LaTeX documents. |
6203 | 5 |
*) |
6 |
||
7 |
signature PRESENT = |
|
8 |
sig |
|
24561 | 9 |
val session_name: theory -> string |
52551 | 10 |
val no_document: ('a -> 'b) -> 'a -> 'b (*not thread-safe!*) |
48804
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48543
diff
changeset
|
11 |
val read_variant: string -> string * string |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
12 |
val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
13 |
string * string -> bool * string -> bool -> theory list -> unit (*not thread-safe!*) |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
14 |
val finish: unit -> unit (*not thread-safe!*) |
7727 | 15 |
val init_theory: string -> unit |
27862
8f727f7c8c1d
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27491
diff
changeset
|
16 |
val theory_source: string -> (unit -> HTML.text) -> unit |
9136 | 17 |
val theory_output: string -> string -> unit |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50707
diff
changeset
|
18 |
val begin_theory: int -> Path.T -> theory -> theory |
52549 | 19 |
val display_drafts: Path.T list -> int |
6203 | 20 |
end; |
21 |
||
7685 | 22 |
structure Present: PRESENT = |
23 |
struct |
|
24 |
||
7727 | 25 |
|
26 |
(** paths **) |
|
27 |
||
28 |
val tex_ext = Path.ext "tex"; |
|
29 |
val tex_path = tex_ext o Path.basic; |
|
30 |
val html_ext = Path.ext "html"; |
|
31 |
val html_path = html_ext o Path.basic; |
|
32 |
val index_path = Path.basic "index.html"; |
|
11856 | 33 |
val readme_html_path = Path.basic "README.html"; |
17082 | 34 |
val documentN = "document"; |
35 |
val document_path = Path.basic documentN; |
|
8196 | 36 |
val doc_indexN = "session"; |
11856 | 37 |
val graph_path = Path.basic "session.graph"; |
38 |
val graph_pdf_path = Path.basic "session_graph.pdf"; |
|
39 |
val graph_eps_path = Path.basic "session_graph.eps"; |
|
7727 | 40 |
|
51415
8a33d581718b
show expanded path, to avoid odd /foo/bar/$ISABELLE_BROWSER_INFO/baz;
wenzelm
parents:
51401
diff
changeset
|
41 |
fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path)); |
11856 | 42 |
|
7727 | 43 |
|
14922 | 44 |
|
7727 | 45 |
(** additional theory data **) |
46 |
||
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
47 |
structure Browser_Info = Theory_Data |
22846 | 48 |
( |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
49 |
type T = {chapter: string, name: string}; |
51567
a86c5e02ba58
proper default browser info for interactive mode, notably thy_deps;
wenzelm
parents:
51419
diff
changeset
|
50 |
val empty = {chapter = "Unsorted", name = "Unknown"}: T; |
16503 | 51 |
fun extend _ = empty; |
33522 | 52 |
fun merge _ = empty; |
22846 | 53 |
); |
7727 | 54 |
|
51567
a86c5e02ba58
proper default browser info for interactive mode, notably thy_deps;
wenzelm
parents:
51419
diff
changeset
|
55 |
val _ = Context.>> (Context.map_theory |
a86c5e02ba58
proper default browser info for interactive mode, notably thy_deps;
wenzelm
parents:
51419
diff
changeset
|
56 |
(Browser_Info.put {chapter = Context.PureN, name = Context.PureN})); |
a86c5e02ba58
proper default browser info for interactive mode, notably thy_deps;
wenzelm
parents:
51419
diff
changeset
|
57 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
58 |
val session_name = #name o Browser_Info.get; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
59 |
val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get; |
24561 | 60 |
|
7727 | 61 |
|
62 |
||
63 |
(** graphs **) |
|
64 |
||
9416 | 65 |
fun ID_of sess s = space_implode "/" (sess @ [s]); |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
66 |
fun ID_of_thy thy = ID_of (session_chapter_name thy) (Context.theory_name thy); |
7727 | 67 |
|
51400 | 68 |
fun theory_link (curr_chapter, curr_session) thy = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
69 |
let |
51400 | 70 |
val {chapter, name = session} = Browser_Info.get thy; |
71 |
val link = html_path (Context.theory_name thy); |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
72 |
in |
51400 | 73 |
if curr_session = session then SOME link |
74 |
else if curr_chapter = chapter then |
|
75 |
SOME (Path.appends [Path.parent, Path.basic session, link]) |
|
76 |
else if chapter = Context.PureN then NONE |
|
77 |
else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link]) |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
78 |
end; |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
79 |
|
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
80 |
(*retrieve graph data from initial collection of theories*) |
51400 | 81 |
fun init_graph (curr_chapter, curr_session) = rev o map (fn thy => |
7727 | 82 |
let |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
83 |
val {chapter, name = session_name} = Browser_Info.get thy; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
84 |
val thy_name = Context.theory_name thy; |
51400 | 85 |
val path = |
86 |
(case theory_link (curr_chapter, curr_session) thy of |
|
87 |
NONE => "" |
|
88 |
| SOME p => Path.implode p); |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
89 |
val entry = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
90 |
{name = thy_name, |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
91 |
ID = ID_of [chapter, session_name] thy_name, |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
92 |
dir = session_name, |
51400 | 93 |
path = path, |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
94 |
unfold = false, |
49561 | 95 |
parents = map ID_of_thy (Theory.parents_of thy), |
96 |
content = []}; |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
97 |
in (0, entry) end); |
7727 | 98 |
|
49561 | 99 |
fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) = |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
100 |
(i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr; |
7727 | 101 |
|
102 |
||
103 |
||
104 |
(** global browser info state **) |
|
105 |
||
106 |
(* type theory_info *) |
|
107 |
||
108 |
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T}; |
|
109 |
||
110 |
fun make_theory_info (tex_source, html_source, html) = |
|
111 |
{tex_source = tex_source, html_source = html_source, html = html}: theory_info; |
|
112 |
||
113 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty); |
|
114 |
||
115 |
fun map_theory_info f {tex_source, html_source, html} = |
|
116 |
make_theory_info (f (tex_source, html_source, html)); |
|
117 |
||
118 |
||
119 |
(* type browser_info *) |
|
120 |
||
11856 | 121 |
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list, |
49561 | 122 |
tex_index: (int * string) list, html_index: (int * string) list, |
123 |
graph: (int * Graph_Display.node) list}; |
|
7727 | 124 |
|
11856 | 125 |
fun make_browser_info (theories, files, tex_index, html_index, graph) = |
126 |
{theories = theories, files = files, tex_index = tex_index, html_index = html_index, |
|
9416 | 127 |
graph = graph}: browser_info; |
7727 | 128 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
129 |
val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []); |
7727 | 130 |
|
51400 | 131 |
fun init_browser_info session thys = |
132 |
make_browser_info (Symtab.empty, [], [], [], init_graph session thys); |
|
7727 | 133 |
|
11856 | 134 |
fun map_browser_info f {theories, files, tex_index, html_index, graph} = |
135 |
make_browser_info (f (theories, files, tex_index, html_index, graph)); |
|
7727 | 136 |
|
137 |
||
138 |
(* state *) |
|
139 |
||
32738 | 140 |
val browser_info = Unsynchronized.ref empty_browser_info; |
141 |
fun change_browser_info f = |
|
142 |
CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f)); |
|
7727 | 143 |
|
32738 | 144 |
val suppress_tex_source = Unsynchronized.ref false; |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
145 |
fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x; |
7727 | 146 |
|
147 |
fun init_theory_info name info = |
|
11856 | 148 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
17412 | 149 |
(Symtab.update (name, info) theories, files, tex_index, html_index, graph)); |
7727 | 150 |
|
151 |
fun change_theory_info name f = |
|
42010 | 152 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
17412 | 153 |
(case Symtab.lookup theories name of |
27491
c8178a6a6480
begin_theory: files_html needs to be produced outside of prep_html_source to make ML files appear!
wenzelm
parents:
27329
diff
changeset
|
154 |
NONE => error ("Browser info: cannot access theory document " ^ quote name) |
17412 | 155 |
| SOME info => (Symtab.update (name, map_theory_info f info) theories, files, |
9416 | 156 |
tex_index, html_index, graph))); |
7727 | 157 |
|
158 |
||
11856 | 159 |
fun add_file file = |
160 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
|
161 |
(theories, file :: files, tex_index, html_index, graph)); |
|
162 |
||
7727 | 163 |
fun add_tex_index txt = |
11856 | 164 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
165 |
(theories, files, txt :: tex_index, html_index, graph)); |
7727 | 166 |
|
167 |
fun add_html_index txt = |
|
11856 | 168 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
169 |
(theories, files, tex_index, txt :: html_index, graph)); |
7727 | 170 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
171 |
fun add_graph_entry entry = |
11856 | 172 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
173 |
(theories, files, tex_index, html_index, ins_graph_entry entry graph)); |
7727 | 174 |
|
11057 | 175 |
fun add_tex_source name txt = |
176 |
if ! suppress_tex_source then () |
|
177 |
else change_theory_info name (fn (tex_source, html_source, html) => |
|
178 |
(Buffer.add txt tex_source, html_source, html)); |
|
7727 | 179 |
|
180 |
fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) => |
|
181 |
(tex_source, Buffer.add txt html_source, html)); |
|
182 |
||
183 |
||
184 |
||
185 |
(** global session state **) |
|
186 |
||
187 |
(* session_info *) |
|
188 |
||
189 |
type session_info = |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
190 |
{name: string, chapter: string, info_path: Path.T, |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
191 |
info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51293
diff
changeset
|
192 |
documents: (string * string) list, doc_dump: (bool * string), verbose: bool, |
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51293
diff
changeset
|
193 |
readme: Path.T option}; |
7727 | 194 |
|
9416 | 195 |
fun make_session_info |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
196 |
(name, chapter, info_path, info, doc_format, doc_graph, doc_output, |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51293
diff
changeset
|
197 |
documents, doc_dump, verbose, readme) = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
198 |
{name = name, chapter = chapter, info_path = info_path, info = info, |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
199 |
doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51293
diff
changeset
|
200 |
documents = documents, doc_dump = doc_dump, verbose = verbose, |
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51293
diff
changeset
|
201 |
readme = readme}: session_info; |
7685 | 202 |
|
203 |
||
7727 | 204 |
(* state *) |
205 |
||
32738 | 206 |
val session_info = Unsynchronized.ref (NONE: session_info option); |
7727 | 207 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
208 |
fun with_session_info x f = (case ! session_info of NONE => x | SOME info => f info); |
7727 | 209 |
|
210 |
||
211 |
||
14922 | 212 |
(** document preparation **) |
7727 | 213 |
|
42004 | 214 |
(* document variants *) |
17082 | 215 |
|
42004 | 216 |
fun read_variant str = |
17082 | 217 |
(case space_explode "=" str of |
218 |
[name] => (name, "") |
|
219 |
| [name, tags] => (name, tags) |
|
42004 | 220 |
| _ => error ("Malformed document variant specification: " ^ quote str)); |
17082 | 221 |
|
222 |
||
7727 | 223 |
(* init session *) |
224 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
225 |
fun init build info info_path doc doc_graph document_output doc_variants |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
226 |
(chapter, name) (doc_dump as (_, dump_prefix)) verbose thys = |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
227 |
if not build andalso not info andalso doc = "" andalso dump_prefix = "" then |
15531 | 228 |
(browser_info := empty_browser_info; session_info := NONE) |
11856 | 229 |
else |
230 |
let |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
231 |
val doc_output = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
232 |
if document_output = "" then NONE else SOME (Path.explode document_output); |
7727 | 233 |
|
42007 | 234 |
val documents = |
235 |
if doc = "" then [] |
|
42005 | 236 |
else if not (can File.check_dir document_path) then |
44389
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
43850
diff
changeset
|
237 |
(if verbose then Output.physical_stderr "Warning: missing document directory\n" |
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
43850
diff
changeset
|
238 |
else (); []) |
48804
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48543
diff
changeset
|
239 |
else doc_variants; |
7727 | 240 |
|
51419
5313abe76bd4
include only README.html, not historic README, which tends towards surprises like src/HOL/SPARK/Examples/README;
wenzelm
parents:
51415
diff
changeset
|
241 |
val readme = if File.exists readme_html_path then SOME readme_html_path else NONE; |
7727 | 242 |
|
17082 | 243 |
val docs = |
244 |
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
|
42007 | 245 |
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; |
11856 | 246 |
in |
42007 | 247 |
session_info := |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
248 |
SOME (make_session_info (name, chapter, info_path, info, doc, |
51398
c3d02b3518c2
discontinued "isabelle usedir" option -P (remote path);
wenzelm
parents:
51293
diff
changeset
|
249 |
doc_graph, doc_output, documents, doc_dump, verbose, readme)); |
51400 | 250 |
browser_info := init_browser_info (chapter, name) thys; |
51401 | 251 |
add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html")) |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
252 |
end; |
7727 | 253 |
|
254 |
||
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28375
diff
changeset
|
255 |
(* isabelle tool wrappers *) |
17082 | 256 |
|
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
257 |
fun isabelle_document {verbose, purge} format name tags dir = |
17082 | 258 |
let |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
259 |
val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \ |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
260 |
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path dir ^ " 2>&1"; |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
261 |
val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format]; |
33682
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
262 |
val _ = if verbose then writeln s else (); |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43712
diff
changeset
|
263 |
val (out, rc) = Isabelle_System.bash_output s; |
33682
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
264 |
val _ = |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
265 |
if not (File.exists doc_path) orelse rc <> 0 then |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
266 |
cat_error out ("Failed to build document " ^ quote (show_path doc_path)) |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
267 |
else if verbose then writeln out |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
268 |
else (); |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
269 |
in doc_path end; |
17082 | 270 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
271 |
fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir => |
17082 | 272 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
273 |
val pdf_path = Path.append dir graph_pdf_path; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
274 |
val eps_path = Path.append dir graph_eps_path; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
275 |
val graph_path = Path.append dir graph_path; |
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
276 |
val _ = Graph_Display.write_graph_browser graph_path graph; |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
277 |
val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path; |
17082 | 278 |
in |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
279 |
if Isabelle_System.isabelle_tool "browser" args = 0 andalso |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
280 |
File.exists pdf_path andalso File.exists eps_path |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
281 |
then (File.read pdf_path, File.read eps_path) |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
282 |
else error "Failed to prepare dependency graph" |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
283 |
end); |
17082 | 284 |
|
285 |
||
11856 | 286 |
(* finish session -- output all generated text *) |
287 |
||
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
288 |
fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index)); |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
289 |
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty; |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
290 |
|
14922 | 291 |
fun write_tex src name path = |
28027 | 292 |
File.write_buffer (Path.append path (tex_path name)) src; |
14922 | 293 |
|
294 |
fun write_tex_index tex_index path = |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
295 |
write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path; |
14922 | 296 |
|
7685 | 297 |
|
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
298 |
fun finish () = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
299 |
with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output, |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
300 |
documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} => |
7727 | 301 |
let |
11856 | 302 |
val {theories, files, tex_index, html_index, graph} = ! browser_info; |
303 |
val thys = Symtab.dest theories; |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
304 |
|
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
305 |
val chapter_prefix = Path.append info_path (Path.basic chapter); |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
306 |
val session_prefix = Path.append chapter_prefix (Path.basic name); |
7727 | 307 |
|
11856 | 308 |
fun finish_html (a, {html, ...}: theory_info) = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
309 |
File.write_buffer (Path.append session_prefix (html_path a)) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
310 |
(Buffer.add HTML.end_document html); |
11856 | 311 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
312 |
val sorted_graph = sorted_index graph; |
11856 | 313 |
val opt_graphs = |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
314 |
if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then |
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28375
diff
changeset
|
315 |
SOME (isabelle_browser sorted_graph) |
15531 | 316 |
else NONE; |
11856 | 317 |
|
42007 | 318 |
val _ = |
319 |
if info then |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
320 |
(Isabelle_System.mkdirs session_prefix; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
321 |
File.write_buffer (Path.append session_prefix index_path) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
322 |
(index_buffer html_index |> Buffer.add HTML.end_document); |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
323 |
(case readme of NONE => () | SOME path => File.copy path session_prefix); |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
324 |
Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph; |
42007 | 325 |
Isabelle_System.isabelle_tool "browser" "-b"; |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
326 |
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
327 |
List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt) |
42007 | 328 |
(HTML.applet_pages name (Url.File index_path, name)); |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
329 |
File.copy (Path.explode "~~/etc/isabelle.css") session_prefix; |
42007 | 330 |
List.app finish_html thys; |
331 |
List.app (uncurry File.write) files; |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
332 |
if verbose then Output.physical_stderr ("Browser info at " ^ show_path session_prefix ^ "\n") |
42007 | 333 |
else ()) |
334 |
else (); |
|
335 |
||
50121
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
336 |
fun prepare_sources doc_copy doc_dir = |
48933 | 337 |
(Isabelle_System.mkdirs doc_dir; |
50121
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
338 |
if doc_copy then Isabelle_System.copy_dir document_path doc_dir else (); |
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
339 |
Isabelle_System.isabelle_tool "latex" |
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
340 |
("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))); |
48933 | 341 |
(case opt_graphs of NONE => () | SOME (pdf, eps) => |
342 |
(File.write (Path.append doc_dir graph_pdf_path) pdf; |
|
343 |
File.write (Path.append doc_dir graph_eps_path) eps)); |
|
344 |
write_tex_index tex_index doc_dir; |
|
345 |
List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys); |
|
346 |
||
42007 | 347 |
val _ = |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
348 |
if dump_prefix = "" then () |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
349 |
else |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
350 |
let |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
351 |
val path = Path.explode dump_prefix; |
50121
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
352 |
val _ = prepare_sources dump_copy path; |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
353 |
in |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
354 |
if verbose then |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
355 |
Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
356 |
else () |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
357 |
end; |
42007 | 358 |
|
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
359 |
fun document_job doc_prefix backdrop (name, tags) = |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
360 |
let |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
361 |
val _ = |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
362 |
File.eq (document_path, doc_prefix) andalso |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
363 |
error ("Overlap of document input and output directory " ^ Path.print doc_prefix); |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
364 |
val dir = Path.append doc_prefix (Path.basic name); |
50121
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
365 |
val copy = not (File.eq (document_path, dir)); |
97d2b77313a0
isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
wenzelm
parents:
49565
diff
changeset
|
366 |
val _ = prepare_sources copy dir; |
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
367 |
fun inform doc = |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
368 |
if verbose orelse not backdrop then |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
369 |
Output.physical_stderr ("Document at " ^ show_path doc ^ "\n") |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
370 |
else (); |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
371 |
in |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
372 |
fn () => |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
373 |
(isabelle_document {verbose = true, purge = backdrop} doc_format name tags dir, inform) |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
374 |
end; |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
375 |
|
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
376 |
val jobs = |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
377 |
(if info orelse is_none doc_output then |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
378 |
map (document_job session_prefix true) documents |
48935
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
379 |
else []) @ |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
380 |
(case doc_output of |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
381 |
NONE => [] |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
382 |
| SOME path => map (document_job path false) documents); |
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
383 |
|
4c92a2f310b6
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
wenzelm
parents:
48933
diff
changeset
|
384 |
val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>); |
7727 | 385 |
in |
386 |
browser_info := empty_browser_info; |
|
15531 | 387 |
session_info := NONE |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
388 |
end); |
7727 | 389 |
|
390 |
||
391 |
(* theory elements *) |
|
392 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
393 |
fun init_theory name = with_session_info () (fn _ => init_theory_info name empty_theory_info); |
7727 | 394 |
|
27862
8f727f7c8c1d
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27491
diff
changeset
|
395 |
fun theory_source name mk_text = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
396 |
with_session_info () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); |
7727 | 397 |
|
9136 | 398 |
fun theory_output name s = |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
399 |
with_session_info () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
7727 | 400 |
|
401 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
402 |
fun begin_theory update_time dir thy = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
403 |
with_session_info thy (fn {name = session_name, chapter, info_path, ...} => |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
404 |
let |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
405 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
406 |
val parents = Theory.parents_of thy; |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
407 |
val parent_specs = parents |> map (fn parent => |
51400 | 408 |
(Option.map Url.File (theory_link (chapter, session_name) parent), |
409 |
(Context.theory_name parent))); |
|
7727 | 410 |
|
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
50707
diff
changeset
|
411 |
val files = []; (* FIXME *) |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
412 |
val files_html = files |> map (fn (raw_path, loadit) => |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
413 |
let |
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43437
diff
changeset
|
414 |
val path = File.check_file (File.full_path dir raw_path); |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
415 |
val base = Path.base path; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
416 |
val base_html = html_ext base; |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
417 |
(* FIXME retain file path!? *) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
418 |
val session_prefix = Path.appends [info_path, Path.basic chapter, Path.basic name]; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
419 |
val _ = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
420 |
add_file (Path.append session_prefix base_html, |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
421 |
HTML.external_file (Url.File base) (File.read path)); |
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
422 |
in (Url.File base_html, Url.File raw_path, loadit) end); |
7727 | 423 |
|
424 |
fun prep_html_source (tex_source, html_source, html) = |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
425 |
let val txt = HTML.begin_theory name parent_specs files_html (Buffer.content html_source) |
7727 | 426 |
in (tex_source, Buffer.empty, Buffer.add txt html) end; |
427 |
||
9416 | 428 |
val entry = |
51400 | 429 |
{name = name, |
430 |
ID = ID_of [chapter, session_name] name, |
|
431 |
dir = session_name, |
|
432 |
unfold = true, |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
433 |
path = Path.implode (html_path name), |
49561 | 434 |
parents = map ID_of_thy parents, |
435 |
content = []}; |
|
7727 | 436 |
in |
437 |
change_theory_info name prep_html_source; |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
438 |
add_graph_entry (update_time, entry); |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
439 |
add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name)); |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
440 |
add_tex_index (update_time, Latex.theory_entry name); |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
441 |
Browser_Info.put {chapter = chapter, name = session_name} thy |
7727 | 442 |
end); |
443 |
||
444 |
||
445 |
||
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
446 |
(** draft document output **) |
14922 | 447 |
|
52549 | 448 |
fun display_drafts src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir => |
14922 | 449 |
let |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
450 |
fun prep_draft path i = |
14935 | 451 |
let |
452 |
val base = Path.base path; |
|
14972 | 453 |
val name = |
24829 | 454 |
(case Path.implode (#1 (Path.split_ext base)) of |
44986
6f27ecf2a951
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
wenzelm
parents:
44389
diff
changeset
|
455 |
"" => "DUMMY" |
6f27ecf2a951
unique file names via serial numbers, to allow files like "root" or multiple files with same base name;
wenzelm
parents:
44389
diff
changeset
|
456 |
| s => s) ^ serial_string (); |
14935 | 457 |
in |
458 |
if File.exists path then |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
459 |
(((name, base, File.read path), (i, Latex.theory_entry name)), i + 1) |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41886
diff
changeset
|
460 |
else error ("Bad file: " ^ Path.print path) |
14935 | 461 |
end; |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
462 |
val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0)); |
14935 | 463 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
464 |
val doc_path = Path.append dir document_path; |
40743 | 465 |
val _ = Isabelle_System.mkdirs doc_path; |
14922 | 466 |
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
|
467 |
val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path; |
40743 | 468 |
val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path); |
469 |
val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path); |
|
14922 | 470 |
|
471 |
fun known name = |
|
472 |
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name))) |
|
20664 | 473 |
in member (op =) ss end; |
14922 | 474 |
val known_syms = known "syms.lst"; |
475 |
val known_ctrls = known "ctrls.lst"; |
|
476 |
||
15570 | 477 |
val _ = srcs |> List.app (fn (name, base, txt) => |
14935 | 478 |
Symbol.explode txt |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
479 |
|> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base) |
14935 | 480 |
|> File.write (Path.append doc_path (tex_path name))); |
14922 | 481 |
val _ = write_tex_index tex_index doc_path; |
482 |
||
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
483 |
val result = |
52743 | 484 |
isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path; |
485 |
val detachable_result = Isabelle_System.create_tmp_path documentN "pdf"; |
|
52549 | 486 |
val _ = File.copy result detachable_result; |
487 |
in |
|
488 |
Isabelle_System.isabelle_tool "display" ("-c " ^ File.shell_path detachable_result ^ " &") |
|
489 |
end); |
|
14922 | 490 |
|
7685 | 491 |
end; |
492 |