src/Pure/Tools/build.scala
changeset 68092 888d35a19866
parent 68088 0763d4eb3ebc
child 68148 fb661e4c4717
     1.1 --- a/src/Pure/Tools/build.scala	Sun May 06 23:01:45 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sun May 06 23:03:08 2018 +0200
     1.3 @@ -195,6 +195,8 @@
     1.4      private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     1.5      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
     1.6  
     1.7 +    private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
     1.8 +
     1.9      private val future_result: Future[Process_Result] =
    1.10        Future.thread("build") {
    1.11          val parent = info.parent.getOrElse("")
    1.12 @@ -286,7 +288,7 @@
    1.13                      text <- Library.try_unprefix("\fexport = ", line)
    1.14                      (args, body) <-
    1.15                        Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text)))
    1.16 -                  } { } // FIXME
    1.17 +                  } { export_consumer(name, args, body) }
    1.18                },
    1.19              progress_limit =
    1.20                options.int("process_output_limit") match {
    1.21 @@ -310,8 +312,14 @@
    1.22      def join: Process_Result =
    1.23      {
    1.24        val result = future_result.join
    1.25 +      val export_result =
    1.26 +        export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
    1.27 +          case Nil => result
    1.28 +          case errs if result.ok => result.copy(rc = 1).errors(errs)
    1.29 +          case errs => result.errors(errs)
    1.30 +        }
    1.31  
    1.32 -      if (result.ok)
    1.33 +      if (export_result.ok)
    1.34          Present.finish(progress, store.browser_info, graph_file, info, name)
    1.35  
    1.36        graph_file.delete
    1.37 @@ -322,11 +330,11 @@
    1.38            case Some(request) => !request.cancel
    1.39          }
    1.40  
    1.41 -      if (result.interrupted) {
    1.42 -        if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
    1.43 -        else result.error(Output.error_message_text("Interrupt"))
    1.44 +      if (export_result.interrupted) {
    1.45 +        if (was_timeout) export_result.error(Output.error_message_text("Timeout")).was_timeout
    1.46 +        else export_result.error(Output.error_message_text("Interrupt"))
    1.47        }
    1.48 -      else result
    1.49 +      else export_result
    1.50      }
    1.51    }
    1.52