# HG changeset patch # User wenzelm # Date 1637081872 -3600 # Node ID 5eac4b13d1f158a8968f0595cc23a7c5367f031d # Parent c606fddc5b05490f80a994efa6ea24b287852bb0 less ambitious parallelism: more direct read/write saves overall heap space and GC time; diff -r c606fddc5b05 -r 5eac4b13d1f1 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Tue Nov 16 16:39:49 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Tue Nov 16 17:57:52 2021 +0100 @@ -497,11 +497,13 @@ html_context: HTML_Context, session_elements: Elements): Unit = { - val hierarchy = deps.sessions_structure.hierarchy(session) val info = deps.sessions_structure(session) val options = info.options val base = deps(session) + val hierarchy = deps.sessions_structure.hierarchy(session) + val hierarchy_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1)) + val session_dir = Isabelle_System.make_directory(html_context.session_dir(info)) Bytes.write(session_dir + session_graph_path, @@ -539,11 +541,8 @@ map(link => HTML.text("View ") ::: List(link))).flatten } - val all_used_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1)) - val present_theories = html_context.register_presented(all_used_theories) - val theory_exports: Map[String, Export_Theory.Theory] = - (for (node <- all_used_theories.iterator) yield { + (for (node <- hierarchy_theories.iterator) yield { val thy_name = node.theory val theory = if (thy_name == Thy_Header.PURE) Export_Theory.no_theory @@ -564,100 +563,90 @@ def entity_context(name: Document.Node.Name): Entity_Context = Entity_Context.make(session, deps, name, theory_exports) - val theories: List[XML.Body] = + + sealed case class Seen_File( + src_path: Path, thy_name: Document.Node.Name, thy_session: String) { - sealed case class Seen_File( - src_path: Path, thy_name: Document.Node.Name, thy_session: String) - { - val files_path: Path = html_context.files_path(thy_name, src_path) + val files_path: Path = html_context.files_path(thy_name, src_path) - def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean = - { - val files_path1 = html_context.files_path(thy_name1, src_path1) - (src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1 - } + def check(src_path1: Path, thy_name1: Document.Node.Name, thy_session1: String): Boolean = + { + val files_path1 = html_context.files_path(thy_name1, src_path1) + (src_path == src_path1 || files_path == files_path1) && thy_session == thy_session1 } - var seen_files = List.empty[Seen_File] + } + var seen_files = List.empty[Seen_File] - sealed case class Theory( - name: Document.Node.Name, - command: Command, - files_html: List[(Path, XML.Tree)], - html: XML.Tree) + def present_theory(name: Document.Node.Name): Option[XML.Body] = + { + progress.expose_interrupt() - def read_theory(name: Document.Node.Name): Option[Theory] = + Build_Job.read_theory(db_context, hierarchy, name.theory).flatMap(command => { - progress.expose_interrupt() + if (verbose) progress.echo("Presenting theory " + name) + val snapshot = Document.State.init.snippet(command) + + val thy_elements = + session_elements.copy(entity = + theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _)) - for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory)) - yield { - if (verbose) progress.echo("Presenting theory " + name) - val snapshot = Document.State.init.snippet(command) + val files_html = + for { + (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html) + if xml.nonEmpty + } + yield { + progress.expose_interrupt() + if (verbose) progress.echo("Presenting file " + src_path) - val thy_elements = - session_elements.copy(entity = - theory_exports(name.theory).others.keySet.foldLeft(session_elements.entity)(_ + _)) + (src_path, html_context.source( + make_html(entity_context(name), thy_elements, xml))) + } - val files_html = - for { - (src_path, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html) - if xml.nonEmpty - } + val thy_html = + html_context.source( + make_html(entity_context(name), 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.session_dir(thy_session)) + val files = + for { (src_path, file_html) <- files_html } yield { - progress.expose_interrupt() - if (verbose) progress.echo("Presenting file " + src_path) + seen_files.find(_.check(src_path, name, thy_session.name)) match { + case None => seen_files ::= Seen_File(src_path, name, thy_session.name) + case Some(seen_file) => + error("Incoherent use of file name " + src_path + " as " + files_path(src_path) + + " in theory " + seen_file.thy_name + " vs. " + name) + } - (src_path, html_context.source( - make_html(entity_context(name), thy_elements, xml))) + 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))) } - val html = - html_context.source( - make_html(entity_context(name), thy_elements, - snapshot.xml_markup(elements = thy_elements.html))) - - Theory(name, command, files_html, html) - } - } + val thy_title = "Theory " + name.theory_base_name - (for (thy <- Par_List.map(read_theory, present_theories).flatten) yield { - val thy_session = html_context.theory_session(thy.name) - val thy_dir = Isabelle_System.make_directory(html_context.session_dir(thy_session)) - val files = - for { (src_path, file_html) <- thy.files_html } - yield { - seen_files.find(_.check(src_path, thy.name, thy_session.name)) match { - case None => seen_files ::= Seen_File(src_path, thy.name, thy_session.name) - case Some(seen_file) => - error("Incoherent use of file name " + src_path + " as " + files_path(src_path) + - " in theory " + seen_file.thy_name + " vs. " + thy.name) - } - - val file_path = html_context.files_path(thy.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))) - } - - val thy_title = "Theory " + thy.name.theory_base_name - - HTML.write_document(thy_dir, html_name(thy.name), - List(HTML.title(thy_title)), List(html_context.head(thy_title), thy.html), + HTML.write_document(thy_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.name == session) { Some( - List(HTML.link(html_name(thy.name), - HTML.text(thy.name.theory_base_name) ::: + List(HTML.link(html_name(name), + HTML.text(name.theory_base_name) ::: (if (files.isEmpty) Nil else List(HTML.itemize(files)))))) } else None - }).flatten + }) } + val theories = html_context.register_presented(hierarchy_theories).flatMap(present_theory) + val title = "Session " + session HTML.write_document(session_dir, "index.html", List(HTML.title(title + Isabelle_System.isabelle_heading())),