author  wenzelm 
Tue, 17 Nov 2020 16:48:18 +0100  
changeset 72635  2a329baa7d39 
parent 72622  830222403681 
child 72636  09ee9eb7a3d3 
permissions  rwrr 
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 
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

44 
if session = session' then SOME link 
72635  45 
else if chapter = chapter' then SOME (Path.parent + Path.basic session' + link) 
46 
else if chapter' = Context.PureN then NONE 

47 
else SOME (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

48 
end; 
149d2bc5ddb6
prefer plain session_graph.pdf over GraphBrowser applet;
wenzelm
parents:
59446
diff
changeset

49 

72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

50 
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

51 
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

52 
HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "<br/>\n" ^ 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

53 
HTML.keyword symbols "imports" ^ " " ^ 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

54 
space_implode " " (map (uncurry HTML.href_opt_path o apsnd (HTML.name symbols)) Bs) ^ 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

55 
"<br/>\n\n</div>\n<div class=\"source\">\n<pre class=\"source\">" :: 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

56 
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

57 

830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

58 
in 
54456  59 

72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

60 
fun export_html thy spans = 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

61 
let 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

62 
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

63 
val parents = 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

64 
Theory.parents_of thy > map (fn thy' => 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

65 
(Option.map 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

66 

72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

67 
val symbols = Resources.html_symbols (); 
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

68 
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

69 
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

70 
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

71 
in Export.export thy (document_html_name thy) html end 
7727  72 

7685  73 
end; 
72622
830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

74 

830222403681
HTML presentation in Isabelle/Scala, based on theory html exports from Isabelle/ML;
wenzelm
parents:
72620
diff
changeset

75 
end; 