src/Pure/Tools/build.scala
changeset 68217 3e90b88b0fc2
parent 68216 c0f86aee29db
child 68219 c0341c0080e2
     1.1 --- a/src/Pure/Tools/build.scala	Sat May 19 14:12:44 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 14:47:54 2018 +0200
     1.3 @@ -179,9 +179,6 @@
     1.4      val numa_node: Option[Int],
     1.5      command_timings: List[Properties.T])
     1.6    {
     1.7 -    val output = store.output_dir + Path.basic(name)
     1.8 -    def output_path: Option[Path] = if (do_output) Some(output) else None
     1.9 -
    1.10      val options =
    1.11        numa_node match {
    1.12          case None => info.options
    1.13 @@ -224,7 +221,8 @@
    1.14  
    1.15          def save_heap: String =
    1.16            (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
    1.17 -            "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(output))
    1.18 +            "ML_Heap.save_child " +
    1.19 +            ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
    1.20  
    1.21          if (pide && !Sessions.is_pure(name)) {
    1.22            val resources = new Resources(deps(parent))
    1.23 @@ -311,19 +309,19 @@
    1.24        else None
    1.25      }
    1.26  
    1.27 -    def join: Process_Result =
    1.28 +    def join: (Process_Result, Option[String]) =
    1.29      {
    1.30 -      val result = future_result.join
    1.31 -      val export_result =
    1.32 +      val result0 = future_result.join
    1.33 +      val result1 =
    1.34          export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
    1.35 -          case Nil => result
    1.36 -          case errs if result.ok => result.copy(rc = 1).errors(errs)
    1.37 -          case errs => result.errors(errs)
    1.38 +          case Nil => result0
    1.39 +          case errs if result0.ok => result0.copy(rc = 1).errors(errs)
    1.40 +          case errs => result0.errors(errs)
    1.41          }
    1.42  
    1.43        Isabelle_System.rm_tree(export_tmp_dir)
    1.44  
    1.45 -      if (export_result.ok)
    1.46 +      if (result1.ok)
    1.47          Present.finish(progress, store.browser_info, graph_file, info, name)
    1.48  
    1.49        graph_file.delete
    1.50 @@ -334,11 +332,19 @@
    1.51            case Some(request) => !request.cancel
    1.52          }
    1.53  
    1.54 -      if (export_result.interrupted) {
    1.55 -        if (was_timeout) export_result.error(Output.error_message_text("Timeout")).was_timeout
    1.56 -        else export_result.error(Output.error_message_text("Interrupt"))
    1.57 -      }
    1.58 -      else export_result
    1.59 +      val result2 =
    1.60 +        if (result1.interrupted) {
    1.61 +          if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
    1.62 +          else result1.error(Output.error_message_text("Interrupt"))
    1.63 +        }
    1.64 +        else result1
    1.65 +
    1.66 +      val heap_digest =
    1.67 +        if (result2.ok && do_output && store.output_heap(name).is_file)
    1.68 +          Some(Sessions.write_heap_digest(store.output_heap(name)))
    1.69 +        else None
    1.70 +
    1.71 +      (result2, heap_digest)
    1.72      }
    1.73    }
    1.74  
    1.75 @@ -517,7 +523,7 @@
    1.76            case Some((name, (input_heaps, job))) =>
    1.77              //{{{ finish job
    1.78  
    1.79 -            val process_result = job.join
    1.80 +            val (process_result, heap_digest) = job.join
    1.81  
    1.82              val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
    1.83              val process_result_tail =
    1.84 @@ -531,21 +537,10 @@
    1.85  
    1.86  
    1.87              // write log file
    1.88 -            val heap_digest =
    1.89 -              if (process_result.ok) {
    1.90 -                val heap_digest =
    1.91 -                  for (path <- job.output_path if path.is_file)
    1.92 -                    yield Sessions.write_heap_digest(path)
    1.93 -
    1.94 -                File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
    1.95 -
    1.96 -                heap_digest
    1.97 -              }
    1.98 -              else {
    1.99 -                File.write(store.output_log(name), terminate_lines(log_lines))
   1.100 -
   1.101 -                None
   1.102 -              }
   1.103 +            if (process_result.ok) {
   1.104 +              File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   1.105 +            }
   1.106 +            else File.write(store.output_log(name), terminate_lines(log_lines))
   1.107  
   1.108              // write database
   1.109              {