# HG changeset patch # User wenzelm # Date 1660819681 -7200 # Node ID d50c2129e73af6e59443bc3d780402657a873a24 # Parent 122648e3effb42762877cf2a2b250e7cd15877f1 more robust directory structure: always relative to session_dir; tuned messages; diff -r 122648e3effb -r d50c2129e73a src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Thu Aug 18 12:02:20 2022 +0200 +++ b/src/Pure/Thy/presentation.scala Thu Aug 18 12:48:01 2022 +0200 @@ -38,14 +38,11 @@ def theory_elements(name: Document.Node.Name): Elements = elements.copy(entity = nodes(name.theory).others.foldLeft(elements.entity)(_ + _)) - def session_dir(name: String): Path = - root_dir + Path.explode(sessions_structure(name).chapter_session) + def session_dir(session: String): Path = + root_dir + Path.explode(sessions_structure(session).chapter_session) - def theory_dir(name: Document.Node.Name): Path = - session_dir(theory_session(name)) - - def files_path(name: Document.Node.Name, path: Path): Path = - theory_dir(name) + Path.explode("files") + path.squash.html + def files_path(session: String, path: Path): Path = + session_dir(session) + Path.explode("files") + path.squash.html private def session_relative(session0: String, session1: String): Option[String] = { for { @@ -541,7 +538,10 @@ val options = info.options val base = session_context.session_base - val session_dir = Isabelle_System.make_directory(html_context.session_dir(session)) + val session_dir = + Isabelle_System.make_directory(html_context.session_dir(session)).expand + + progress.echo("Presenting " + session + " in " + session_dir + " ...") Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(options, base.session_graph_display)) @@ -551,8 +551,9 @@ doc <- info.document_variants db <- session_context.session_db() document <- Document_Build.read_document(db, session, doc.name) - } yield { - val doc_path = (session_dir + doc.path.pdf).expand + } + yield { + val doc_path = session_dir + doc.path.pdf if (verbose) progress.echo("Presenting document " + session + "/" + doc.name) if (options.bool("document_echo")) progress.echo("Document at " + doc_path) Bytes.write(doc_path, document.pdf) @@ -581,12 +582,17 @@ def present_theory(name: Document.Node.Name): Option[XML.Body] = { progress.expose_interrupt() - Build_Job.read_theory(session_context.theory(name.theory)).flatMap { command => + Build_Job.read_theory(session_context.theory(name.theory)).map { command => if (verbose) progress.echo("Presenting theory " + name) val snapshot = Document.State.init.snippet(command) val thy_elements = html_context.theory_elements(name) + val thy_html = + html_context.source( + make_html(Entity_Context.make(session, name, html_context), + thy_elements, snapshot.xml_markup(elements = thy_elements.html))) + val files_html = for { (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html) @@ -595,53 +601,42 @@ yield { progress.expose_interrupt() if (verbose) progress.echo("Presenting file " + src_path) - - (src_path, html_context.source( - make_html(Entity_Context.empty, thy_elements, xml))) + (src_path, html_context.source(make_html(Entity_Context.empty, thy_elements, xml))) } - val thy_html = - html_context.source( - make_html(Entity_Context.make(session, name, html_context), - thy_elements, snapshot.xml_markup(elements = thy_elements.html))) - - val thy_session = html_context.theory_session(name) - val thy_dir = Isabelle_System.make_directory(html_context.theory_dir(name)) val files = - for { (src_path, file_html) <- files_html } - yield { - val file_path = html_context.files_path(name, src_path) - val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) - HTML.write_document(file_path.dir, file_path.file_name, - List(HTML.title(file_title)), List(html_context.head(file_title), file_html), - base = Some(html_context.root_dir)) - - List(HTML.link(files_path(src_path), HTML.text(file_title))) - } + for { + (src_path, file_html) <- files_html + file_path = html_context.files_path(session, src_path) + rel_path <- File.relative_path(session_dir, file_path) + } + yield { + val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short) + HTML.write_document(file_path.dir, file_path.file_name, + List(HTML.title(file_title)), List(html_context.head(file_title), file_html), + base = Some(html_context.root_dir)) + List(HTML.link(rel_path.implode, HTML.text(file_title))) + } val thy_title = "Theory " + name.theory_base_name - HTML.write_document(thy_dir, html_name(name), + HTML.write_document(session_dir, html_name(name), List(HTML.title(thy_title)), List(html_context.head(thy_title), thy_html), base = Some(html_context.root_dir)) - if (thy_session == session) { - Some( - List(HTML.link(html_name(name), - HTML.text(name.theory_base_name) ::: - (if (files.isEmpty) Nil else List(HTML.itemize(files)))))) - } - else None + List(HTML.link(html_name(name), + HTML.text(name.theory_base_name) ::: + (if (files.isEmpty) Nil else List(HTML.itemize(files))))) } } val theories = base.proper_session_theories.flatMap(present_theory) val title = "Session " + session - HTML.write_document(session_dir, "index.html", - List(HTML.title(title + Isabelle_System.isabelle_heading())), - html_context.head(title, List(HTML.par(view_links))) :: - html_context.contents("Theories", theories), - base = Some(html_context.root_dir)) + HTML.write_document(session_dir, "index.html", + List(HTML.title(title + Isabelle_System.isabelle_heading())), + html_context.head(title, List(HTML.par(view_links))) :: + html_context.contents("Theories", theories), + base = Some(html_context.root_dir)) } } diff -r 122648e3effb -r d50c2129e73a src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Aug 18 12:02:20 2022 +0200 +++ b/src/Pure/Tools/build.scala Thu Aug 18 12:48:01 2022 +0200 @@ -487,7 +487,6 @@ if (!no_build && !progress.stopped && results.ok) { if (presentation_sessions.nonEmpty) { val presentation_dir = presentation.dir(store) - progress.echo("Presentation in " + presentation_dir.absolute) Presentation.update_root(presentation_dir) for ((chapter, infos) <- presentation_sessions.groupBy(_.chapter).iterator) { @@ -501,7 +500,6 @@ Par_List.map({ (session: String) => progress.expose_interrupt() - progress.echo("Presenting " + session + " ...") val html_context = Presentation.html_context(deps.sessions_structure, Presentation.elements1,