src/Pure/Tools/build.scala
changeset 68221 dbef88c2b6c5
parent 68220 8fc4e3d1df86
child 68289 c29fc61fb1b1
     1.1 --- a/src/Pure/Tools/build.scala	Sat May 19 16:13:39 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 20:05:13 2018 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4      {
     1.5        val no_timings: Timings = (Nil, 0.0)
     1.6  
     1.7 -      store.try_open_database(name) match {
     1.8 +      store.access_database(name) match {
     1.9          case None => no_timings
    1.10          case Some(db) =>
    1.11            def ignore_error(msg: String) =
    1.12 @@ -189,7 +189,7 @@
    1.13      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
    1.14  
    1.15      private val export_tmp_dir = Isabelle_System.tmp_dir("export")
    1.16 -    private val export_consumer = Export.consumer(store.open_output_database(name))
    1.17 +    private val export_consumer = Export.consumer(store.open_database(name, output = true))
    1.18  
    1.19      private val future_result: Future[Process_Result] =
    1.20        Future.thread("build") {
    1.21 @@ -425,7 +425,7 @@
    1.22        if (soft_build && !fresh_build) {
    1.23          val outdated =
    1.24            deps0.sessions_structure.build_topological_order.flatMap(name =>
    1.25 -            store.try_open_database(name) match {
    1.26 +            store.access_database(name) match {
    1.27                case Some(db) =>
    1.28                  using(db)(store.read_build(_, name)) match {
    1.29                    case Some(build)
    1.30 @@ -546,7 +546,7 @@
    1.31                      ml_statistics = true,
    1.32                      task_statistics = true)
    1.33  
    1.34 -              using(store.open_output_database(name))(db =>
    1.35 +              using(store.open_database(name, output = true))(db =>
    1.36                  store.write_session_info(db, name,
    1.37                    build_log =
    1.38                      if (process_result.timeout) build_log.error("Timeout") else build_log,
    1.39 @@ -581,7 +581,7 @@
    1.40  
    1.41                  val (current, heap_digest) =
    1.42                  {
    1.43 -                  store.try_open_database(name) match {
    1.44 +                  store.access_database(name) match {
    1.45                      case Some(db) =>
    1.46                        using(db)(store.read_build(_, name)) match {
    1.47                          case Some(build) =>
    1.48 @@ -613,7 +613,7 @@
    1.49                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.50  
    1.51                    store.clean_output(name)
    1.52 -                  using(store.open_output_database(name))(store.init_session_info(_, name))
    1.53 +                  using(store.open_database(name, output = true))(store.init_session_info(_, name))
    1.54  
    1.55                    val numa_node = numa_nodes.next(used_node(_))
    1.56                    val job =