--- a/src/Doc/System/Presentation.thy Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Doc/System/Presentation.thy Wed Nov 18 21:53:58 2020 +0100
@@ -132,19 +132,19 @@
-O set option "document_output", relative to current directory
-V verbose latex
-d DIR include session directory
- -n no build of session
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v verbose build
Prepare the theory document of a session.\<close>}
Generated {\LaTeX} sources are taken from the session build database:
- @{tool_ref build} is invoked beforehand to ensure that it is up-to-date, but
- option \<^verbatim>\<open>-n\<close> suppresses that. Further files are generated on the spot,
- notably essential Isabelle style files, and \<^verbatim>\<open>session.tex\<close> to input all
- theory sources from the session (excluding imports from other sessions).
+ @{tool_ref build} is invoked beforehand to ensure that it is up-to-date.
+ Further files are generated on the spot, notably essential Isabelle style
+ files, and \<^verbatim>\<open>session.tex\<close> to input all theory sources from the session
+ (excluding imports from other sessions).
- \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool build}.
+ \<^medskip> Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-v\<close> have the same meaning as for @{tool
+ build}.
\<^medskip> Option \<^verbatim>\<open>-V\<close> prints full output of {\LaTeX} tools.
--- a/src/Doc/System/Sessions.thy Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Doc/System/Sessions.thy Wed Nov 18 21:53:58 2020 +0100
@@ -317,6 +317,7 @@
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
+ -P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
@@ -402,6 +403,11 @@
the command-line are applied in the given order.
\<^medskip>
+ Option \<^verbatim>\<open>-P\<close> enables PDF/HTML presentation in the given directory, where
+ ``\<^verbatim>\<open>-P:\<close>'' refers to the default @{setting_ref ISABELLE_BROWSER_INFO} (or
+ @{setting_ref ISABELLE_BROWSER_INFO_SYSTEM}).
+
+ \<^medskip>
Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
sessions. By default, images are only saved for inner nodes of the hierarchy
of sessions, as required for other sessions to continue later on.
--- a/src/Pure/Admin/build_doc.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/Admin/build_doc.scala Wed Nov 18 21:53:58 2020 +0100
@@ -50,7 +50,7 @@
val errs =
Par_List.map((doc_session: (String, String)) =>
try {
- Present.build_documents(doc_session._2, deps, store, progress = progress)
+ Presentation.build_documents(doc_session._2, deps, store, progress = progress)
None
}
catch {
--- a/src/Pure/General/sha1.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/General/sha1.scala Wed Nov 18 21:53:58 2020 +0100
@@ -66,6 +66,8 @@
def digest(bytes: Bytes): Digest = bytes.sha1_digest
def digest(string: String): Digest = digest(Bytes(string))
+ def digest_set(digests: List[Digest]): Digest =
+ digest(cat_lines(digests.map(_.toString).sorted))
val digest_length: Int = digest("").rep.length
}
--- a/src/Pure/PIDE/resources.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/PIDE/resources.scala Wed Nov 18 21:53:58 2020 +0100
@@ -37,14 +37,14 @@
pair(list(string),
pair(list(pair(string, string)), list(string)))))))))(
(Symbol.codes,
- (resources.sessions_structure.session_positions,
- (resources.sessions_structure.dest_session_directories,
- (resources.sessions_structure.session_chapters,
- (resources.sessions_structure.bibtex_entries,
+ (sessions_structure.session_positions,
+ (sessions_structure.dest_session_directories,
+ (sessions_structure.session_chapters,
+ (sessions_structure.bibtex_entries,
(command_timings,
- (resources.session_base.doc_names,
- (resources.session_base.global_theories.toList,
- resources.session_base.loaded_theories.keys))))))))))
+ (session_base.doc_names,
+ (session_base.global_theories.toList,
+ session_base.loaded_theories.keys))))))))))
}
@@ -56,7 +56,7 @@
def make_theory_content(thy_name: Document.Node.Name): Option[String] =
File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
- def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+ def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
def is_hidden(name: Document.Node.Name): Boolean =
--- a/src/Pure/ROOT.ML Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/ROOT.ML Wed Nov 18 21:53:58 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";
--- a/src/Pure/System/isabelle_tool.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/System/isabelle_tool.scala Wed Nov 18 21:53:58 2020 +0100
@@ -155,7 +155,7 @@
Phabricator.isabelle_tool2,
Phabricator.isabelle_tool3,
Phabricator.isabelle_tool4,
- Present.isabelle_tool,
+ Presentation.isabelle_tool,
Profiling_Report.isabelle_tool,
Server.isabelle_tool,
Sessions.isabelle_tool,
--- a/src/Pure/Thy/bibtex.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/Thy/bibtex.scala Wed Nov 18 21:53:58 2020 +0100
@@ -29,7 +29,7 @@
override def theory_content(name: String): String =
"""theory "bib" imports Pure begin bibtex_file """ + quote(name) + """ end"""
- override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+ override def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] =
{
val name = snapshot.node_name
if (detect(name.node)) {
@@ -39,7 +39,7 @@
File.write(bib, snapshot.node.source)
Bibtex.html_output(List(bib), style = "unsort", title = title)
}
- Some(Present.Preview(title, content))
+ Some(Presentation.Preview(title, content))
}
else None
}
--- a/src/Pure/Thy/file_format.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/Thy/file_format.scala Wed Nov 18 21:53:58 2020 +0100
@@ -88,7 +88,7 @@
} yield s
}
- def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] = None
+ def make_preview(snapshot: Document.Snapshot): Option[Presentation.Preview] = None
/* PIDE session agent */
--- a/src/Pure/Thy/present.ML Wed Nov 18 18:45:50 2020 +0000
+++ /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 ^ "<br/>\n" ^
- (if null Bs then ""
- else
- HTML.keyword symbols "imports" ^ " " ^
- space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "<br/>\n") ^
- "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
- body @ ["</pre>\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;
--- a/src/Pure/Thy/present.scala Wed Nov 18 18:45:50 2020 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,440 +0,0 @@
-/* Title: Pure/Thy/present.scala
- Author: Makarius
-
-Theory presentation: HTML and LaTeX documents.
-*/
-
-package isabelle
-
-
-import scala.collection.immutable.SortedMap
-
-
-object Present
-{
- /* maintain chapter index -- NOT thread-safe */
-
- private val sessions_path = Path.basic(".sessions")
-
- private def read_sessions(dir: Path): List[(String, String)] =
- {
- val path = dir + sessions_path
- if (path.is_file) {
- import XML.Decode._
- list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
- }
- else Nil
- }
-
- private def write_sessions(dir: Path, sessions: List[(String, String)])
- {
- import XML.Encode._
- File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
- }
-
- def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
- {
- val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter))
-
- val sessions0 =
- try { read_sessions(dir) }
- catch { case _: XML.Error => Nil }
-
- val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
- write_sessions(dir, sessions)
-
- val title = "Isabelle/" + chapter + " sessions"
- HTML.write_document(dir, "index.html",
- List(HTML.title(title + " (" + Distribution.version + ")")),
- HTML.chapter(title) ::
- (if (sessions.isEmpty) Nil
- else
- List(HTML.div("sessions",
- List(HTML.description(
- sessions.map({ case (name, description) =>
- val descr = Symbol.trim_blank_lines(description)
- (List(HTML.link(name + "/index.html", HTML.text(name))),
- if (descr == "") Nil
- else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))))
- }
-
- def make_global_index(browser_info: Path)
- {
- if (!(browser_info + Path.explode("index.html")).is_file) {
- Isabelle_System.make_directory(browser_info)
- File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
- browser_info + Path.explode("isabelle.gif"))
- File.write(browser_info + Path.explode("index.html"),
- File.read(Path.explode("~~/lib/html/library_index_header.template")) +
- File.read(Path.explode("~~/lib/html/library_index_content.template")) +
- File.read(Path.explode("~~/lib/html/library_index_footer.template")))
- }
- }
-
-
- /* present session */
-
- val session_graph_path = Path.explode("session_graph.pdf")
- val readme_path = Path.basic("README.html")
-
- def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
- def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name)
-
- def theory_link(name: Document.Node.Name): XML.Tree =
- HTML.link(html_name(name), HTML.text(name.theory_base_name))
-
- def session_html(session: String, deps: Sessions.Deps, store: Sessions.Store): Path =
- {
- val info = deps.sessions_structure(session)
- val options = info.options
- val base = deps(session)
-
- val session_dir = store.browser_info + info.chapter_session
- val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
- for (entry <- Isabelle_Fonts.fonts(hidden = true))
- File.copy(entry.path, session_fonts)
-
- Bytes.write(session_dir + session_graph_path,
- graphview.Graph_File.make_pdf(options, base.session_graph_display))
-
- val links =
- {
- val deps_link =
- HTML.link(session_graph_path, HTML.text("theory dependencies"))
-
- val readme_links =
- if ((info.dir + readme_path).is_file) {
- File.copy(info.dir + readme_path, session_dir + readme_path)
- List(HTML.link(readme_path, HTML.text("README")))
- }
- else Nil
-
- val document_links =
- for ((name, _) <- info.documents)
- yield HTML.link(Path.basic(name).pdf, HTML.text(name))
-
- Library.separate(HTML.break ::: HTML.nl,
- (deps_link :: readme_links ::: document_links).
- map(link => HTML.text("View ") ::: List(link))).flatten
- }
-
- val theories =
- using(Export.open_database_context(deps.sessions_structure, store))(context =>
- for {
- name <- base.session_theories
- entry <- context.try_entry(session, name.theory, document_html_name(name))
- } yield name -> entry.uncompressed(cache = store.xz_cache))
-
- val theories_body =
- HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name)))
-
- val title = "Session " + session
- HTML.write_document(session_dir, "index.html",
- List(HTML.title(title + " (" + Distribution.version + ")")),
- HTML.div("head", List(HTML.chapter(title), HTML.par(links))) ::
- (if (theories.isEmpty) Nil
- else List(HTML.div("theories", List(HTML.section("Theories"), theories_body)))))
-
- for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html)
-
- session_dir
- }
-
-
- /** preview **/
-
- sealed case class Preview(title: String, content: String)
-
- def preview(
- resources: Resources,
- snapshot: Document.Snapshot,
- plain_text: Boolean = false,
- fonts_url: String => String = HTML.fonts_url()): Preview =
- {
- require(!snapshot.is_outdated)
-
- def output_document(title: String, body: XML.Body): String =
- HTML.output_document(
- List(
- HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
- HTML.title(title)),
- List(HTML.source(body)), css = "", structural = false)
-
- val name = snapshot.node_name
-
- if (plain_text) {
- val title = "File " + quote(name.path.file_name)
- val content = output_document(title, HTML.text(snapshot.node.source))
- Preview(title, content)
- }
- else {
- resources.make_preview(snapshot) match {
- case Some(preview) => preview
- case None =>
- val title =
- if (name.is_theory) "Theory " + quote(name.theory_base_name)
- else "File " + quote(name.path.file_name)
- val content = output_document(title, pide_document(snapshot))
- Preview(title, content)
- }
- }
- }
-
-
- /* PIDE document */
-
- private val document_elements =
- Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
- Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
-
- private val div_elements =
- Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
- HTML.descr.name)
-
- private def html_div(html: XML.Body): Boolean =
- html exists {
- case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
- case XML.Text(_) => false
- }
-
- private def html_class(c: String, html: XML.Body): XML.Tree =
- if (html.forall(_ == HTML.no_text)) HTML.no_text
- else if (html_div(html)) HTML.div(c, html)
- else HTML.span(c, html)
-
- private def make_html(xml: XML.Body): XML.Body =
- xml map {
- case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
- html_class(Markup.Language.DOCUMENT, make_html(body))
- case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
- case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
- case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
- case XML.Elem(Markup.Markdown_List(kind), body) =>
- if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
- case XML.Elem(markup, body) =>
- val name = markup.name
- val html =
- markup.properties match {
- case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
- List(html_class(kind, make_html(body)))
- case _ =>
- make_html(body)
- }
- Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
- case Some(c) => html_class(c.toString, html)
- case None => html_class(name, html)
- }
- case XML.Text(text) =>
- XML.Text(Symbol.decode(text))
- }
-
- def pide_document(snapshot: Document.Snapshot): XML.Body =
- make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
-
-
-
- /** build documents **/
-
- val session_tex_path = Path.explode("session.tex")
-
- def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
- def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
-
- def isabelletags(tags: List[String]): String =
- Library.terminate_lines(
- tags.map(tag =>
- tag.toList match {
- case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
- case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
- case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
- case cs => "\\isakeeptag{" + cs.mkString + "}"
- }))
-
- def build_documents(
- session: String,
- deps: Sessions.Deps,
- store: Sessions.Store,
- progress: Progress = new Progress,
- verbose: Boolean = false,
- verbose_latex: Boolean = false): List[(String, Bytes)] =
- {
- /* session info */
-
- val info = deps.sessions_structure(session)
- val options = info.options
- val base = deps(session)
- val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
-
-
- /* prepare document directory */
-
- lazy val tex_files =
- using(Export.open_database_context(deps.sessions_structure, store))(context =>
- for (name <- base.session_theories ::: base.document_theories)
- yield {
- val entry = context.entry(session, name.theory, document_tex_name(name))
- Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
- }
- )
-
- def prepare_dir(dir: Path, doc_name: String, doc_tags: List[String]): (Path, String) =
- {
- val doc_dir = dir + Path.basic(doc_name)
- Isabelle_System.make_directory(doc_dir)
-
- Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
- File.write(doc_dir + Path.explode("isabelletags.sty"), isabelletags(doc_tags))
- for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir)
- Bytes.write(doc_dir + session_graph_path, graph_pdf)
-
- File.write(doc_dir + session_tex_path,
- Library.terminate_lines(
- base.session_theories.map(name => "\\input{" + tex_name(name) + "}")))
-
- for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex)
-
- val root1 = "root_" + doc_name
- val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root"
-
- (doc_dir, root)
- }
-
-
- /* produce documents */
-
- val doc_output = info.document_output
-
- val docs =
- for ((doc_name, doc_tags) <- info.documents)
- yield {
- Isabelle_System.with_tmp_dir("document")(tmp_dir =>
- {
- val (doc_dir, root) = prepare_dir(tmp_dir, doc_name, doc_tags)
- doc_output.foreach(prepare_dir(_, doc_name, doc_tags))
-
-
- // bash scripts
-
- def root_bash(ext: String): String = Bash.string(root + "." + ext)
-
- def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
- "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
-
- def bash(items: String*): Process_Result =
- progress.bash(items.mkString(" && "), cwd = doc_dir.file,
- echo = verbose_latex, watchdog = Time.seconds(0.5))
-
-
- // prepare document
-
- val result =
- if ((doc_dir + Path.explode("build")).is_file) {
- bash("./build pdf " + Bash.string(doc_name))
- }
- else {
- bash(
- latex_bash(),
- "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
- "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
- latex_bash(),
- latex_bash())
- }
-
-
- // result
-
- val root_pdf = Path.basic(root).pdf
- val result_path = doc_dir + root_pdf
-
- if (!result.ok) {
- cat_error(
- Library.trim_line(result.err),
- cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
- "Failed to build document " + quote(doc_name))
- }
- else if (!result_path.is_file) {
- error("Bad document result: expected to find " + root_pdf)
- }
- else doc_name -> Bytes.read(result_path)
- })
- }
-
- def output(dir: Path)
- {
- Isabelle_System.make_directory(dir)
- for ((name, pdf) <- docs) {
- val path = dir + Path.basic(name).pdf
- Bytes.write(path, pdf)
- progress.echo_document(path)
- }
- }
-
- if (info.options.bool("browser_info") || doc_output.isEmpty) {
- output(store.browser_info + info.chapter_session)
- }
-
- doc_output.foreach(output)
-
- docs
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("document", "prepare session theory document", args =>
- {
- var verbose_latex = false
- var dirs: List[Path] = Nil
- var no_build = false
- var options = Options.init()
- var verbose_build = false
-
- val getopts = Getopts(
- """
-Usage: isabelle document [OPTIONS] SESSION
-
- Options are:
- -O set option "document_output", relative to current directory
- -V verbose latex
- -d DIR include session directory
- -n no build of session
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -v verbose build
-
- Prepare the theory document of a session.
-""",
- "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
- "V" -> (_ => verbose_latex = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "n" -> (_ => no_build = true),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose_build = true))
-
- val more_args = getopts(args)
- val session =
- more_args match {
- case List(a) => a
- case _ => getopts.usage()
- }
-
- val progress = new Console_Progress(verbose = verbose_build)
- val store = Sessions.store(options)
-
- progress.interrupt_handler {
- if (!no_build) {
- val res =
- Build.build(options, selection = Sessions.Selection.session(session),
- dirs = dirs, progress = progress, verbose = verbose_build)
- if (!res.ok) error("Failed to build session " + quote(session))
- }
-
- val deps =
- Sessions.load_structure(options + "document=pdf", dirs = dirs).
- selection_deps(Sessions.Selection.session(session))
-
- build_documents(session, deps, store, progress = progress,
- verbose = true, verbose_latex = verbose_latex)
- }
- })
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/presentation.scala Wed Nov 18 21:53:58 2020 +0100
@@ -0,0 +1,578 @@
+/* Title: Pure/Thy/present.scala
+ Author: Makarius
+
+Theory presentation: HTML and LaTeX documents.
+*/
+
+package isabelle
+
+
+import scala.collection.immutable.SortedMap
+
+
+object Presentation
+{
+ /* document variants */
+
+ object Document_Variant
+ {
+ def parse(name: String, tags: String): Document_Variant =
+ Document_Variant(name, Library.space_explode(',', tags))
+
+ def parse(opt: String): Document_Variant =
+ Library.space_explode('=', opt) match {
+ case List(name) => Document_Variant(name, Nil)
+ case List(name, tags) => parse(name, tags)
+ case _ => error("Malformed document variant: " + quote(opt))
+ }
+ }
+
+ sealed case class Document_Variant(name: String, tags: List[String], sources: String = "")
+ {
+ def print_tags: String = tags.mkString(",")
+ def print: String = if (tags.isEmpty) name else name + "=" + print_tags
+
+ def path: Path = Path.basic(name)
+
+ def latex_sty: String =
+ Library.terminate_lines(
+ tags.map(tag =>
+ tag.toList match {
+ case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
+ case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
+ case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
+ case cs => "\\isakeeptag{" + cs.mkString + "}"
+ }))
+
+ def set_sources(s: String): Document_Variant = copy(sources = s)
+ }
+
+
+ /* SQL data model */
+
+ object Data
+ {
+ val session_name = SQL.Column.string("session_name").make_primary_key
+ val name = SQL.Column.string("name").make_primary_key
+ val tags = SQL.Column.string("tags")
+ val sources = SQL.Column.string("sources")
+ val pdf = SQL.Column.bytes("pdf")
+
+ val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, pdf))
+
+ def where_equal(session_name: String, name: String = ""): SQL.Source =
+ "WHERE " + Data.session_name.equal(session_name) +
+ (if (name == "") "" else " AND " + Data.name.equal(name))
+ }
+
+ def read_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] =
+ {
+ val select =
+ Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name))
+ db.using_statement(select)(stmt =>
+ stmt.execute_query().iterator(res =>
+ {
+ val name = res.string(Data.name)
+ val tags = res.string(Data.tags)
+ val sources = res.string(Data.sources)
+ Document_Variant.parse(name, tags).set_sources(sources)
+ }).toList)
+ }
+
+ def read_document(db: SQL.Database, session_name: String, name: String)
+ : Option[(Document_Variant, Bytes)] =
+ {
+ val select = Data.table.select(sql = Data.where_equal(session_name, name))
+ db.using_statement(select)(stmt =>
+ {
+ val res = stmt.execute_query()
+ if (res.next()) {
+ val name = res.string(Data.name)
+ val tags = res.string(Data.tags)
+ val sources = res.string(Data.sources)
+ val pdf = res.bytes(Data.pdf)
+ Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf)
+ }
+ else None
+ })
+ }
+
+ def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes)
+ {
+ db.using_statement(Data.table.insert())(stmt =>
+ {
+ stmt.string(1) = session_name
+ stmt.string(2) = doc.name
+ stmt.string(3) = doc.print_tags
+ stmt.string(4) = doc.sources
+ stmt.bytes(5) = pdf
+ stmt.execute()
+ })
+ }
+
+
+ /* presentation context */
+
+ object Context
+ {
+ val none: Context = new Context { def enabled: Boolean = false }
+ val standard: Context = new Context { def enabled: Boolean = true }
+
+ def dir(path: Path): Context =
+ new Context {
+ def enabled: Boolean = true
+ override def dir(store: Sessions.Store): Path = path
+ }
+
+ def make(s: String): Context =
+ if (s == ":") standard else dir(Path.explode(s))
+ }
+
+ abstract class Context private
+ {
+ def enabled: Boolean
+ def enabled(info: Sessions.Info): Boolean = enabled || info.browser_info
+ def dir(store: Sessions.Store): Path = store.presentation_dir
+ def dir(store: Sessions.Store, info: Sessions.Info): Path =
+ dir(store) + Path.basic(info.chapter) + Path.basic(info.name)
+ }
+
+
+ /* maintain chapter index -- NOT thread-safe */
+
+ private val sessions_path = Path.basic(".sessions")
+
+ private def read_sessions(dir: Path): List[(String, String)] =
+ {
+ val path = dir + sessions_path
+ if (path.is_file) {
+ import XML.Decode._
+ list(pair(string, string))(Symbol.decode_yxml(File.read(path)))
+ }
+ else Nil
+ }
+
+ private def write_sessions(dir: Path, sessions: List[(String, String)])
+ {
+ import XML.Encode._
+ File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
+ }
+
+ def update_chapter_index(browser_info: Path, chapter: String, new_sessions: List[(String, String)])
+ {
+ val dir = Isabelle_System.make_directory(browser_info + Path.basic(chapter))
+
+ val sessions0 =
+ try { read_sessions(dir) }
+ catch { case _: XML.Error => Nil }
+
+ val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
+ write_sessions(dir, sessions)
+
+ val title = "Isabelle/" + chapter + " sessions"
+ HTML.write_document(dir, "index.html",
+ List(HTML.title(title + " (" + Distribution.version + ")")),
+ HTML.chapter(title) ::
+ (if (sessions.isEmpty) Nil
+ else
+ List(HTML.div("sessions",
+ List(HTML.description(
+ sessions.map({ case (name, description) =>
+ val descr = Symbol.trim_blank_lines(description)
+ (List(HTML.link(name + "/index.html", HTML.text(name))),
+ if (descr == "") Nil
+ else HTML.break ::: List(HTML.pre(HTML.text(descr)))) })))))))
+ }
+
+ def make_global_index(browser_info: Path)
+ {
+ if (!(browser_info + Path.explode("index.html")).is_file) {
+ Isabelle_System.make_directory(browser_info)
+ File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+ browser_info + Path.explode("isabelle.gif"))
+ File.write(browser_info + Path.explode("index.html"),
+ File.read(Path.explode("~~/lib/html/library_index_header.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+ File.read(Path.explode("~~/lib/html/library_index_footer.template")))
+ }
+ }
+
+
+ /* present session */
+
+ val session_graph_path = Path.explode("session_graph.pdf")
+ val readme_path = Path.basic("README.html")
+
+ def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
+ def document_html_name(name: Document.Node.Name): String = "document/" + html_name(name)
+
+ def theory_link(name: Document.Node.Name): XML.Tree =
+ HTML.link(html_name(name), HTML.text(name.theory_base_name))
+
+ def session_html(
+ session: String,
+ deps: Sessions.Deps,
+ store: Sessions.Store,
+ presentation: Context): Path =
+ {
+ val info = deps.sessions_structure(session)
+ val options = info.options
+ val base = deps(session)
+
+ val session_dir = presentation.dir(store, info)
+ val session_fonts = Isabelle_System.make_directory(session_dir + Path.explode("fonts"))
+ for (entry <- Isabelle_Fonts.fonts(hidden = true))
+ File.copy(entry.path, session_fonts)
+
+ Bytes.write(session_dir + session_graph_path,
+ graphview.Graph_File.make_pdf(options, base.session_graph_display))
+
+ val links =
+ {
+ val deps_link =
+ HTML.link(session_graph_path, HTML.text("theory dependencies"))
+
+ val readme_links =
+ if ((info.dir + readme_path).is_file) {
+ File.copy(info.dir + readme_path, session_dir + readme_path)
+ List(HTML.link(readme_path, HTML.text("README")))
+ }
+ else Nil
+
+ val document_links =
+ for (doc <- info.documents)
+ yield HTML.link(doc.path.pdf, HTML.text(doc.name))
+
+ Library.separate(HTML.break ::: HTML.nl,
+ (deps_link :: readme_links ::: document_links).
+ map(link => HTML.text("View ") ::: List(link))).flatten
+ }
+
+ val theories =
+ using(Export.open_database_context(deps.sessions_structure, store))(context =>
+ for {
+ name <- base.session_theories
+ entry <- context.try_entry(session, name.theory, document_html_name(name))
+ } yield name -> entry.uncompressed(cache = store.xz_cache))
+
+ val theories_body =
+ HTML.itemize(for ((name, _) <- theories) yield List(theory_link(name)))
+
+ val title = "Session " + session
+ HTML.write_document(session_dir, "index.html",
+ List(HTML.title(title + " (" + Distribution.version + ")")),
+ HTML.div("head", List(HTML.chapter(title), HTML.par(links))) ::
+ (if (theories.isEmpty) Nil
+ else List(HTML.div("theories", List(HTML.section("Theories"), theories_body)))))
+
+ for ((name, html) <- theories) Bytes.write(session_dir + Path.basic(html_name(name)), html)
+
+ session_dir
+ }
+
+
+ /** preview **/
+
+ sealed case class Preview(title: String, content: String)
+
+ def preview(
+ resources: Resources,
+ snapshot: Document.Snapshot,
+ plain_text: Boolean = false,
+ fonts_url: String => String = HTML.fonts_url()): Preview =
+ {
+ require(!snapshot.is_outdated)
+
+ def output_document(title: String, body: XML.Body): String =
+ HTML.output_document(
+ List(
+ HTML.style(HTML.fonts_css(fonts_url) + "\n\n" + File.read(HTML.isabelle_css)),
+ HTML.title(title)),
+ List(HTML.source(body)), css = "", structural = false)
+
+ val name = snapshot.node_name
+
+ if (plain_text) {
+ val title = "File " + quote(name.path.file_name)
+ val content = output_document(title, HTML.text(snapshot.node.source))
+ Preview(title, content)
+ }
+ else {
+ resources.make_preview(snapshot) match {
+ case Some(preview) => preview
+ case None =>
+ val title =
+ if (name.is_theory) "Theory " + quote(name.theory_base_name)
+ else "File " + quote(name.path.file_name)
+ val content = output_document(title, pide_document(snapshot))
+ Preview(title, content)
+ }
+ }
+ }
+
+
+ /* PIDE document */
+
+ private val document_elements =
+ Rendering.foreground_elements ++ Rendering.text_color_elements ++ Rendering.markdown_elements +
+ Markup.NUMERAL + Markup.COMMENT + Markup.LANGUAGE
+
+ private val div_elements =
+ Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
+ HTML.descr.name)
+
+ private def html_div(html: XML.Body): Boolean =
+ html exists {
+ case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
+ case XML.Text(_) => false
+ }
+
+ private def html_class(c: String, html: XML.Body): XML.Tree =
+ if (html.forall(_ == HTML.no_text)) HTML.no_text
+ else if (html_div(html)) HTML.div(c, html)
+ else HTML.span(c, html)
+
+ private def make_html(xml: XML.Body): XML.Body =
+ xml map {
+ case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(Markup.Language.DOCUMENT)), body) =>
+ html_class(Markup.Language.DOCUMENT, make_html(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) => HTML.par(make_html(body))
+ case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) => HTML.item(make_html(body))
+ case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => HTML.no_text
+ case XML.Elem(Markup.Markdown_List(kind), body) =>
+ if (kind == Markup.ENUMERATE) HTML.enum(make_html(body)) else HTML.list(make_html(body))
+ case XML.Elem(markup, body) =>
+ val name = markup.name
+ val html =
+ markup.properties match {
+ case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
+ List(html_class(kind, make_html(body)))
+ case _ =>
+ make_html(body)
+ }
+ Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
+ case Some(c) => html_class(c.toString, html)
+ case None => html_class(name, html)
+ }
+ case XML.Text(text) =>
+ XML.Text(Symbol.decode(text))
+ }
+
+ def pide_document(snapshot: Document.Snapshot): XML.Body =
+ make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
+
+
+
+ /** build documents **/
+
+ val session_tex_path = Path.explode("session.tex")
+
+ def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
+ def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
+
+ def build_documents(
+ session: String,
+ deps: Sessions.Deps,
+ store: Sessions.Store,
+ progress: Progress = new Progress,
+ verbose: Boolean = false,
+ verbose_latex: Boolean = false): List[(Document_Variant, Bytes)] =
+ {
+ /* session info */
+
+ val info = deps.sessions_structure(session)
+ val options = info.options
+ val base = deps(session)
+ val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display)
+
+
+ /* prepare document directory */
+
+ lazy val tex_files =
+ using(Export.open_database_context(deps.sessions_structure, store))(context =>
+ for (name <- base.session_theories ::: base.document_theories)
+ yield {
+ val entry = context.entry(session, name.theory, document_tex_name(name))
+ Path.basic(tex_name(name)) -> entry.uncompressed(cache = store.xz_cache)
+ }
+ )
+
+ def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) =
+ {
+ val doc_dir = dir + Path.basic(doc.name)
+ Isabelle_System.make_directory(doc_dir)
+
+ Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
+ File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty)
+ for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir)
+
+ File.write(doc_dir + session_tex_path,
+ Library.terminate_lines(
+ base.session_theories.map(name => "\\input{" + tex_name(name) + "}")))
+
+ for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex)
+
+ val root1 = "root_" + doc.name
+ val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root"
+
+ (doc_dir, root)
+ }
+
+ def prepare_dir2(dir: Path, doc: Document_Variant): Unit =
+ {
+ val doc_dir = dir + Path.basic(doc.name)
+
+ // non-deterministic, but irrelevant
+ Bytes.write(doc_dir + session_graph_path, graph_pdf)
+ }
+
+
+ /* produce documents */
+
+ val doc_output = info.document_output
+
+ val documents =
+ for (doc <- info.documents)
+ yield {
+ Isabelle_System.with_tmp_dir("document")(tmp_dir =>
+ {
+ // prepare sources
+
+ val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
+ val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
+ val sources = SHA1.digest_set(digests).toString
+ prepare_dir2(tmp_dir, doc)
+
+ doc_output.foreach(prepare_dir1(_, doc))
+ doc_output.foreach(prepare_dir2(_, doc))
+
+
+ // old document from database
+
+ val old_document =
+ using(store.open_database(session))(db =>
+ for {
+ document@(doc, pdf) <- read_document(db, session, doc.name)
+ if doc.sources == sources
+ }
+ yield {
+ Bytes.write(doc_dir + doc.path.pdf, pdf)
+ document
+ })
+
+ old_document getOrElse {
+ // bash scripts
+
+ def root_bash(ext: String): String = Bash.string(root + "." + ext)
+
+ def latex_bash(fmt: String = "pdf", ext: String = "tex"): String =
+ "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext)
+
+ def bash(items: String*): Process_Result =
+ progress.bash(items.mkString(" && "), cwd = doc_dir.file,
+ echo = verbose_latex, watchdog = Time.seconds(0.5))
+
+
+ // prepare document
+
+ val result =
+ if ((doc_dir + Path.explode("build")).is_file) {
+ bash("./build pdf " + Bash.string(doc.name))
+ }
+ else {
+ bash(
+ latex_bash(),
+ "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }",
+ "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }",
+ latex_bash(),
+ latex_bash())
+ }
+
+
+ // result
+
+ val root_pdf = Path.basic(root).pdf
+ val result_path = doc_dir + root_pdf
+
+ if (!result.ok) {
+ cat_error(
+ Library.trim_line(result.err),
+ cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)),
+ "Failed to build document " + quote(doc.name))
+ }
+ else if (!result_path.is_file) {
+ error("Bad document result: expected to find " + root_pdf)
+ }
+ else doc.set_sources(sources) -> Bytes.read(result_path)
+ }
+ })
+ }
+
+ for (dir <- doc_output; (doc, pdf) <- documents) {
+ val path = dir + doc.path.pdf
+ Bytes.write(path, pdf)
+ progress.echo_document(path)
+ }
+
+ documents
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("document", "prepare session theory document", args =>
+ {
+ var verbose_latex = false
+ var dirs: List[Path] = Nil
+ var options = Options.init()
+ var verbose_build = false
+
+ val getopts = Getopts(
+ """
+Usage: isabelle document [OPTIONS] SESSION
+
+ Options are:
+ -O set option "document_output", relative to current directory
+ -V verbose latex
+ -d DIR include session directory
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose build
+
+ Prepare the theory document of a session.
+""",
+ "O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
+ "V" -> (_ => verbose_latex = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose_build = true))
+
+ val more_args = getopts(args)
+ val session =
+ more_args match {
+ case List(a) => a
+ case _ => getopts.usage()
+ }
+
+ val progress = new Console_Progress(verbose = verbose_build)
+ val store = Sessions.store(options)
+
+ progress.interrupt_handler {
+ val res =
+ Build.build(options, selection = Sessions.Selection.session(session),
+ dirs = dirs, progress = progress, verbose = verbose_build)
+ if (!res.ok) error("Failed to build session " + quote(session))
+
+ val deps =
+ Sessions.load_structure(options + "document=pdf", dirs = dirs).
+ selection_deps(Sessions.Selection.session(session))
+
+ if (deps.sessions_structure(session).document_output.isEmpty) {
+ progress.echo_warning("No document_output")
+ }
+
+ build_documents(session, deps, store, progress = progress,
+ verbose = true, verbose_latex = verbose_latex)
+ }
+ })
+}
--- a/src/Pure/Thy/sessions.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Wed Nov 18 21:53:58 2020 +0100
@@ -254,7 +254,11 @@
info.document_theories.flatMap(
{
case (thy, pos) =>
- val parent_sessions = sessions_structure.build_requirements(List(session_name))
+ val parent_sessions =
+ if (sessions_structure.build_graph.defined(session_name)) {
+ sessions_structure.build_requirements(List(session_name))
+ }
+ else Nil
def err(msg: String): Option[String] =
Some(msg + " " + quote(thy) + Position.here(pos))
@@ -459,8 +463,6 @@
export_files: List[(Path, Int, List[String])],
meta_digest: SHA1.Digest)
{
- def chapter_session: Path = Path.basic(chapter) + Path.basic(name)
-
def deps: List[String] = parent.toList ::: imports
def deps_base(session_bases: String => Base): Base =
@@ -490,20 +492,21 @@
case doc => error("Bad document specification " + quote(doc))
}
- def documents: List[(String, List[String])] =
+ def documents_variants: List[Presentation.Document_Variant] =
{
val variants =
- for (s <- Library.space_explode(':', options.string("document_variants")))
- yield {
- Library.space_explode('=', s) match {
- case List(name) => (name, Nil)
- case List(name, tags) => (name, Library.space_explode(',', tags))
- case _ => error("Malformed document_variants: " + quote(s))
- }
- }
- val dups = Library.duplicates(variants.map(_._1))
+ Library.space_explode(':', options.string("document_variants")).
+ map(Presentation.Document_Variant.parse)
+
+ val dups = Library.duplicates(variants.map(_.name))
if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups))
+ variants
+ }
+
+ def documents: List[Presentation.Document_Variant] =
+ {
+ val variants = documents_variants
if (!document_enabled || document_files.isEmpty) Nil else variants
}
@@ -513,6 +516,8 @@
case s => Some(dir + Path.explode(s))
}
+ def browser_info: Boolean = options.bool("browser_info")
+
lazy val bibtex_entries: List[Text.Info[String]] =
(for {
(document_dir, file) <- document_files.iterator
@@ -1193,7 +1198,7 @@
if (system_heaps) List(system_output_dir)
else List(user_output_dir, system_output_dir)
- val browser_info: Path =
+ def presentation_dir: Path =
if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM")
else Path.explode("$ISABELLE_BROWSER_INFO")
@@ -1325,6 +1330,11 @@
db.create_table(Export.Data.table)
db.using_statement(
Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute)
+
+ db.create_table(Presentation.Data.table)
+ db.using_statement(
+ Presentation.Data.table.delete(
+ Presentation.Data.session_name.where_equal(name)))(_.execute)
}
}
--- a/src/Pure/Thy/thy_info.ML Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/Thy/thy_info.ML Wed Nov 18 21:53:58 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 ^ "<br/>\n" ^
+ (if null Bs then ""
+ else
+ HTML.keyword symbols "imports" ^ " " ^
+ space_implode " " (map (uncurry HTML.href_path o apsnd (HTML.name symbols)) Bs) ^ "<br/>\n") ^
+ "\n</div>\n<div class=\"source\">\n<pre class=\"source\">" ::
+ body @ ["</pre>\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];
--- a/src/Pure/Tools/build.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/Tools/build.scala Wed Nov 18 21:53:58 2020 +0100
@@ -158,6 +158,7 @@
deps: Sessions.Deps,
store: Sessions.Store,
do_store: Boolean,
+ presentation: Presentation.Context,
verbose: Boolean,
val numa_node: Option[Int],
command_timings0: List[Properties.T])
@@ -359,19 +360,30 @@
val document_errors =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) {
- if (info.documents.nonEmpty) {
- val document_progress =
- new Progress {
- override def echo(msg: String): Unit =
- document_output.synchronized { document_output += msg }
- override def echo_document(path: Path): Unit =
- progress.echo_document(path)
- }
- Present.build_documents(session_name, deps, store, verbose = verbose,
- verbose_latex = true, progress = document_progress)
- }
- if (info.options.bool("browser_info")) {
- val dir = Present.session_html(session_name, deps, store)
+ val documents =
+ if (info.documents.isEmpty) Nil
+ else {
+ val document_progress =
+ new Progress {
+ override def echo(msg: String): Unit =
+ document_output.synchronized { document_output += msg }
+ override def echo_document(path: Path): Unit =
+ progress.echo_document(path)
+ }
+ val documents =
+ Presentation.build_documents(session_name, deps, store, verbose = verbose,
+ verbose_latex = true, progress = document_progress)
+ using(store.open_database(session_name, output = true))(db =>
+ for ((doc, pdf) <- documents) {
+ db.transaction {
+ Presentation.write_document(db, session_name, doc, pdf)
+ }
+ })
+ documents
+ }
+ if (presentation.enabled(info)) {
+ val dir = Presentation.session_html(session_name, deps, store, presentation)
+ for ((doc, pdf) <- documents) Bytes.write(dir + doc.path.pdf, pdf)
if (verbose) progress.echo("Browser info at " + dir.absolute)
}
}
@@ -481,6 +493,7 @@
def build(
options: Options,
selection: Sessions.Selection = Sessions.Selection.empty,
+ presentation: Presentation.Context = Presentation.Context.none,
progress: Progress = new Progress,
check_unknown_files: Boolean = false,
build_heap: Boolean = false,
@@ -520,7 +533,7 @@
full_sessions(session_name).meta_digest ::
deps.sources(session_name) :::
deps.imported_sources(session_name)
- SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
+ SHA1.digest_set(digests).toString
}
val deps =
@@ -729,8 +742,8 @@
val numa_node = numa_nodes.next(used_node)
val job =
- new Job(progress, session_name, info, deps, store, do_store, verbose,
- numa_node, queue.command_timings(session_name))
+ new Job(progress, session_name, info, deps, store, do_store, presentation,
+ verbose, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
else {
@@ -794,14 +807,16 @@
(name, result) <- results0.iterator
if result.ok
info = full_sessions(name)
- if info.options.bool("browser_info")
+ if presentation.enabled(info)
} yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
+ val dir = presentation.dir(store)
+
for ((chapter, entries) <- browser_chapters)
- Present.update_chapter_index(store.browser_info, chapter, entries)
+ Presentation.update_chapter_index(dir, chapter, entries)
- if (browser_chapters.nonEmpty) Present.make_global_index(store.browser_info)
+ if (browser_chapters.nonEmpty) Presentation.make_global_index(dir)
}
results
@@ -817,6 +832,7 @@
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
+ var presentation = Presentation.Context.none
var requirements = false
var soft_build = false
var exclude_session_groups: List[String] = Nil
@@ -842,6 +858,7 @@
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
+ -P DIR enable HTML/PDF presentation in directory (":" for default)
-R refer to requirements of selected sessions
-S soft build: only observe changes of sources, not heap images
-X NAME exclude sessions from group NAME and all descendants
@@ -866,6 +883,7 @@
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
+ "P:" -> (arg => presentation = Presentation.Context.make(arg)),
"R" -> (_ => requirements = true),
"S" -> (_ => soft_build = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -908,6 +926,7 @@
exclude_sessions = exclude_sessions,
session_groups = session_groups,
sessions = sessions),
+ presentation = presentation,
progress = progress,
check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
build_heap = build_heap,
--- a/src/Pure/build-jars Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Pure/build-jars Wed Nov 18 21:53:58 2020 +0100
@@ -153,7 +153,7 @@
src/Pure/Thy/file_format.scala
src/Pure/Thy/html.scala
src/Pure/Thy/latex.scala
- src/Pure/Thy/present.scala
+ src/Pure/Thy/presentation.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_element.scala
src/Pure/Thy/thy_header.scala
--- a/src/Tools/VSCode/src/preview_panel.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Tools/VSCode/src/preview_panel.scala Wed Nov 18 21:53:58 2020 +0100
@@ -30,7 +30,7 @@
val snapshot = model.snapshot()
if (snapshot.is_outdated) m
else {
- val preview = Present.preview(resources, snapshot)
+ val preview = Presentation.preview(resources, snapshot)
channel.write(
Protocol.Preview_Response(file, column, preview.title, preview.content))
m - file
--- a/src/Tools/jEdit/src/document_model.scala Wed Nov 18 18:45:50 2020 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Wed Nov 18 21:53:58 2020 +0100
@@ -320,7 +320,7 @@
yield {
val snapshot = model.await_stable_snapshot()
val preview =
- Present.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
+ Presentation.preview(PIDE.resources, snapshot, fonts_url = HTML.fonts_dir(fonts_root),
plain_text = query.startsWith(plain_text_prefix))
HTTP.Response.html(preview.content)
})