diff -r 787ba1d19d3a -r 52cb065aa916 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML Wed Nov 18 15:41:02 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Nov 18 15:47:53 2020 +0100
@@ -1,8 +1,8 @@
(* Title: Pure/Thy/thy_info.ML
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
Global theory info database, with auto-loading according to theory and
-file dependencies.
+file dependencies, and presentation of theory documents.
*)
signature THY_INFO =
@@ -28,7 +28,68 @@
structure Thy_Info: THY_INFO =
struct
-(** presentation of consolidated theory **)
+(** theory presentation **)
+
+(* artefact names *)
+
+fun document_name ext thy =
+ Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
+
+val document_html_name = document_name "html";
+val document_tex_name = document_name "tex";
+
+fun html_name thy = Path.basic (Context.theory_name thy ^ ".html");
+
+
+(* theory as HTML *)
+
+local
+
+fun get_session_chapter thy =
+ let
+ val session = Resources.theory_qualifier (Context.theory_long_name thy);
+ val chapter = Resources.session_chapter session;
+ in (session, chapter) end;
+
+fun theory_link thy thy' =
+ let
+ val ((session, chapter), (session', chapter')) = apply2 get_session_chapter (thy, thy');
+ val link = html_name thy';
+ in
+ if session = session' then link
+ else if chapter = chapter' then Path.parent + Path.basic session' + link
+ else Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link
+ end;
+
+fun theory_document symbols A Bs body =
+ HTML.begin_document symbols ("Theory " ^ A) ^ "\n" ^
+ HTML.command symbols "theory" ^ " " ^ HTML.name symbols A ^ "
\n" ^
+ (if null Bs then ""
+ else
+ HTML.keyword symbols "imports" ^ " " ^
+ space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "
\n") ^
+ "\n\n
" :: + body @ ["\n", HTML.end_document]; + +in + +fun export_html thy spans = + let + val name = Context.theory_name thy; + val parents = + Theory.parents_of thy |> map (fn thy' => + (Url.File (theory_link thy thy'), Context.theory_name thy')); + + val symbols = Resources.html_symbols (); + val keywords = Thy_Header.get_keywords thy; + val body = map (HTML.present_span symbols keywords) spans; + val html = XML.blob (theory_document symbols name parents body); + in Export.export thy (document_html_name thy) html end + +end; + + +(* hook for consolidated theory *) type presentation_context = {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T, @@ -52,7 +113,7 @@ val _ = Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy => - (Present.export_html thy (map #span segments); + (export_html thy (map #span segments); if exists (Toplevel.is_skipped_proof o #state) segments then () else let @@ -62,7 +123,7 @@ else let val thy_name = Context.theory_name thy; - val document_tex_name = Present.document_tex_name thy; + val document_tex_name = document_tex_name thy; val latex = Latex.isabelle_body thy_name body; val output = [Latex.output_text latex, Latex.output_positions file_pos latex];