1 (* Title: Pure/Thy/browser_info.ML |
|
2 ID: $Id$ |
|
3 Author: Stefan Berghofer and Markus Wenzel, TU Muenchen |
|
4 |
|
5 Theory browsing information (HTML and graph files). |
|
6 *) |
|
7 |
|
8 signature BASIC_BROWSER_INFO = |
|
9 sig |
|
10 val section: string -> unit |
|
11 end; |
|
12 |
|
13 signature BROWSER_INFO = |
|
14 sig |
|
15 include BASIC_BROWSER_INFO |
|
16 val init: bool -> string list -> string -> Url.T option * bool -> unit |
|
17 val finish: unit -> unit |
|
18 val theory_source: bool -> string -> (string, string list) Source.source * Position.T -> unit |
|
19 val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
|
20 val end_theory: string -> unit |
|
21 val result: string -> string -> thm -> unit |
|
22 val results: string -> string -> thm list -> unit |
|
23 val theorem: string -> thm -> unit |
|
24 val theorems: string -> thm list -> unit |
|
25 val subsection: string -> unit |
|
26 val subsubsection: string -> unit |
|
27 val setup: (theory -> theory) list |
|
28 end; |
|
29 |
|
30 structure BrowserInfo: BROWSER_INFO = |
|
31 struct |
|
32 |
|
33 |
|
34 (** paths **) |
|
35 |
|
36 val output_path = Path.variable "ISABELLE_BROWSER_INFO"; |
|
37 |
|
38 fun top_path sess_path offset = |
|
39 Path.append (Path.appends (replicate (offset + length sess_path) Path.parent)); |
|
40 |
|
41 val html_ext = Path.ext "html"; |
|
42 val html_path = html_ext o Path.basic; |
|
43 val graph_path = Path.ext "graph" o Path.basic; |
|
44 val index_path = Path.basic "index.html"; |
|
45 |
|
46 val session_path = Path.basic ".session"; |
|
47 val session_entries_path = Path.unpack ".session/entries"; |
|
48 val pre_index_path = Path.unpack ".session/pre-index"; |
|
49 |
|
50 |
|
51 |
|
52 (** additional theory data **) |
|
53 |
|
54 structure BrowserInfoArgs = |
|
55 struct |
|
56 val name = "Pure/browser_info"; |
|
57 type T = {session: string list, is_local: bool}; |
|
58 |
|
59 val empty = {session = [], is_local = false}; |
|
60 val copy = I; |
|
61 val prep_ext = I; |
|
62 fun merge _ = empty; |
|
63 fun print _ _ = (); |
|
64 end; |
|
65 |
|
66 structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs); |
|
67 |
|
68 fun get_info thy = |
|
69 if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty |
|
70 else BrowserInfoData.get thy; |
|
71 |
|
72 |
|
73 |
|
74 (** graphs **) |
|
75 |
|
76 type graph_node = |
|
77 {name: string, ID: string, dir: string, unfold: bool, |
|
78 path: string, parents: string list}; |
|
79 |
|
80 fun get_graph path = map (fn (a :: b :: c :: d :: e :: r) => |
|
81 {name = unenclose a, ID = unenclose b, |
|
82 dir = unenclose c, unfold = (d = "+"), |
|
83 path = unenclose (if d = "+" then e else d), |
|
84 parents = map unenclose (fst (split_last (if d = "+" then tl r else r)))}) |
|
85 (map (filter_out (equal "") o space_explode " ") (split_lines (File.read path))); |
|
86 |
|
87 fun put_graph gr path = File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} => |
|
88 "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
|
89 path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr)); |
|
90 |
|
91 fun dir_of sess = space_implode "/" (case sess of |
|
92 [] => ["Pure"] | [x] => [x, "base"] | xs => xs); |
|
93 |
|
94 fun ID_of sess s = dir_of sess ^ "/" ^ s; |
|
95 |
|
96 (* retrieve graph data from theory loader database *) |
|
97 |
|
98 fun make_graph remote_path unfold curr_sess = map (fn name => |
|
99 let |
|
100 val {session, is_local} = get_info (ThyInfo.theory name); |
|
101 val path' = Path.append (Path.make session) (html_path name) |
|
102 in |
|
103 {name = name, ID = ID_of session name, dir = dir_of session, |
|
104 path = if null session then "" else |
|
105 if is_some remote_path andalso not is_local then |
|
106 Url.pack (Url.append (the remote_path) (Url.file path')) |
|
107 else Path.pack (top_path curr_sess 2 path'), |
|
108 unfold = unfold andalso (length session = 1), |
|
109 parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) |
|
110 (ThyInfo.get_preds name)} |
|
111 end) (ThyInfo.names ()); |
|
112 |
|
113 fun add_graph_entry' (entry as {ID, ...}) (gr : graph_node list) = |
|
114 filter_out (fn entry' => #ID entry' = ID) gr @ [entry]; |
|
115 |
|
116 |
|
117 |
|
118 (** global browser info state **) |
|
119 |
|
120 (* type theory_info *) |
|
121 |
|
122 type theory_info = {source: Buffer.T, html: Buffer.T}; |
|
123 |
|
124 fun make_theory_info (source, html) = |
|
125 {source = source, html = html}: theory_info; |
|
126 |
|
127 val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty); |
|
128 fun map_theory_info f {source, html} = make_theory_info (f (source, html)); |
|
129 |
|
130 |
|
131 (* type browser_info *) |
|
132 |
|
133 type browser_info = {theories: theory_info Symtab.table, index: Buffer.T, |
|
134 graph: graph_node list, all_graph: graph_node list}; |
|
135 |
|
136 fun make_browser_info (theories, index, graph, all_graph) = |
|
137 {theories = theories, index = index, graph = graph, all_graph = all_graph}: browser_info; |
|
138 |
|
139 val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, [], []); |
|
140 |
|
141 fun initial_browser_info remote_path graph_path curr_sess = make_browser_info |
|
142 (Symtab.empty, Buffer.empty, make_graph remote_path false curr_sess, |
|
143 if_none (try get_graph graph_path) (make_graph remote_path true [""])); |
|
144 |
|
145 fun map_browser_info f {theories, index, graph, all_graph} = |
|
146 make_browser_info (f (theories, index, graph, all_graph)); |
|
147 |
|
148 |
|
149 (* state *) |
|
150 |
|
151 val browser_info = ref empty_browser_info; |
|
152 |
|
153 fun change_browser_info f = browser_info := map_browser_info f (! browser_info); |
|
154 |
|
155 fun init_theory_info name info = change_browser_info (fn (theories, index, graph, all_graph) => |
|
156 (Symtab.update ((name, info), theories), index, graph, all_graph)); |
|
157 |
|
158 fun change_theory_info name f = change_browser_info (fn (theories, index, graph, all_graph) => |
|
159 (case Symtab.lookup (theories, name) of |
|
160 None => (warning ("Browser info: cannot access theory document " ^ quote name); |
|
161 (theories, index, graph, all_graph)) |
|
162 | Some info => (Symtab.update ((name, map_theory_info f info), theories), index, graph, all_graph))); |
|
163 |
|
164 |
|
165 fun add_index txt = change_browser_info (fn (theories, index, graph, all_graph) => |
|
166 (theories, Buffer.add txt index, graph, all_graph)); |
|
167 |
|
168 (*add entry to graph for current session*) |
|
169 fun add_graph_entry e = change_browser_info (fn (theories, index, graph, all_graph) => |
|
170 (theories, index, add_graph_entry' e graph, all_graph)); |
|
171 |
|
172 (*add entry to graph for all sessions*) |
|
173 fun add_all_graph_entry e = change_browser_info (fn (theories, index, graph, all_graph) => |
|
174 (theories, index, graph, add_graph_entry' e all_graph)); |
|
175 |
|
176 fun add_source name txt = change_theory_info name (fn (source, html) => |
|
177 (Buffer.add txt source, html)); |
|
178 |
|
179 fun add_html name txt = change_theory_info name (fn (source, html) => |
|
180 (source, Buffer.add txt html)); |
|
181 |
|
182 |
|
183 |
|
184 (** global session state **) |
|
185 |
|
186 (* session_info *) |
|
187 |
|
188 type session_info = |
|
189 {name: string, parent: string, session: string, path: string list, |
|
190 html_prefix: Path.T, graph_path: Path.T, all_graph_path: Path.T, remote_path: Url.T option}; |
|
191 |
|
192 fun make_session_info (name, parent, session, path, html_prefix, graph_path, all_graph_path, remote_path) = |
|
193 {name = name, parent = parent, session = session, path = path, |
|
194 html_prefix = html_prefix, graph_path = graph_path, |
|
195 all_graph_path = all_graph_path, remote_path = remote_path}: session_info; |
|
196 |
|
197 |
|
198 (* state *) |
|
199 |
|
200 val session_info = ref (None: session_info option); |
|
201 |
|
202 fun with_session x f = (case ! session_info of None => x | Some info => f info); |
|
203 fun with_context f = f (PureThy.get_name (Context.the_context ())); |
|
204 |
|
205 |
|
206 |
|
207 (** HTML output **) |
|
208 |
|
209 (* maintain index *) |
|
210 |
|
211 val session_entries = |
|
212 HTML.session_entries o map (fn name => (Url.file (Path.append (Path.basic name) index_path), name)); |
|
213 |
|
214 fun get_entries dir = |
|
215 split_lines (File.read (Path.append dir session_entries_path)); |
|
216 |
|
217 fun put_entries entries dir = |
|
218 File.write (Path.append dir session_entries_path) (cat_lines entries); |
|
219 |
|
220 |
|
221 fun create_index dir = |
|
222 File.read (Path.append dir pre_index_path) ^ |
|
223 session_entries (get_entries dir) ^ HTML.end_index |
|
224 |> File.write (Path.append dir index_path); |
|
225 |
|
226 fun update_index dir name = |
|
227 (case try get_entries dir of |
|
228 None => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir)) |
|
229 | Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir)); |
|
230 |
|
231 |
|
232 (* init session *) |
|
233 |
|
234 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
|
235 |
|
236 fun could_copy inpath outpath = |
|
237 if File.exists inpath then (File.copy inpath outpath; true) |
|
238 else false; |
|
239 |
|
240 fun init false _ _ _ = (browser_info := empty_browser_info; session_info := None) |
|
241 | init true path name (remote_path, first_time) = |
|
242 let |
|
243 val parent_name = name_of_session (take (length path - 1, path)); |
|
244 val session_name = name_of_session path; |
|
245 val sess_prefix = Path.make path; |
|
246 val out_path = Path.expand output_path; |
|
247 val html_prefix = Path.append out_path sess_prefix; |
|
248 val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix]; |
|
249 val graph_path = Path.append graph_prefix (Path.basic "session.graph"); |
|
250 val graph_lnk = Url.file (top_path path 0 (Path.appends |
|
251 [Path.unpack "graph/data", sess_prefix, Path.basic "medium.html"])); |
|
252 val graph_up_lnk = (Url.file (top_path path 2 (Path.append sess_prefix index_path)), session_name); |
|
253 val codebase = Url.file (top_path path 1 Path.current); |
|
254 val all_graph_path = Path.appends [out_path, Path.unpack "graph/data", |
|
255 Path.basic (hd path), Path.basic "all_sessions.graph"]; |
|
256 |
|
257 val _ = (File.mkdir html_prefix; File.mkdir graph_prefix); |
|
258 fun prep_readme readme = |
|
259 let val readme_path = Path.basic readme in |
|
260 if could_copy readme_path (Path.append html_prefix readme_path) then Some readme_path |
|
261 else None |
|
262 end; |
|
263 val opt_readme = |
|
264 (case prep_readme "README.html" of None => prep_readme "README" | some => some); |
|
265 |
|
266 val parent_index_path = Path.append Path.parent index_path; |
|
267 val index_up_lnk = if first_time then |
|
268 Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path)) |
|
269 else Url.file parent_index_path; |
|
270 |
|
271 val index_text = HTML.begin_index (index_up_lnk, parent_name) |
|
272 (Url.file index_path, session_name) (apsome Url.file opt_readme) graph_lnk; |
|
273 in |
|
274 File.mkdir (Path.append html_prefix session_path); |
|
275 File.write (Path.append html_prefix session_entries_path) ""; |
|
276 seq (fn (name, txt) => File.write (Path.append graph_prefix (Path.basic name)) txt) |
|
277 (HTML.applet_pages session_name codebase graph_up_lnk (length path = 1)); |
|
278 session_info := Some (make_session_info (name, parent_name, session_name, path, |
|
279 html_prefix, graph_path, all_graph_path, remote_path)); |
|
280 browser_info := initial_browser_info remote_path all_graph_path path; |
|
281 add_index index_text |
|
282 end; |
|
283 |
|
284 |
|
285 (* finish session *) |
|
286 |
|
287 fun finish () = with_session () (fn {name, html_prefix, graph_path, all_graph_path, path, ...} => |
|
288 let |
|
289 val {theories, index, graph, all_graph} = ! browser_info; |
|
290 |
|
291 fun finish_node (a, {source = _, html}) = |
|
292 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html); |
|
293 in |
|
294 seq finish_node (Symtab.dest theories); |
|
295 Buffer.write (Path.append html_prefix pre_index_path) index; |
|
296 put_graph graph graph_path; |
|
297 put_graph all_graph all_graph_path; |
|
298 create_index html_prefix; |
|
299 update_index (Path.append html_prefix Path.parent) name; |
|
300 browser_info := empty_browser_info; |
|
301 session_info := None |
|
302 end); |
|
303 |
|
304 |
|
305 (* theory elements *) |
|
306 |
|
307 fun theory_source is_old name (src, _) = with_session () (fn _ => |
|
308 (init_theory_info name empty_theory_info; add_source name (HTML.source src))); |
|
309 |
|
310 |
|
311 (* FIXME clean *) |
|
312 |
|
313 fun parent_link remote_path curr_session name = |
|
314 let |
|
315 val {session, is_local} = get_info (ThyInfo.theory name); |
|
316 val path = Path.append (Path.make session) (html_path name) |
|
317 in (if null session then None else |
|
318 Some (if is_some remote_path andalso not is_local then |
|
319 Url.append (the remote_path) (Url.file path) |
|
320 else Url.file (top_path curr_session 0 path)), name) |
|
321 end; |
|
322 |
|
323 fun begin_theory name raw_parents orig_files thy = |
|
324 with_session thy (fn {session, path, html_prefix, remote_path, ...} => |
|
325 let |
|
326 val parents = map (parent_link remote_path path) raw_parents; |
|
327 val ml_path = ThyLoad.ml_path name; |
|
328 val files = map (apsnd Some) orig_files @ |
|
329 (if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []); |
|
330 |
|
331 fun prep_file (raw_path, loadit) = |
|
332 (case ThyLoad.check_file raw_path of |
|
333 Some (path, _) => |
|
334 let |
|
335 val base = Path.base path; |
|
336 val base_html = html_ext base; |
|
337 in |
|
338 File.write (Path.append html_prefix base_html) (HTML.ml_file (Url.file base) (File.read path)); |
|
339 (Some (Url.file base_html), Url.file raw_path, loadit) |
|
340 end |
|
341 | None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path)); |
|
342 (None, Url.file raw_path, loadit))); |
|
343 |
|
344 val files_html = map prep_file files; |
|
345 |
|
346 fun prep_source (source, html) = |
|
347 let val txt = |
|
348 HTML.begin_theory (Url.file index_path, session) name parents files_html (Buffer.content source) |
|
349 in (Buffer.empty, Buffer.add txt html) end; |
|
350 |
|
351 fun make_entry unfold all = |
|
352 {name = name, ID = ID_of path name, dir = dir_of path, unfold = unfold, |
|
353 path = Path.pack (top_path (if all then [""] else path) 2 |
|
354 (Path.append (Path.make path) (html_path name))), |
|
355 parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents}; |
|
356 |
|
357 in |
|
358 change_theory_info name prep_source; |
|
359 add_all_graph_entry (make_entry (length path = 1) true); |
|
360 add_graph_entry (make_entry true false); |
|
361 add_index (HTML.theory_entry (Url.file (html_path name), name)); |
|
362 BrowserInfoData.put {session = path, is_local = is_some remote_path} thy |
|
363 end); |
|
364 |
|
365 fun end_theory _ = (); |
|
366 |
|
367 fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm)); |
|
368 fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms)); |
|
369 fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm)); |
|
370 fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms)); |
|
371 fun section s = with_session () (fn _ => with_context add_html (HTML.section s)); |
|
372 fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s)); |
|
373 fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s)); |
|
374 |
|
375 |
|
376 |
|
377 (** theory setup **) |
|
378 |
|
379 val setup = [BrowserInfoData.init]; |
|
380 |
|
381 |
|
382 end; |
|