--- a/src/Pure/Tools/build.scala Wed Nov 11 20:58:36 2020 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 11 21:00:14 2020 +0100
@@ -165,12 +165,7 @@
val options: Options = NUMA.policy_options(info.options, numa_node)
private val sessions_structure = deps.sessions_structure
-
- private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
- graphview.Graph_File.write(options, graph_file, deps(session_name).session_graph_display)
-
- private val export_consumer =
- Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
+ private val documents = info.documents.map(_._1)
private val future_result: Future[Process_Result] =
Future.thread("build", uninterruptible = true) {
@@ -180,22 +175,20 @@
YXML.string_of_body(
{
import XML.Encode._
- pair(list(pair(string, int)), pair(list(properties), pair(bool,
- pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
- pair(string, pair(string, pair(string, pair(Path.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(Options.encode, list(pair(string, properties)))),
pair(list(pair(string, properties)),
pair(list(pair(string, string)),
pair(list(string), pair(list(pair(string, string)),
- pair(list(string), list(string)))))))))))))))))(
- (Symbol.codes, (command_timings0, (verbose,
- (store.browser_info, (info.document_files, (File.standard_path(graph_file),
- (parent, (info.chapter, (session_name, (Path.current,
+ pair(list(string), list(string))))))))))))))))(
+ (Symbol.codes, (command_timings0, (verbose, (store.browser_info,
+ (documents, (parent, (info.chapter, (session_name, (Path.current,
(info.theories,
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(base.doc_names, (base.global_theories.toList,
- (base.loaded_theories.keys, info.bibtex_entries.map(_.info))))))))))))))))))
+ (base.loaded_theories.keys, info.bibtex_entries.map(_.info)))))))))))))))))
})
val env =
@@ -234,6 +227,9 @@
}
}
+ val export_consumer =
+ Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache)
+
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
val messages = new mutable.ListBuffer[XML.Elem]
@@ -242,6 +238,7 @@
val session_timings = new mutable.ListBuffer[Properties.T]
val runtime_statistics = new mutable.ListBuffer[Properties.T]
val task_statistics = new mutable.ListBuffer[Properties.T]
+ val document_output = new mutable.ListBuffer[String]
def fun(
name: String,
@@ -355,7 +352,7 @@
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
- val errors =
+ val build_errors =
Isabelle_Thread.interrupt_handler(_ => process.terminate) {
Exn.capture { process.await_startup } match {
case Exn.Res(_) =>
@@ -367,25 +364,58 @@
val process_result =
Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
- val process_output =
- stdout.toString ::
- messages.toList.map(message =>
- Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
- command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
- theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
- session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
- runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
- task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply)
+
+ val export_errors =
+ export_consumer.shutdown(close = true).map(Output.error_message_text)
+
+ 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)
+ }
+ 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 ERROR(msg) => List(msg) case e@Exn.Interrupt() => List(Exn.message(e)) }
val result =
- process_result.output(process_output).error(Library.trim_line(stderr.toString))
+ {
+ val more_output =
+ Library.trim_line(stdout.toString) ::
+ messages.toList.map(message =>
+ Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric))) :::
+ command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
+ theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) :::
+ session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
+ runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
+ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
+ document_output.toList
- errors match {
- case Exn.Res(Nil) => result
- case Exn.Res(errs) =>
- result.error_rc.output(
- errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
- errs.map(Protocol.Error_Message_Marker.apply))
+ val more_errors =
+ Library.trim_line(stderr.toString) :: export_errors ::: document_errors
+
+ process_result.output(more_output).errors(more_errors)
+ }
+
+ build_errors match {
+ case Exn.Res(build_errs) =>
+ val errs = build_errs ::: document_errors
+ if (errs.isEmpty) result
+ else {
+ result.error_rc.output(
+ errs.flatMap(s => split_lines(Output.error_message_text(s))) :::
+ errs.map(Protocol.Error_Message_Marker.apply))
+ }
case Exn.Exn(Exn.Interrupt()) =>
if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result
case Exn.Exn(exn) => throw exn
@@ -404,23 +434,7 @@
def join: (Process_Result, Option[String]) =
{
- val result0 = future_result.join
- val result1 =
- export_consumer.shutdown(close = true).map(Output.error_message_text) match {
- case Nil => result0
- case errs => result0.errors(errs).error_rc
- }
-
- if (result1.ok) {
- for (document_output <- proper_string(options.string("document_output"))) {
- val document_output_dir =
- Isabelle_System.make_directory(info.dir + Path.explode(document_output))
- Present.write_tex_index(document_output_dir, deps(session_name).session_theories)
- }
- Present.finish(progress, store.browser_info, graph_file, info, session_name)
- }
-
- graph_file.delete
+ val result1 = future_result.join
val was_timeout =
timeout_request match {