# HG changeset patch # User wenzelm # Date 1605710873 -3600 # Node ID 52cb065aa9168db01fdfa68201df413b9b693341 # Parent 787ba1d19d3a57c90e46e8a133ac99a59335e1fe clarified modules; diff -r 787ba1d19d3a -r 52cb065aa916 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Nov 18 15:41:02 2020 +0100 +++ b/src/Pure/ROOT.ML Wed Nov 18 15:47:53 2020 +0100 @@ -309,7 +309,6 @@ ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; -ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; diff -r 787ba1d19d3a -r 52cb065aa916 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Wed Nov 18 15:41:02 2020 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,76 +0,0 @@ -(* Title: Pure/Thy/present.ML - Author: Makarius - -Theory presentation: HTML and LaTeX documents. -*) - -signature PRESENT = -sig - val document_html_name: theory -> Path.binding - val document_tex_name: theory -> Path.binding - val html_name: theory -> Path.T - val export_html: theory -> Command_Span.span list -> unit -end; - -structure Present: PRESENT = -struct - -(** 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
\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; - -end; 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
\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];