author | wenzelm |
Tue, 14 Aug 2012 15:42:58 +0200 | |
changeset 48805 | c3ea910b3581 |
parent 48804 | 6348e5fca42e |
child 48933 | d25e47e32bc0 |
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 BASIC_PRESENT = |
|
8 |
sig |
|
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
9 |
val no_document: ('a -> 'b) -> 'a -> 'b (*not thread-safe!*) |
6203 | 10 |
end; |
11 |
||
12 |
signature PRESENT = |
|
13 |
sig |
|
7727 | 14 |
include BASIC_PRESENT |
24561 | 15 |
val session_name: theory -> string |
9452 | 16 |
val write_graph: {name: string, ID: string, dir: string, unfold: bool, |
17 |
path: string, parents: string list} list -> Path.T -> unit |
|
20577 | 18 |
val display_graph: {name: string, ID: string, dir: string, unfold: bool, |
19 |
path: string, parents: string list} list -> unit |
|
48543 | 20 |
datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty |
21 |
val dump_mode: string -> dump_mode |
|
48804
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48543
diff
changeset
|
22 |
val read_variant: string -> string * string |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
23 |
val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list -> |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
24 |
string list -> string -> string * dump_mode -> Url.T option * bool -> bool -> |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
25 |
theory list -> unit (*not thread-safe!*) |
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
26 |
val finish: unit -> unit (*not thread-safe!*) |
7727 | 27 |
val init_theory: string -> unit |
27862
8f727f7c8c1d
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27491
diff
changeset
|
28 |
val theory_source: string -> (unit -> HTML.text) -> unit |
9136 | 29 |
val theory_output: string -> string -> unit |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
30 |
val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory |
14922 | 31 |
val drafts: string -> Path.T list -> Path.T |
6203 | 32 |
end; |
33 |
||
7685 | 34 |
structure Present: PRESENT = |
35 |
struct |
|
36 |
||
7727 | 37 |
|
38 |
(** paths **) |
|
39 |
||
40 |
val tex_ext = Path.ext "tex"; |
|
41 |
val tex_path = tex_ext o Path.basic; |
|
42 |
val html_ext = Path.ext "html"; |
|
43 |
val html_path = html_ext o Path.basic; |
|
44 |
val index_path = Path.basic "index.html"; |
|
11856 | 45 |
val readme_html_path = Path.basic "README.html"; |
46 |
val readme_path = Path.basic "README"; |
|
17082 | 47 |
val documentN = "document"; |
48 |
val document_path = Path.basic documentN; |
|
8196 | 49 |
val doc_indexN = "session"; |
11856 | 50 |
val graph_path = Path.basic "session.graph"; |
51 |
val graph_pdf_path = Path.basic "session_graph.pdf"; |
|
52 |
val graph_eps_path = Path.basic "session_graph.eps"; |
|
7727 | 53 |
|
54 |
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
|
55 |
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
|
56 |
val pre_index_path = Path.explode ".session/pre-index"; |
7727 | 57 |
|
9044 | 58 |
fun mk_rel_path [] ys = Path.make ys |
59 |
| mk_rel_path xs [] = Path.appends (replicate (length xs) Path.parent) |
|
9416 | 60 |
| mk_rel_path (ps as x :: xs) (qs as y :: ys) = if x = y then mk_rel_path xs ys else |
9044 | 61 |
Path.appends (replicate (length ps) Path.parent @ [Path.make qs]); |
7727 | 62 |
|
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
63 |
fun show_path path = Path.implode (Path.append (File.pwd ()) path); |
11856 | 64 |
|
7727 | 65 |
|
14922 | 66 |
|
7727 | 67 |
(** additional theory data **) |
68 |
||
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
69 |
structure Browser_Info = Theory_Data |
22846 | 70 |
( |
9416 | 71 |
type T = {name: string, session: string list, is_local: bool}; |
27329 | 72 |
val empty = {name = "", session = [], is_local = false}: T; |
16503 | 73 |
fun extend _ = empty; |
33522 | 74 |
fun merge _ = empty; |
22846 | 75 |
); |
7727 | 76 |
|
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
77 |
val put_info = Browser_Info.put; |
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
78 |
val get_info = Browser_Info.get; |
24561 | 79 |
val session_name = #name o get_info; |
80 |
||
7727 | 81 |
|
82 |
||
83 |
(** graphs **) |
|
84 |
||
85 |
type graph_node = |
|
86 |
{name: string, ID: string, dir: string, unfold: bool, |
|
87 |
path: string, parents: string list}; |
|
88 |
||
9416 | 89 |
fun write_graph gr path = |
90 |
File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
|
91 |
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
|
28840 | 92 |
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); |
7727 | 93 |
|
20577 | 94 |
fun display_graph gr = |
95 |
let |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
96 |
val path = Isabelle_System.create_tmp_path "graph" ""; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
97 |
val _ = write_graph gr path; |
24561 | 98 |
val _ = writeln "Displaying graph ..."; |
40743 | 99 |
val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); |
20577 | 100 |
in () end; |
101 |
||
102 |
||
9416 | 103 |
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
|
104 |
fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy); |
7727 | 105 |
|
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
106 |
|
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
107 |
(*retrieve graph data from initial collection of theories*) |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
108 |
fun init_graph remote_path curr_sess = rev o map (fn thy => |
7727 | 109 |
let |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
110 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
111 |
val {name = sess_name, session, is_local} = get_info thy; |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
112 |
val entry = |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
113 |
{name = name, ID = ID_of session name, dir = sess_name, |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
114 |
path = |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
115 |
if null session then "" else |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
116 |
if is_some remote_path andalso not is_local then |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
117 |
Url.implode (Url.append (the remote_path) (Url.File |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
118 |
(Path.append (Path.make session) (html_path name)))) |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
119 |
else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)), |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
120 |
unfold = false, |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
121 |
parents = map ID_of_thy (Theory.parents_of thy)}; |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
122 |
in (0, entry) end); |
7727 | 123 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
124 |
fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) = |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
125 |
(i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr; |
7727 | 126 |
|
127 |
||
128 |
||
129 |
(** global browser info state **) |
|
130 |
||
131 |
(* type theory_info *) |
|
132 |
||
133 |
type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T}; |
|
134 |
||
135 |
fun make_theory_info (tex_source, html_source, html) = |
|
136 |
{tex_source = tex_source, html_source = html_source, html = html}: theory_info; |
|
137 |
||
138 |
val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty); |
|
139 |
||
140 |
fun map_theory_info f {tex_source, html_source, html} = |
|
141 |
make_theory_info (f (tex_source, html_source, html)); |
|
142 |
||
143 |
||
144 |
(* type browser_info *) |
|
145 |
||
11856 | 146 |
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list, |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
147 |
tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list}; |
7727 | 148 |
|
11856 | 149 |
fun make_browser_info (theories, files, tex_index, html_index, graph) = |
150 |
{theories = theories, files = files, tex_index = tex_index, html_index = html_index, |
|
9416 | 151 |
graph = graph}: browser_info; |
7727 | 152 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
153 |
val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []); |
7727 | 154 |
|
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
155 |
fun init_browser_info remote_path curr_sess thys = make_browser_info |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
156 |
(Symtab.empty, [], [], [], init_graph remote_path curr_sess thys); |
7727 | 157 |
|
11856 | 158 |
fun map_browser_info f {theories, files, tex_index, html_index, graph} = |
159 |
make_browser_info (f (theories, files, tex_index, html_index, graph)); |
|
7727 | 160 |
|
161 |
||
162 |
(* state *) |
|
163 |
||
32738 | 164 |
val browser_info = Unsynchronized.ref empty_browser_info; |
165 |
fun change_browser_info f = |
|
166 |
CRITICAL (fn () => Unsynchronized.change browser_info (map_browser_info f)); |
|
7727 | 167 |
|
32738 | 168 |
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
|
169 |
fun no_document f x = Unsynchronized.setmp suppress_tex_source true f x; |
7727 | 170 |
|
171 |
fun init_theory_info name info = |
|
11856 | 172 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
17412 | 173 |
(Symtab.update (name, info) theories, files, tex_index, html_index, graph)); |
7727 | 174 |
|
175 |
fun change_theory_info name f = |
|
42010 | 176 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
17412 | 177 |
(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
|
178 |
NONE => error ("Browser info: cannot access theory document " ^ quote name) |
17412 | 179 |
| SOME info => (Symtab.update (name, map_theory_info f info) theories, files, |
9416 | 180 |
tex_index, html_index, graph))); |
7727 | 181 |
|
182 |
||
11856 | 183 |
fun add_file file = |
184 |
change_browser_info (fn (theories, files, tex_index, html_index, graph) => |
|
185 |
(theories, file :: files, tex_index, html_index, graph)); |
|
186 |
||
7727 | 187 |
fun add_tex_index txt = |
11856 | 188 |
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
|
189 |
(theories, files, txt :: tex_index, html_index, graph)); |
7727 | 190 |
|
191 |
fun add_html_index txt = |
|
11856 | 192 |
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
|
193 |
(theories, files, tex_index, txt :: html_index, graph)); |
7727 | 194 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
195 |
fun add_graph_entry entry = |
11856 | 196 |
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
|
197 |
(theories, files, tex_index, html_index, ins_graph_entry entry graph)); |
7727 | 198 |
|
11057 | 199 |
fun add_tex_source name txt = |
200 |
if ! suppress_tex_source then () |
|
201 |
else change_theory_info name (fn (tex_source, html_source, html) => |
|
202 |
(Buffer.add txt tex_source, html_source, html)); |
|
7727 | 203 |
|
204 |
fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) => |
|
205 |
(tex_source, Buffer.add txt html_source, html)); |
|
206 |
||
207 |
||
208 |
||
209 |
(** global session state **) |
|
210 |
||
211 |
(* session_info *) |
|
212 |
||
48543 | 213 |
datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty; |
214 |
||
215 |
fun dump_mode "all" = Dump_all |
|
216 |
| dump_mode "tex" = Dump_tex |
|
217 |
| dump_mode "tex+sty" = Dump_tex_sty |
|
218 |
| dump_mode s = |
|
219 |
error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")"); |
|
220 |
||
7727 | 221 |
type session_info = |
222 |
{name: string, parent: string, session: string, path: string list, html_prefix: Path.T, |
|
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
223 |
info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
224 |
documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
225 |
verbose: bool, readme: Path.T option}; |
7727 | 226 |
|
9416 | 227 |
fun make_session_info |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
228 |
(name, parent, session, path, html_prefix, info, doc_format, doc_graph, doc_output, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
229 |
documents, doc_dump, remote_path, verbose, readme) = |
7802 | 230 |
{name = name, parent = parent, session = session, path = path, html_prefix = html_prefix, |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
231 |
info = info, doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
232 |
documents = documents, doc_dump = doc_dump, remote_path = remote_path, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
233 |
verbose = verbose, readme = readme}: session_info; |
7685 | 234 |
|
235 |
||
7727 | 236 |
(* state *) |
237 |
||
32738 | 238 |
val session_info = Unsynchronized.ref (NONE: session_info option); |
7727 | 239 |
|
42126 | 240 |
fun session_default x f = (case ! session_info of NONE => x | SOME info => f info); |
7727 | 241 |
|
242 |
||
243 |
||
14922 | 244 |
(** document preparation **) |
7727 | 245 |
|
246 |
(* maintain index *) |
|
247 |
||
248 |
val session_entries = |
|
249 |
HTML.session_entries o |
|
14898 | 250 |
map (fn name => (Url.File (Path.append (Path.basic name) index_path), name)); |
7727 | 251 |
|
252 |
fun get_entries dir = |
|
253 |
split_lines (File.read (Path.append dir session_entries_path)); |
|
254 |
||
255 |
fun put_entries entries dir = |
|
256 |
File.write (Path.append dir session_entries_path) (cat_lines entries); |
|
257 |
||
258 |
||
259 |
fun create_index dir = |
|
260 |
File.read (Path.append dir pre_index_path) ^ |
|
27862
8f727f7c8c1d
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27491
diff
changeset
|
261 |
session_entries (get_entries dir) ^ HTML.end_document |
7727 | 262 |
|> File.write (Path.append dir index_path); |
263 |
||
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
264 |
fun update_index dir name = |
7727 | 265 |
(case try get_entries dir of |
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
|
266 |
NONE => warning ("Browser info: cannot access session index of " ^ Path.print dir) |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
267 |
| SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)); |
7727 | 268 |
|
269 |
||
42004 | 270 |
(* document variants *) |
17082 | 271 |
|
42004 | 272 |
fun read_variant str = |
17082 | 273 |
(case space_explode "=" str of |
274 |
[name] => (name, "") |
|
275 |
| [name, tags] => (name, tags) |
|
42004 | 276 |
| _ => error ("Malformed document variant specification: " ^ quote str)); |
17082 | 277 |
|
278 |
||
7727 | 279 |
(* init session *) |
280 |
||
12895 | 281 |
fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
282 |
||
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
283 |
fun init build info info_path doc doc_graph document_output doc_variants path name |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
284 |
(doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys = |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
285 |
if not build andalso not info andalso doc = "" andalso dump_prefix = "" then |
15531 | 286 |
(browser_info := empty_browser_info; session_info := NONE) |
11856 | 287 |
else |
288 |
let |
|
33957 | 289 |
val parent_name = name_of_session (take (length path - 1) path); |
11856 | 290 |
val session_name = name_of_session path; |
291 |
val sess_prefix = Path.make path; |
|
48445 | 292 |
val html_prefix = Path.append (Path.expand (Path.explode info_path)) sess_prefix; |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
293 |
val doc_output = if document_output = "" then NONE else SOME (Path.explode document_output); |
7727 | 294 |
|
42007 | 295 |
val documents = |
296 |
if doc = "" then [] |
|
42005 | 297 |
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
|
298 |
(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
|
299 |
else (); []) |
48804
6348e5fca42e
more direct interpretation of document_variants for build (unchanged for usedir);
wenzelm
parents:
48543
diff
changeset
|
300 |
else doc_variants; |
7727 | 301 |
|
11856 | 302 |
val parent_index_path = Path.append Path.parent index_path; |
42007 | 303 |
val index_up_lnk = |
304 |
if first_time then |
|
16263
0609fb8df4a7
removed copy, copy_all (superceded by File.copy, File.copy_dir);
wenzelm
parents:
15801
diff
changeset
|
305 |
Url.append (the remote_path) (Url.File (Path.append sess_prefix parent_index_path)) |
14898 | 306 |
else Url.File parent_index_path; |
11856 | 307 |
val readme = |
15531 | 308 |
if File.exists readme_html_path then SOME readme_html_path |
309 |
else if File.exists readme_path then SOME readme_path |
|
310 |
else NONE; |
|
7727 | 311 |
|
17082 | 312 |
val docs = |
313 |
(case readme of NONE => [] | SOME p => [(Url.File p, "README")]) @ |
|
42007 | 314 |
map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents; |
11856 | 315 |
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
|
316 |
(Url.File index_path, session_name) docs (Url.explode "medium.html"); |
11856 | 317 |
in |
42007 | 318 |
session_info := |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
319 |
SOME (make_session_info (name, parent_name, session_name, path, html_prefix, info, doc, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
320 |
doc_graph, doc_output, documents, doc_dump, remote_path, verbose, readme)); |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
321 |
browser_info := init_browser_info remote_path path thys; |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
322 |
add_html_index (0, index_text) |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
323 |
end; |
7727 | 324 |
|
325 |
||
28496
4cff10648928
renamed isatool to isabelle_tool in programming interfaces;
wenzelm
parents:
28375
diff
changeset
|
326 |
(* isabelle tool wrappers *) |
17082 | 327 |
|
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
328 |
fun isabelle_document {verbose, purge} format name tags dir = |
17082 | 329 |
let |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
330 |
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
|
331 |
\-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
|
332 |
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
|
333 |
val _ = if verbose then writeln s else (); |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43712
diff
changeset
|
334 |
val (out, rc) = Isabelle_System.bash_output s; |
33682
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
335 |
val _ = |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
336 |
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
|
337 |
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
|
338 |
else if verbose then writeln out |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
339 |
else (); |
0c5d1485dea7
isabelle_document: more explicit error output, notably for drafts;
wenzelm
parents:
33522
diff
changeset
|
340 |
in doc_path end; |
17082 | 341 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
342 |
fun isabelle_browser graph = Isabelle_System.with_tmp_dir "browser" (fn dir => |
17082 | 343 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
344 |
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
|
345 |
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
|
346 |
val graph_path = Path.append dir graph_path; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
347 |
val _ = write_graph graph graph_path; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
348 |
val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path; |
17082 | 349 |
in |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
else error "Failed to prepare dependency graph" |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
354 |
end); |
17082 | 355 |
|
356 |
||
11856 | 357 |
(* finish session -- output all generated text *) |
358 |
||
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
359 |
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
|
360 |
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
|
361 |
|
14922 | 362 |
fun write_tex src name path = |
28027 | 363 |
File.write_buffer (Path.append path (tex_path name)) src; |
14922 | 364 |
|
365 |
fun write_tex_index tex_index path = |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
366 |
write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path; |
14922 | 367 |
|
7685 | 368 |
|
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
369 |
fun finish () = |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
370 |
session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output, |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
371 |
documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} => |
7727 | 372 |
let |
11856 | 373 |
val {theories, files, tex_index, html_index, graph} = ! browser_info; |
374 |
val thys = Symtab.dest theories; |
|
9416 | 375 |
val parent_html_prefix = Path.append html_prefix Path.parent; |
7727 | 376 |
|
11856 | 377 |
fun finish_html (a, {html, ...}: theory_info) = |
28027 | 378 |
File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html); |
11856 | 379 |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
380 |
val sorted_graph = sorted_index graph; |
11856 | 381 |
val opt_graphs = |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
382 |
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
|
383 |
SOME (isabelle_browser sorted_graph) |
15531 | 384 |
else NONE; |
11856 | 385 |
|
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
386 |
fun prepare_sources doc_dir doc_mode = |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
387 |
(Isabelle_System.mkdirs doc_dir; |
48543 | 388 |
(case doc_mode of |
389 |
Dump_all => Isabelle_System.copy_dir document_path doc_dir |
|
390 |
| Dump_tex_sty => |
|
391 |
ignore (Isabelle_System.isabelle_tool "latex" |
|
392 |
("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")))) |
|
393 |
| Dump_tex => ()); |
|
15531 | 394 |
(case opt_graphs of NONE => () | SOME (pdf, eps) => |
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
395 |
(File.write (Path.append doc_dir graph_pdf_path) pdf; |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
396 |
File.write (Path.append doc_dir graph_eps_path) eps)); |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
397 |
write_tex_index tex_index doc_dir; |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
398 |
List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys); |
42007 | 399 |
val _ = |
400 |
if info then |
|
401 |
(Isabelle_System.mkdirs (Path.append html_prefix session_path); |
|
402 |
File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index); |
|
403 |
File.write (Path.append html_prefix session_entries_path) ""; |
|
404 |
create_index html_prefix; |
|
405 |
if length path > 1 then update_index parent_html_prefix name else (); |
|
406 |
(case readme of NONE => () | SOME path => File.copy path html_prefix); |
|
407 |
write_graph sorted_graph (Path.append html_prefix graph_path); |
|
408 |
Isabelle_System.isabelle_tool "browser" "-b"; |
|
409 |
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; |
|
410 |
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) |
|
411 |
(HTML.applet_pages name (Url.File index_path, name)); |
|
43437 | 412 |
File.copy (Path.explode "~~/etc/isabelle.css") html_prefix; |
42007 | 413 |
List.app finish_html thys; |
414 |
List.app (uncurry File.write) files; |
|
44389
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
43850
diff
changeset
|
415 |
if verbose then Output.physical_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") |
42007 | 416 |
else ()) |
417 |
else (); |
|
418 |
||
419 |
val _ = |
|
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
420 |
if dump_prefix = "" then () |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
421 |
else |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
422 |
let |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
423 |
val path = Path.explode dump_prefix; |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
424 |
val _ = prepare_sources path dump_mode; |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
425 |
in |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
426 |
if verbose then |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
427 |
Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n") |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
428 |
else () |
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48445
diff
changeset
|
429 |
end; |
42007 | 430 |
|
431 |
val doc_paths = |
|
42009
b008525c4399
parallel preparation of document variants, within separate directories;
wenzelm
parents:
42008
diff
changeset
|
432 |
documents |> Par_List.map (fn (name, tags) => |
42007 | 433 |
let |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
434 |
val (doc_prefix, purge) = |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
435 |
(case doc_output of |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
436 |
SOME path => (path, false) |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
437 |
| NONE => (html_prefix, true)); |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
438 |
val _ = |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
439 |
File.eq (document_path, doc_prefix) andalso |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
440 |
error ("Overlap of document input and output directory " ^ Path.print doc_prefix); |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
441 |
val dir = Path.append doc_prefix (Path.basic name); |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
442 |
val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all; |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
443 |
val _ = prepare_sources dir mode; |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
444 |
in isabelle_document {verbose = true, purge = purge} doc_format name tags dir end); |
42007 | 445 |
val _ = |
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
446 |
if verbose orelse is_some doc_output then |
44389
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
43850
diff
changeset
|
447 |
doc_paths |
a3b5fdfb04a3
tuned signature -- contrast physical output primitives versus Output.raw_message;
wenzelm
parents:
43850
diff
changeset
|
448 |
|> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")) |
42007 | 449 |
else (); |
7727 | 450 |
in |
451 |
browser_info := empty_browser_info; |
|
15531 | 452 |
session_info := NONE |
42008
7423e833a880
Present.init/finish/no_document are not thread-safe -- eliminated futile CRITICAL sections;
wenzelm
parents:
42007
diff
changeset
|
453 |
end); |
7727 | 454 |
|
455 |
||
456 |
(* theory elements *) |
|
457 |
||
42126 | 458 |
fun init_theory name = session_default () (fn _ => init_theory_info name empty_theory_info); |
7727 | 459 |
|
27862
8f727f7c8c1d
removed obsolete verbatim_source, results, chapter, section etc.;
wenzelm
parents:
27491
diff
changeset
|
460 |
fun theory_source name mk_text = |
42126 | 461 |
session_default () (fn _ => add_html_source name (HTML.theory_source (mk_text ()))); |
7727 | 462 |
|
9136 | 463 |
fun theory_output name s = |
42126 | 464 |
session_default () (fn _ => add_tex_source name (Latex.isabelle_file name s)); |
7727 | 465 |
|
466 |
||
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
467 |
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
|
468 |
let |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
469 |
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
|
470 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
471 |
val link = |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
472 |
if null session then NONE |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
473 |
else SOME |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
474 |
(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
|
475 |
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
|
476 |
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
|
477 |
in (link, name) end; |
7727 | 478 |
|
26323
73efc70edeef
theory loader: discontinued *attached* ML scripts;
wenzelm
parents:
24829
diff
changeset
|
479 |
fun begin_theory update_time dir files thy = |
42126 | 480 |
session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} => |
7727 | 481 |
let |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
482 |
val name = Context.theory_name thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
483 |
val parents = Theory.parents_of thy; |
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
484 |
val parent_specs = map (parent_link remote_path path) parents; |
7727 | 485 |
|
37939
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
486 |
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
|
487 |
let |
43712
3c2c912af2ef
moved Outer_Syntax.load_thy to Thy_Load.load_thy;
wenzelm
parents:
43437
diff
changeset
|
488 |
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
|
489 |
val base = Path.base path; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
490 |
val base_html = html_ext base; |
965537d86fcc
discontinued special treatment of ML files -- no longer complete extensions on demand;
wenzelm
parents:
37216
diff
changeset
|
491 |
val _ = add_file (Path.append html_prefix base_html, |
37940
4857eab31298
generic external source files -- nothing special about ML here;
wenzelm
parents:
37939
diff
changeset
|
492 |
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
|
493 |
in (Url.File base_html, Url.File raw_path, loadit) end); |
7727 | 494 |
|
495 |
fun prep_html_source (tex_source, html_source, html) = |
|
496 |
let |
|
14898 | 497 |
val txt = HTML.begin_theory (Url.File index_path, session) |
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
|
498 |
name parent_specs files_html (Buffer.content html_source) |
7727 | 499 |
in (tex_source, Buffer.empty, Buffer.add txt html) end; |
500 |
||
9416 | 501 |
val entry = |
502 |
{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
|
503 |
path = Path.implode (html_path name), |
23899
ab37b1f690c7
clarified init/begin_theory: no longer depend on thy_info.ML;
wenzelm
parents:
23884
diff
changeset
|
504 |
parents = map ID_of_thy parents}; |
7727 | 505 |
in |
506 |
change_theory_info name prep_html_source; |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
507 |
add_graph_entry (update_time, entry); |
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
508 |
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
|
509 |
add_tex_index (update_time, Latex.theory_entry name); |
27327 | 510 |
put_info {name = sess_name, session = path, is_local = is_some remote_path} thy |
7727 | 511 |
end); |
512 |
||
513 |
||
514 |
||
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
515 |
(** draft document output **) |
14922 | 516 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
517 |
fun drafts doc_format src_paths = Isabelle_System.with_tmp_dir "drafts" (fn dir => |
14922 | 518 |
let |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
519 |
fun prep_draft path i = |
14935 | 520 |
let |
521 |
val base = Path.base path; |
|
14972 | 522 |
val name = |
24829 | 523 |
(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
|
524 |
"" => "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
|
525 |
| s => s) ^ serial_string (); |
14935 | 526 |
in |
527 |
if File.exists path then |
|
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
528 |
(((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
|
529 |
else error ("Bad file: " ^ Path.print path) |
14935 | 530 |
end; |
24150
ed724867099a
sort indexes according to symbolic update_time (multithreading-safe);
wenzelm
parents:
24102
diff
changeset
|
531 |
val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0)); |
14935 | 532 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
533 |
val doc_path = Path.append dir document_path; |
40743 | 534 |
val _ = Isabelle_System.mkdirs doc_path; |
14922 | 535 |
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
|
536 |
val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path; |
40743 | 537 |
val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path); |
538 |
val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path); |
|
14922 | 539 |
|
540 |
fun known name = |
|
541 |
let val ss = split_lines (File.read (Path.append doc_path (Path.basic name))) |
|
20664 | 542 |
in member (op =) ss end; |
14922 | 543 |
val known_syms = known "syms.lst"; |
544 |
val known_ctrls = known "ctrls.lst"; |
|
545 |
||
15570 | 546 |
val _ = srcs |> List.app (fn (name, base, txt) => |
14935 | 547 |
Symbol.explode txt |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
20664
diff
changeset
|
548 |
|> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base) |
14935 | 549 |
|> File.write (Path.append doc_path (tex_path name))); |
14922 | 550 |
val _ = write_tex_index tex_index doc_path; |
551 |
||
48805
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
552 |
val result = |
c3ea910b3581
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents:
48804
diff
changeset
|
553 |
isabelle_document {verbose = false, purge = true} doc_format documentN "" doc_path; |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
554 |
val result' = Isabelle_System.create_tmp_path documentN doc_format; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
555 |
val _ = File.copy result result'; |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
42126
diff
changeset
|
556 |
in result' end); |
14922 | 557 |
|
7685 | 558 |
end; |
559 |
||
32738 | 560 |
structure Basic_Present: BASIC_PRESENT = Present; |
561 |
open Basic_Present; |