wenzelm@6203
|
1 |
(* Title: Pure/Thy/present.ML
|
wenzelm@9416
|
2 |
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen
|
wenzelm@6203
|
3 |
|
wenzelm@9416
|
4 |
Theory presentation: HTML, graph files, (PDF)LaTeX documents.
|
wenzelm@6203
|
5 |
*)
|
wenzelm@6203
|
6 |
|
wenzelm@6203
|
7 |
signature BASIC_PRESENT =
|
wenzelm@6203
|
8 |
sig
|
wenzelm@11057
|
9 |
val no_document: ('a -> 'b) -> 'a -> 'b
|
wenzelm@6203
|
10 |
end;
|
wenzelm@6203
|
11 |
|
wenzelm@6203
|
12 |
signature PRESENT =
|
wenzelm@6203
|
13 |
sig
|
wenzelm@7727
|
14 |
include BASIC_PRESENT
|
wenzelm@24561
|
15 |
val session_name: theory -> string
|
wenzelm@9452
|
16 |
val write_graph: {name: string, ID: string, dir: string, unfold: bool,
|
wenzelm@9452
|
17 |
path: string, parents: string list} list -> Path.T -> unit
|
wenzelm@20577
|
18 |
val display_graph: {name: string, ID: string, dir: string, unfold: bool,
|
wenzelm@20577
|
19 |
path: string, parents: string list} list -> unit
|
wenzelm@17082
|
20 |
val init: bool -> bool -> string -> bool -> string list -> string list ->
|
wenzelm@23899
|
21 |
string -> (bool * Path.T) option -> Url.T option * bool -> bool -> theory list -> unit
|
wenzelm@7727
|
22 |
val finish: unit -> unit
|
wenzelm@7727
|
23 |
val init_theory: string -> unit
|
wenzelm@27862
|
24 |
val theory_source: string -> (unit -> HTML.text) -> unit
|
wenzelm@9136
|
25 |
val theory_output: string -> string -> unit
|
wenzelm@24150
|
26 |
val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory
|
wenzelm@14922
|
27 |
val drafts: string -> Path.T list -> Path.T
|
wenzelm@6203
|
28 |
end;
|
wenzelm@6203
|
29 |
|
wenzelm@7685
|
30 |
structure Present: PRESENT =
|
wenzelm@7685
|
31 |
struct
|
wenzelm@7685
|
32 |
|
wenzelm@7685
|
33 |
|
wenzelm@7727
|
34 |
(** paths **)
|
wenzelm@7685
|
35 |
|
wenzelm@7727
|
36 |
val output_path = Path.variable "ISABELLE_BROWSER_INFO";
|
wenzelm@7685
|
37 |
|
wenzelm@7727
|
38 |
val tex_ext = Path.ext "tex";
|
wenzelm@7727
|
39 |
val tex_path = tex_ext o Path.basic;
|
wenzelm@7727
|
40 |
val html_ext = Path.ext "html";
|
wenzelm@7727
|
41 |
val html_path = html_ext o Path.basic;
|
wenzelm@7727
|
42 |
val index_path = Path.basic "index.html";
|
wenzelm@11856
|
43 |
val readme_html_path = Path.basic "README.html";
|
wenzelm@11856
|
44 |
val readme_path = Path.basic "README";
|
wenzelm@17082
|
45 |
val documentN = "document";
|
wenzelm@17082
|
46 |
val document_path = Path.basic documentN;
|
wenzelm@8196
|
47 |
val doc_indexN = "session";
|
wenzelm@11856
|
48 |
val graph_path = Path.basic "session.graph";
|
wenzelm@11856
|
49 |
val graph_pdf_path = Path.basic "session_graph.pdf";
|
wenzelm@11856
|
50 |
val graph_eps_path = Path.basic "session_graph.eps";
|
wenzelm@7727
|
51 |
|
wenzelm@7727
|
52 |
val session_path = Path.basic ".session";
|
wenzelm@21858
|
53 |
val session_entries_path = Path.explode ".session/entries";
|
wenzelm@21858
|
54 |
val pre_index_path = Path.explode ".session/pre-index";
|
wenzelm@7727
|
55 |
|
berghofe@9044
|
56 |
fun mk_rel_path [] ys = Path.make ys
|
berghofe@9044
|
57 |
| mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent)
|
wenzelm@9416
|
58 |
| mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else
|
berghofe@9044
|
59 |
Path.appends (replicate (length ps) Path.parent @ [Path.make qs]);
|
wenzelm@7727
|
60 |
|
wenzelm@21858
|
61 |
fun show_path path = Path.implode (Path.append (File.pwd ()) path);
|
wenzelm@11856
|
62 |
|
wenzelm@7727
|
63 |
|
wenzelm@14922
|
64 |
|
wenzelm@7727
|
65 |
(** additional theory data **)
|
wenzelm@7727
|
66 |
|
wenzelm@33522
|
67 |
structure BrowserInfoData = Theory_Data
|
wenzelm@22846
|
68 |
(
|
wenzelm@9416
|
69 |
type T = {name: string, session: string list, is_local: bool};
|
wenzelm@27329
|
70 |
val empty = {name = "", session = [], is_local = false}: T;
|
wenzelm@16503
|
71 |
fun extend _ = empty;
|
wenzelm@33522
|
72 |
fun merge _ = empty;
|
wenzelm@22846
|
73 |
);
|
wenzelm@7727
|
74 |
|
wenzelm@27327
|
75 |
val put_info = BrowserInfoData.put;
|
wenzelm@26957
|
76 |
val get_info = BrowserInfoData.get;
|
wenzelm@24561
|
77 |
val session_name = #name o get_info;
|
wenzelm@24561
|
78 |
|
wenzelm@7727
|
79 |
|
wenzelm@7727
|
80 |
|
wenzelm@7727
|
81 |
(** graphs **)
|
wenzelm@7727
|
82 |
|
wenzelm@7727
|
83 |
type graph_node =
|
wenzelm@7727
|
84 |
{name: string, ID: string, dir: string, unfold: bool,
|
wenzelm@7727
|
85 |
path: string, parents: string list};
|
wenzelm@7727
|
86 |
|
wenzelm@9416
|
87 |
fun write_graph gr path =
|
wenzelm@9416
|
88 |
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
|
wenzelm@9416
|
89 |
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
|
wenzelm@28840
|
90 |
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
|
wenzelm@7727
|
91 |
|
wenzelm@20577
|
92 |
fun display_graph gr =
|
wenzelm@20577
|
93 |
let
|
wenzelm@24561
|
94 |
val _ = writeln "Displaying graph ...";
|
wenzelm@21858
|
95 |
val path = File.tmp_path (Path.explode "tmp.graph");
|
wenzelm@20577
|
96 |
val _ = write_graph gr path;
|
wenzelm@40996
|
97 |
val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
|
wenzelm@20577
|
98 |
in () end;
|
wenzelm@20577
|
99 |
|
wenzelm@20577
|
100 |
|
wenzelm@9416
|
101 |
fun ID_of sess s = space_implode "/" (sess @ [s]);
|
wenzelm@23899
|
102 |
fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
|
wenzelm@7727
|
103 |
|
wenzelm@23899
|
104 |
|
wenzelm@23899
|
105 |
(*retrieve graph data from initial collection of theories*)
|
wenzelm@24150
|
106 |
fun init_graph remote_path curr_sess = rev o map (fn thy =>
|
wenzelm@7727
|
107 |
let
|
wenzelm@23899
|
108 |
val name = Context.theory_name thy;
|
wenzelm@23899
|
109 |
val {name = sess_name, session, is_local} = get_info thy;
|
wenzelm@9416
|
110 |
val path' = Path.append (Path.make session) (html_path name);
|
wenzelm@24150
|
111 |
val entry =
|
wenzelm@24150
|
112 |
{name = name, ID = ID_of session name, dir = sess_name,
|
wenzelm@24150
|
113 |
path =
|
wenzelm@24150
|
114 |
if null session then "" else
|
wenzelm@24150
|
115 |
if is_some remote_path andalso not is_local then
|
wenzelm@24150
|
116 |
Url.implode (Url.append (the remote_path) (Url.File
|
wenzelm@24150
|
117 |
(Path.append (Path.make session) (html_path name))))
|
wenzelm@24150
|
118 |
else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
|
wenzelm@24150
|
119 |
unfold = false,
|
wenzelm@24150
|
120 |
parents = map ID_of_thy (Theory.parents_of thy)};
|
wenzelm@24150
|
121 |
in (0, entry) end);
|
wenzelm@7727
|
122 |
|
wenzelm@24150
|
123 |
fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) =
|
wenzelm@24150
|
124 |
(i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
|
wenzelm@7727
|
125 |
|
wenzelm@7727
|
126 |
|
wenzelm@7727
|
127 |
|
wenzelm@7727
|
128 |
(** global browser info state **)
|
wenzelm@7727
|
129 |
|
wenzelm@7727
|
130 |
(* type theory_info *)
|
wenzelm@7727
|
131 |
|
wenzelm@7727
|
132 |
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
|
wenzelm@7727
|
133 |
|
wenzelm@7727
|
134 |
fun make_theory_info (tex_source, html_source, html) =
|
wenzelm@7727
|
135 |
{tex_source = tex_source, html_source = html_source, html = html}: theory_info;
|
wenzelm@7727
|
136 |
|
wenzelm@7727
|
137 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
|
wenzelm@7727
|
138 |
|
wenzelm@7727
|
139 |
fun map_theory_info f {tex_source, html_source, html} =
|
wenzelm@7727
|
140 |
make_theory_info (f (tex_source, html_source, html));
|
wenzelm@7727
|
141 |
|
wenzelm@7727
|
142 |
|
wenzelm@7727
|
143 |
(* type browser_info *)
|
wenzelm@7727
|
144 |
|
wenzelm@11856
|
145 |
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
|
wenzelm@24150
|
146 |
tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list};
|
wenzelm@7727
|
147 |
|
wenzelm@11856
|
148 |
fun make_browser_info (theories, files, tex_index, html_index, graph) =
|
wenzelm@11856
|
149 |
{theories = theories, files = files, tex_index = tex_index, html_index = html_index,
|
wenzelm@9416
|
150 |
graph = graph}: browser_info;
|
wenzelm@7727
|
151 |
|
wenzelm@24150
|
152 |
val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
|
wenzelm@7727
|
153 |
|
wenzelm@23899
|
154 |
fun init_browser_info remote_path curr_sess thys = make_browser_info
|
wenzelm@24150
|
155 |
(Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
|
wenzelm@7727
|
156 |
|
wenzelm@11856
|
157 |
fun map_browser_info f {theories, files, tex_index, html_index, graph} =
|
wenzelm@11856
|
158 |
make_browser_info (f (theories, files, tex_index, html_index, graph));
|
wenzelm@7727
|
159 |
|
wenzelm@7727
|
160 |
|
wenzelm@7727
|
161 |
(* state *)
|
wenzelm@7727
|
162 |
|
wenzelm@32738
|
163 |
val browser_info = Unsynchronized.ref empty_browser_info;
|
wenzelm@32738
|
164 |
fun change_browser_info f =
|
wenzelm@32738
|
165 |
CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f));
|
wenzelm@7727
|
166 |
|
wenzelm@32738
|
167 |
val suppress_tex_source = Unsynchronized.ref false;
|
wenzelm@39862
|
168 |
fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x; (* FIXME unreliable *)
|
wenzelm@7727
|
169 |
|
wenzelm@7727
|
170 |
fun init_theory_info name info =
|
wenzelm@11856
|
171 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
|
wenzelm@17412
|
172 |
(Symtab.update (name, info) theories, files, tex_index, html_index, graph));
|
wenzelm@7727
|
173 |
|
wenzelm@7727
|
174 |
fun change_theory_info name f =
|
wenzelm@11856
|
175 |
change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
|
wenzelm@17412
|
176 |
(case Symtab.lookup theories name of
|
wenzelm@27491
|
177 |
NONE => error ("Browser info: cannot access theory document " ^ quote name)
|
wenzelm@17412
|
178 |
| SOME info => (Symtab.update (name, map_theory_info f info) theories, files,
|
wenzelm@9416
|
179 |
tex_index, html_index, graph)));
|
wenzelm@7727
|
180 |
|
wenzelm@7727
|
181 |
|
wenzelm@11856
|
182 |
fun add_file file =
|
wenzelm@11856
|
183 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
|
wenzelm@11856
|
184 |
(theories, file :: files, tex_index, html_index, graph));
|
wenzelm@11856
|
185 |
|
wenzelm@7727
|
186 |
fun add_tex_index txt =
|
wenzelm@11856
|
187 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
|
wenzelm@24150
|
188 |
(theories, files, txt :: tex_index, html_index, graph));
|
wenzelm@7727
|
189 |
|
wenzelm@7727
|
190 |
fun add_html_index txt =
|
wenzelm@11856
|
191 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
|
wenzelm@24150
|
192 |
(theories, files, tex_index, txt :: html_index, graph));
|
wenzelm@7727
|
193 |
|
wenzelm@24150
|
194 |
fun add_graph_entry entry =
|
wenzelm@11856
|
195 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
|
wenzelm@24150
|
196 |
(theories, files, tex_index, html_index, ins_graph_entry entry graph));
|
wenzelm@7727
|
197 |
|
wenzelm@11057
|
198 |
fun add_tex_source name txt =
|
wenzelm@11057
|
199 |
if ! suppress_tex_source then ()
|
wenzelm@11057
|
200 |
else change_theory_info name (fn (tex_source, html_source, html) =>
|
wenzelm@11057
|
201 |
(Buffer.add txt tex_source, html_source, html));
|
wenzelm@7727
|
202 |
|
wenzelm@7727
|
203 |
fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
|
wenzelm@7727
|
204 |
(tex_source, Buffer.add txt html_source, html));
|
wenzelm@7727
|
205 |
|
wenzelm@7727
|
206 |
fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
|
wenzelm@7727
|
207 |
(tex_source, html_source, Buffer.add txt html));
|
wenzelm@7727
|
208 |
|
wenzelm@7727
|
209 |
|
wenzelm@7727
|
210 |
|
wenzelm@7727
|
211 |
(** global session state **)
|
wenzelm@7727
|
212 |
|
wenzelm@7727
|
213 |
(* session_info *)
|
wenzelm@7727
|
214 |
|
wenzelm@7727
|
215 |
type session_info =
|
wenzelm@7727
|
216 |
{name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
|
wenzelm@17082
|
217 |
info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
|
wenzelm@17210
|
218 |
doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option,
|
wenzelm@17210
|
219 |
remote_path: Url.T option, verbose: bool, readme: Path.T option};
|
wenzelm@7727
|
220 |
|
wenzelm@9416
|
221 |
fun make_session_info
|
wenzelm@17082
|
222 |
(name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
|
wenzelm@17082
|
223 |
doc_prefix1, doc_prefix2, remote_path, verbose, readme) =
|
wenzelm@7802
|
224 |
{name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
|
wenzelm@17082
|
225 |
info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
|
wenzelm@17082
|
226 |
doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path,
|
wenzelm@17082
|
227 |
verbose = verbose, readme = readme}: session_info;
|
wenzelm@7727
|
228 |
|
wenzelm@7727
|
229 |
|
wenzelm@7727
|
230 |
(* state *)
|
wenzelm@7727
|
231 |
|
wenzelm@32738
|
232 |
val session_info = Unsynchronized.ref (NONE: session_info option);
|
wenzelm@7727
|
233 |
|
skalberg@15531
|
234 |
fun with_session x f = (case ! session_info of NONE => x | SOME info => f info);
|
wenzelm@26433
|
235 |
fun with_context f = f (Context.theory_name (ML_Context.the_global_context ()));
|
wenzelm@7727
|
236 |
|
wenzelm@7727
|
237 |
|
wenzelm@7727
|
238 |
|
wenzelm@14922
|
239 |
(** document preparation **)
|
wenzelm@7727
|
240 |
|
wenzelm@7727
|
241 |
(* maintain index *)
|
wenzelm@7727
|
242 |
|
wenzelm@7727
|
243 |
val session_entries =
|
wenzelm@7727
|
244 |
HTML.session_entries o
|
wenzelm@14898
|
245 |
map (fn name => (Url.File (Path.append (Path.basic name) index_path), name));
|
wenzelm@7727
|
246 |
|
wenzelm@7727
|
247 |
fun get_entries dir =
|
wenzelm@7727
|
248 |
split_lines (File.read (Path.append dir session_entries_path));
|
wenzelm@7727
|
249 |
|
wenzelm@7727
|
250 |
fun put_entries entries dir =
|
wenzelm@7727
|
251 |
File.write (Path.append dir session_entries_path) (cat_lines entries);
|
wenzelm@7727
|
252 |
|
wenzelm@7727
|
253 |
|
wenzelm@7727
|
254 |
fun create_index dir =
|
wenzelm@7727
|
255 |
File.read (Path.append dir pre_index_path) ^
|
wenzelm@27862
|
256 |
session_entries (get_entries dir) ^ HTML.end_document
|
wenzelm@7727
|
257 |
|> File.write (Path.append dir index_path);
|
wenzelm@7727
|
258 |
|
wenzelm@24150
|
259 |
fun update_index dir name = CRITICAL (fn () =>
|
wenzelm@7727
|
260 |
(case try get_entries dir of
|
wenzelm@21858
|
261 |
NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
|
wenzelm@24150
|
262 |
| SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
|
wenzelm@7727
|
263 |
|
wenzelm@7727
|
264 |
|
wenzelm@17082
|
265 |
(* document versions *)
|
wenzelm@17082
|
266 |
|
wenzelm@17082
|
267 |
fun read_version str =
|
wenzelm@17082
|
268 |
(case space_explode "=" str of
|
wenzelm@17082
|
269 |
[name] => (name, "")
|
wenzelm@17082
|
270 |
| [name, tags] => (name, tags)
|
wenzelm@17082
|
271 |
| _ => error ("Malformed document version specification: " ^ quote str));
|
wenzelm@17082
|
272 |
|
wenzelm@17082
|
273 |
fun read_versions strs =
|
wenzelm@19046
|
274 |
rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
|
wenzelm@28375
|
275 |
|> filter_out (fn (_, s) => s = "-");
|
wenzelm@17082
|
276 |
|
wenzelm@17082
|
277 |
|
wenzelm@7727
|
278 |
(* init session *)
|
wenzelm@7727
|
279 |
|
wenzelm@7727
|
280 |
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
|
wenzelm@7727
|
281 |
|
wenzelm@17082
|
282 |
fun init build info doc doc_graph doc_versions path name doc_prefix2
|
wenzelm@23944
|
283 |
(remote_path, first_time) verbose thys = CRITICAL (fn () =>
|
wenzelm@11911
|
284 |
if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
|
skalberg@15531
|
285 |
(browser_info := empty_browser_info; session_info := NONE)
|
wenzelm@11856
|
286 |
else
|
wenzelm@11856
|
287 |
let
|
haftmann@33956
|
288 |
val parent_name = name_of_session (take (length path - 1) path);
|
wenzelm@11856
|
289 |
val session_name = name_of_session path;
|
wenzelm@11856
|
290 |
val sess_prefix = Path.make path;
|
wenzelm@11856
|
291 |
val html_prefix = Path.append (Path.expand output_path) sess_prefix;
|
wenzelm@7727
|
292 |
|
wenzelm@17082
|
293 |
val (doc_prefix1, documents) =
|
wenzelm@17082
|
294 |
if doc = "" then (NONE, [])
|
wenzelm@21962
|
295 |
else if not (File.exists document_path) then
|
wenzelm@40026
|
296 |
(if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
|
wenzelm@22580
|
297 |
(NONE, []))
|
wenzelm@17082
|
298 |
else (SOME (Path.append html_prefix document_path, html_prefix),
|
wenzelm@17082
|
299 |
read_versions doc_versions);
|
wenzelm@7727
|
300 |
|
wenzelm@11856
|
301 |
val parent_index_path = Path.append Path.parent index_path;
|
wenzelm@11856
|
302 |
val index_up_lnk = if first_time then
|
wenzelm@16263
|
303 |
Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path))
|
wenzelm@14898
|
304 |
else Url.File parent_index_path;
|
wenzelm@11856
|
305 |
val readme =
|
skalberg@15531
|
306 |
if File.exists readme_html_path then SOME readme_html_path
|
skalberg@15531
|
307 |
else if File.exists readme_path then SOME readme_path
|
skalberg@15531
|
308 |
else NONE;
|
wenzelm@7727
|
309 |
|
wenzelm@17082
|
310 |
val docs =
|
wenzelm@17082
|
311 |
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @
|
wenzelm@17082
|
312 |
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
|
wenzelm@11856
|
313 |
val index_text = HTML.begin_index (index_up_lnk, parent_name)
|
wenzelm@21858
|
314 |
(Url.File index_path, session_name) docs (Url.explode "medium.html");
|
wenzelm@11856
|
315 |
in
|
skalberg@15531
|
316 |
session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
|
wenzelm@17082
|
317 |
info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
|
wenzelm@23899
|
318 |
browser_info := init_browser_info remote_path path thys;
|
wenzelm@24150
|
319 |
add_html_index (0, index_text)
|
wenzelm@23944
|
320 |
end);
|
wenzelm@7727
|
321 |
|
wenzelm@7727
|
322 |
|
wenzelm@28496
|
323 |
(* isabelle tool wrappers *)
|
wenzelm@17082
|
324 |
|
wenzelm@28496
|
325 |
fun isabelle_document verbose format name tags path result_path =
|
wenzelm@17082
|
326 |
let
|
wenzelm@28500
|
327 |
val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
|
wenzelm@33682
|
328 |
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^ " 2>&1";
|
wenzelm@17082
|
329 |
val doc_path = Path.append result_path (Path.ext format (Path.basic name));
|
wenzelm@33682
|
330 |
val _ = if verbose then writeln s else ();
|
wenzelm@35010
|
331 |
val (out, rc) = bash_output s;
|
wenzelm@33682
|
332 |
val _ =
|
wenzelm@33682
|
333 |
if not (File.exists doc_path) orelse rc <> 0 then
|
wenzelm@33682
|
334 |
cat_error out ("Failed to build document " ^ quote (show_path doc_path))
|
wenzelm@33682
|
335 |
else if verbose then writeln out
|
wenzelm@33682
|
336 |
else ();
|
wenzelm@33682
|
337 |
in doc_path end;
|
wenzelm@17082
|
338 |
|
wenzelm@28496
|
339 |
fun isabelle_browser graph =
|
wenzelm@17082
|
340 |
let
|
wenzelm@17082
|
341 |
val pdf_path = File.tmp_path graph_pdf_path;
|
wenzelm@17082
|
342 |
val eps_path = File.tmp_path graph_eps_path;
|
wenzelm@17082
|
343 |
val gr_path = File.tmp_path graph_path;
|
wenzelm@31819
|
344 |
val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
|
wenzelm@17082
|
345 |
in
|
wenzelm@17082
|
346 |
write_graph graph gr_path;
|
wenzelm@40996
|
347 |
if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
|
wenzelm@31819
|
348 |
not (File.exists eps_path) orelse not (File.exists pdf_path)
|
wenzelm@17082
|
349 |
then error "Failed to prepare dependency graph"
|
wenzelm@17082
|
350 |
else
|
wenzelm@17082
|
351 |
let val pdf = File.read pdf_path and eps = File.read eps_path
|
wenzelm@17082
|
352 |
in File.rm pdf_path; File.rm eps_path; File.rm gr_path; (pdf, eps) end
|
wenzelm@17082
|
353 |
end;
|
wenzelm@17082
|
354 |
|
wenzelm@17082
|
355 |
|
wenzelm@11856
|
356 |
(* finish session -- output all generated text *)
|
wenzelm@7727
|
357 |
|
wenzelm@24150
|
358 |
fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index));
|
wenzelm@24150
|
359 |
fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
|
wenzelm@24150
|
360 |
|
wenzelm@14922
|
361 |
fun write_tex src name path =
|
wenzelm@28027
|
362 |
File.write_buffer (Path.append path (tex_path name)) src;
|
wenzelm@14922
|
363 |
|
wenzelm@14922
|
364 |
fun write_tex_index tex_index path =
|
wenzelm@24150
|
365 |
write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
|
wenzelm@14922
|
366 |
|
wenzelm@7727
|
367 |
|
wenzelm@23944
|
368 |
fun finish () = CRITICAL (fn () =>
|
wenzelm@23944
|
369 |
with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
|
wenzelm@23944
|
370 |
documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
|
wenzelm@7727
|
371 |
let
|
wenzelm@11856
|
372 |
val {theories, files, tex_index, html_index, graph} = ! browser_info;
|
wenzelm@11856
|
373 |
val thys = Symtab.dest theories;
|
wenzelm@9416
|
374 |
val parent_html_prefix = Path.append html_prefix Path.parent;
|
wenzelm@7727
|
375 |
|
wenzelm@11856
|
376 |
fun finish_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
|
wenzelm@11856
|
377 |
fun finish_html (a, {html, ...}: theory_info) =
|
wenzelm@28027
|
378 |
File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
|
wenzelm@11856
|
379 |
|
wenzelm@24150
|
380 |
val sorted_graph = sorted_index graph;
|
wenzelm@11856
|
381 |
val opt_graphs =
|
wenzelm@16263
|
382 |
if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
|
wenzelm@28496
|
383 |
SOME (isabelle_browser sorted_graph)
|
skalberg@15531
|
384 |
else NONE;
|
wenzelm@11856
|
385 |
|
wenzelm@17210
|
386 |
fun prepare_sources cp path =
|
wenzelm@40996
|
387 |
(Isabelle_System.mkdirs path;
|
wenzelm@40996
|
388 |
if cp then Isabelle_System.copy_dir document_path path else ();
|
wenzelm@40996
|
389 |
Isabelle_System.isabelle_tool "latex"
|
wenzelm@31819
|
390 |
("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
|
skalberg@15531
|
391 |
(case opt_graphs of NONE => () | SOME (pdf, eps) =>
|
wenzelm@11856
|
392 |
(File.write (Path.append path graph_pdf_path) pdf;
|
wenzelm@11856
|
393 |
File.write (Path.append path graph_eps_path) eps));
|
wenzelm@14922
|
394 |
write_tex_index tex_index path;
|
skalberg@15570
|
395 |
List.app (finish_tex path) thys);
|
wenzelm@7727
|
396 |
in
|
wenzelm@21962
|
397 |
if info then
|
wenzelm@40996
|
398 |
(Isabelle_System.mkdirs (Path.append html_prefix session_path);
|
wenzelm@28027
|
399 |
File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
|
wenzelm@11856
|
400 |
File.write (Path.append html_prefix session_entries_path) "";
|
wenzelm@11856
|
401 |
create_index html_prefix;
|
wenzelm@11856
|
402 |
if length path > 1 then update_index parent_html_prefix name else ();
|
wenzelm@16263
|
403 |
(case readme of NONE => () | SOME path => File.copy path html_prefix);
|
wenzelm@24150
|
404 |
write_graph sorted_graph (Path.append html_prefix graph_path);
|
wenzelm@40996
|
405 |
Isabelle_System.isabelle_tool "browser" "-b";
|
wenzelm@21858
|
406 |
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
|
skalberg@15570
|
407 |
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
|
wenzelm@14898
|
408 |
(HTML.applet_pages name (Url.File index_path, name));
|
wenzelm@21858
|
409 |
File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
|
skalberg@15570
|
410 |
List.app finish_html thys;
|
skalberg@15570
|
411 |
List.app (uncurry File.write) files;
|
wenzelm@40026
|
412 |
if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
|
wenzelm@21962
|
413 |
else ();
|
wenzelm@11856
|
414 |
|
wenzelm@17210
|
415 |
(case doc_prefix2 of NONE => () | SOME (cp, path) =>
|
wenzelm@17210
|
416 |
(prepare_sources cp path;
|
wenzelm@40026
|
417 |
if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
|
wenzelm@12895
|
418 |
|
wenzelm@17082
|
419 |
(case doc_prefix1 of NONE => () | SOME (path, result_path) =>
|
wenzelm@17082
|
420 |
documents |> List.app (fn (name, tags) =>
|
wenzelm@17082
|
421 |
let
|
wenzelm@17210
|
422 |
val _ = prepare_sources true path;
|
wenzelm@28496
|
423 |
val doc_path = isabelle_document true doc_format name tags path result_path;
|
wenzelm@17082
|
424 |
in
|
wenzelm@40026
|
425 |
if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
|
wenzelm@17082
|
426 |
end));
|
wenzelm@11856
|
427 |
|
wenzelm@7727
|
428 |
browser_info := empty_browser_info;
|
skalberg@15531
|
429 |
session_info := NONE
|
wenzelm@23944
|
430 |
end));
|
wenzelm@7727
|
431 |
|
wenzelm@7727
|
432 |
|
wenzelm@7727
|
433 |
(* theory elements *)
|
wenzelm@7727
|
434 |
|
wenzelm@7727
|
435 |
fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
|
wenzelm@7727
|
436 |
|
wenzelm@27862
|
437 |
fun theory_source name mk_text =
|
wenzelm@27862
|
438 |
with_session () (fn _ => add_html_source name (HTML.theory_source (mk_text ())));
|
wenzelm@7727
|
439 |
|
wenzelm@9136
|
440 |
fun theory_output name s =
|
wenzelm@9917
|
441 |
with_session () (fn _ => add_tex_source name (Latex.isabelle_file name s));
|
wenzelm@7727
|
442 |
|
wenzelm@7727
|
443 |
|
wenzelm@23899
|
444 |
fun parent_link remote_path curr_session thy =
|
wenzelm@23899
|
445 |
let
|
wenzelm@23899
|
446 |
val {name = _, session, is_local} = get_info thy;
|
wenzelm@23899
|
447 |
val name = Context.theory_name thy;
|
wenzelm@23899
|
448 |
val link =
|
wenzelm@23899
|
449 |
if null session then NONE
|
wenzelm@23899
|
450 |
else SOME
|
wenzelm@23899
|
451 |
(if is_some remote_path andalso not is_local then
|
wenzelm@23899
|
452 |
Url.append (the remote_path) (Url.File (Path.append (Path.make session) (html_path name)))
|
wenzelm@23899
|
453 |
else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
|
wenzelm@23899
|
454 |
in (link, name) end;
|
wenzelm@7727
|
455 |
|
wenzelm@26323
|
456 |
fun begin_theory update_time dir files thy =
|
wenzelm@9416
|
457 |
with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
|
wenzelm@7727
|
458 |
let
|
wenzelm@23899
|
459 |
val name = Context.theory_name thy;
|
wenzelm@23899
|
460 |
val parents = Theory.parents_of thy;
|
wenzelm@23899
|
461 |
val parent_specs = map (parent_link remote_path path) parents;
|
wenzelm@7727
|
462 |
|
wenzelm@38188
|
463 |
val files_html = files |> map (fn (raw_path, loadit) =>
|
wenzelm@38188
|
464 |
let
|
wenzelm@38379
|
465 |
val path = #1 (Thy_Load.check_file [dir] raw_path);
|
wenzelm@38188
|
466 |
val base = Path.base path;
|
wenzelm@38188
|
467 |
val base_html = html_ext base;
|
wenzelm@38188
|
468 |
val _ = add_file (Path.append html_prefix base_html,
|
wenzelm@38189
|
469 |
HTML.external_file (Url.File base) (File.read path));
|
wenzelm@38188
|
470 |
in (Url.File base_html, Url.File raw_path, loadit) end);
|
wenzelm@7727
|
471 |
|
wenzelm@7727
|
472 |
fun prep_html_source (tex_source, html_source, html) =
|
wenzelm@7727
|
473 |
let
|
wenzelm@14898
|
474 |
val txt = HTML.begin_theory (Url.File index_path, session)
|
wenzelm@27491
|
475 |
name parent_specs files_html (Buffer.content html_source)
|
wenzelm@7727
|
476 |
in (tex_source, Buffer.empty, Buffer.add txt html) end;
|
wenzelm@7727
|
477 |
|
wenzelm@9416
|
478 |
val entry =
|
wenzelm@9416
|
479 |
{name = name, ID = ID_of path name, dir = sess_name, unfold = true,
|
wenzelm@21858
|
480 |
path = Path.implode (html_path name),
|
wenzelm@23899
|
481 |
parents = map ID_of_thy parents};
|
wenzelm@7727
|
482 |
in
|
wenzelm@7727
|
483 |
change_theory_info name prep_html_source;
|
wenzelm@24150
|
484 |
add_graph_entry (update_time, entry);
|
wenzelm@24150
|
485 |
add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
|
wenzelm@24150
|
486 |
add_tex_index (update_time, Latex.theory_entry name);
|
wenzelm@27327
|
487 |
put_info {name = sess_name, session = path, is_local = is_some remote_path} thy
|
wenzelm@7727
|
488 |
end);
|
wenzelm@7727
|
489 |
|
wenzelm@7727
|
490 |
|
wenzelm@7727
|
491 |
|
wenzelm@14922
|
492 |
(** draft document output **)
|
wenzelm@14922
|
493 |
|
wenzelm@14922
|
494 |
fun drafts doc_format src_paths =
|
wenzelm@14922
|
495 |
let
|
wenzelm@24150
|
496 |
fun prep_draft path i =
|
wenzelm@14935
|
497 |
let
|
wenzelm@14935
|
498 |
val base = Path.base path;
|
wenzelm@14972
|
499 |
val name =
|
wenzelm@24829
|
500 |
(case Path.implode (#1 (Path.split_ext base)) of
|
wenzelm@24829
|
501 |
"" => "DUMMY" ^ serial_string ()
|
wenzelm@24829
|
502 |
| s => s);
|
wenzelm@14935
|
503 |
in
|
wenzelm@14935
|
504 |
if File.exists path then
|
wenzelm@24150
|
505 |
(((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
|
wenzelm@21858
|
506 |
else error ("Bad file: " ^ quote (Path.implode path))
|
wenzelm@14935
|
507 |
end;
|
wenzelm@24150
|
508 |
val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
|
wenzelm@14935
|
509 |
|
wenzelm@17082
|
510 |
val doc_path = File.tmp_path document_path;
|
wenzelm@17082
|
511 |
val result_path = Path.append doc_path Path.parent;
|
wenzelm@40996
|
512 |
val _ = Isabelle_System.mkdirs doc_path;
|
wenzelm@14922
|
513 |
val root_path = Path.append doc_path (Path.basic "root.tex");
|
wenzelm@21858
|
514 |
val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
|
wenzelm@40996
|
515 |
val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
|
wenzelm@40996
|
516 |
val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
|
wenzelm@14922
|
517 |
|
wenzelm@14922
|
518 |
fun known name =
|
wenzelm@14922
|
519 |
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
|
wenzelm@20664
|
520 |
in member (op =) ss end;
|
wenzelm@14922
|
521 |
val known_syms = known "syms.lst";
|
wenzelm@14922
|
522 |
val known_ctrls = known "ctrls.lst";
|
wenzelm@14922
|
523 |
|
skalberg@15570
|
524 |
val _ = srcs |> List.app (fn (name, base, txt) =>
|
wenzelm@14935
|
525 |
Symbol.explode txt
|
wenzelm@21858
|
526 |
|> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
|
wenzelm@14935
|
527 |
|> File.write (Path.append doc_path (tex_path name)));
|
wenzelm@14922
|
528 |
val _ = write_tex_index tex_index doc_path;
|
wenzelm@28496
|
529 |
in isabelle_document false doc_format documentN "" doc_path result_path end;
|
wenzelm@14922
|
530 |
|
wenzelm@14922
|
531 |
|
wenzelm@7685
|
532 |
end;
|
wenzelm@7685
|
533 |
|
wenzelm@32738
|
534 |
structure Basic_Present: BASIC_PRESENT = Present;
|
wenzelm@32738
|
535 |
open Basic_Present;
|