diff -r 65554bac121b -r 830222403681 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Nov 16 22:21:40 2020 +0100 +++ b/src/Pure/Tools/build.scala Mon Nov 16 22:23:04 2020 +0100 @@ -165,7 +165,6 @@ val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure - private val documents = info.documents.map(_._1) private val future_result: Future[Process_Result] = Future.thread("build", uninterruptible = true) { @@ -175,23 +174,22 @@ YXML.string_of_body( { import XML.Encode._ - pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Path.encode, - pair(list(string), pair(string, pair(string, pair(string, pair(Path.encode, + pair(list(pair(string, int)), pair(list(properties), pair(string, pair(string, + pair(string, pair(Path.encode, pair(list(pair(Options.encode, list(pair(string, properties)))), pair(list(pair(string, properties)), pair(list(pair(string, string)), pair(list(pair(string, string)), pair(list(string), pair(list(pair(string, string)), - pair(list(string), list(pair(string, list(string)))))))))))))))))))( - (Symbol.codes, (command_timings0, (verbose, (store.browser_info, - (documents, (parent, (info.chapter, (session_name, (Path.current, - (info.theories, + pair(list(string), list(pair(string, list(string))))))))))))))))( + (Symbol.codes, (command_timings0, (parent, (info.chapter, + (session_name, (Path.current, (info.theories, (sessions_structure.session_positions, (sessions_structure.dest_session_directories, (sessions_structure.session_chapters, (base.doc_names, (base.global_theories.toList, - (base.loaded_theories.keys, sessions_structure.bibtex_entries))))))))))))))))) + (base.loaded_theories.keys, sessions_structure.bibtex_entries)))))))))))))) }) val env = @@ -373,20 +371,23 @@ val document_errors = try { - if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && 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 (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) + if (verbose) progress.echo("Browser info at " + dir.absolute) + } } - val graph_pdf = - graphview.Graph_File.make_pdf(options, deps(session_name).session_graph_display) - Present.finish(store.browser_info, graph_pdf, info, session_name) Nil } catch { case Exn.Interrupt.ERROR(msg) => List(msg) }