author | wenzelm |
Tue, 17 Nov 2020 16:54:49 +0100 | |
changeset 72636 | 09ee9eb7a3d3 |
parent 72635 | 2a329baa7d39 |
permissions | -rw-r--r-- |
6203 | 1 |
(* Title: Pure/Thy/present.ML |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
2 |
Author: Makarius |
6203 | 3 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
4 |
Theory presentation: HTML and LaTeX documents. |
6203 | 5 |
*) |
6 |
||
7 |
signature PRESENT = |
|
8 |
sig |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
9 |
val document_html_name: theory -> Path.binding |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
10 |
val document_tex_name: theory -> Path.binding |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
11 |
val html_name: theory -> Path.T |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
12 |
val export_html: theory -> Command_Span.span list -> unit |
6203 | 13 |
end; |
14 |
||
7685 | 15 |
structure Present: PRESENT = |
16 |
struct |
|
17 |
||
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
18 |
(** artefact names **) |
7727 | 19 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
20 |
fun document_name ext thy = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
21 |
Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext); |
7727 | 22 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
23 |
val document_html_name = document_name "html"; |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
24 |
val document_tex_name = document_name "tex"; |
7727 | 25 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
26 |
fun html_name thy = Path.basic (Context.theory_name thy ^ ".html"); |
7685 | 27 |
|
28 |
||
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
29 |
(* theory as HTML *) |
7727 | 30 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
31 |
local |
11856 | 32 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
33 |
fun get_session_chapter thy = |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
34 |
let |
72616 | 35 |
val session = Resources.theory_qualifier (Context.theory_long_name thy); |
36 |
val chapter = Resources.session_chapter session; |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
37 |
in (session, chapter) end; |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
38 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
39 |
fun theory_link thy thy' = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
40 |
let |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
41 |
val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy'); |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
42 |
val link = html_name thy'; |
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
43 |
in |
72636 | 44 |
if session = session' then link |
45 |
else if chapter = chapter' then Path.parent + Path.basic session' + link |
|
46 |
else Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link |
|
59448
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
47 |
end; |
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset
|
48 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
49 |
fun theory_document symbols A Bs body = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
50 |
HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^ |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
51 |
HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^ |
72636 | 52 |
(if null Bs then "" |
53 |
else |
|
54 |
HTML.keyword symbols "imports" ^ " " ^ |
|
55 |
space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "<br/>\n") ^ |
|
56 |
"\n</div>\n<div class=\"source\">\n<pre class=\"source\">" :: |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
57 |
body @ ["</pre>\n", HTML.end_document]; |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
58 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
59 |
in |
54456 | 60 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
61 |
fun export_html thy spans = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
62 |
let |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
63 |
val name = Context.theory_name thy; |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
64 |
val parents = |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
65 |
Theory.parents_of thy |> map (fn thy' => |
72636 | 66 |
(Url.File (theory_link thy thy'), Context.theory_name thy')); |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72511
diff
changeset
|
67 |
|
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
68 |
val symbols = Resources.html_symbols (); |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
69 |
val keywords = Thy_Header.get_keywords thy; |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
70 |
val body = map (HTML.present_span symbols keywords) spans; |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
71 |
val html = XML.blob (theory_document symbols name parents body); |
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
72 |
in Export.export thy (document_html_name thy) html end |
7727 | 73 |
|
7685 | 74 |
end; |
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
75 |
|
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset
|
76 |
end; |