src/Pure/Tools/build.scala
changeset 68214 b0e2a19df95b
parent 68213 bb93511c7e8f
child 68216 c0f86aee29db
     1.1 --- a/src/Pure/Tools/build.scala	Fri May 18 21:08:24 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri May 18 21:50:46 2018 +0200
     1.3 @@ -38,32 +38,29 @@
     1.4      {
     1.5        val no_timings: Timings = (Nil, 0.0)
     1.6  
     1.7 -      store.find_database(name) match {
     1.8 +      store.try_open_database(name) match {
     1.9          case None => no_timings
    1.10 -        case Some(database) =>
    1.11 +        case Some(db) =>
    1.12            def ignore_error(msg: String) =
    1.13            {
    1.14 -            progress.echo_warning("Ignoring bad database: " +
    1.15 -              database.expand + (if (msg == "") "" else "\n" + msg))
    1.16 +            progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
    1.17              no_timings
    1.18            }
    1.19            try {
    1.20 -            using(SQLite.open_database(database))(db =>
    1.21 -            {
    1.22 -              val command_timings = store.read_command_timings(db, name)
    1.23 -              val session_timing =
    1.24 -                store.read_session_timing(db, name) match {
    1.25 -                  case Markup.Elapsed(t) => t
    1.26 -                  case _ => 0.0
    1.27 -                }
    1.28 -              (command_timings, session_timing)
    1.29 -            })
    1.30 +            val command_timings = store.read_command_timings(db, name)
    1.31 +            val session_timing =
    1.32 +              store.read_session_timing(db, name) match {
    1.33 +                case Markup.Elapsed(t) => t
    1.34 +                case _ => 0.0
    1.35 +              }
    1.36 +            (command_timings, session_timing)
    1.37            }
    1.38            catch {
    1.39              case ERROR(msg) => ignore_error(msg)
    1.40              case exn: java.lang.Error => ignore_error(Exn.message(exn))
    1.41              case _: XML.Error => ignore_error("")
    1.42            }
    1.43 +          finally { db.close }
    1.44        }
    1.45      }
    1.46  
    1.47 @@ -195,7 +192,7 @@
    1.48      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
    1.49  
    1.50      private val export_tmp_dir = Isabelle_System.tmp_dir("export")
    1.51 -    private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
    1.52 +    private val export_consumer = Export.consumer(store.open_output_database(name))
    1.53  
    1.54      private val future_result: Future[Process_Result] =
    1.55        Future.thread("build") {
    1.56 @@ -422,9 +419,9 @@
    1.57        if (soft_build && !fresh_build) {
    1.58          val outdated =
    1.59            deps0.sessions_structure.build_topological_order.flatMap(name =>
    1.60 -            store.find_database(name) match {
    1.61 -              case Some(database) =>
    1.62 -                using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.63 +            store.try_open_database(name) match {
    1.64 +              case Some(db) =>
    1.65 +                (try { store.read_build(db, name) } finally { db.close }) match {
    1.66                    case Some(build)
    1.67                    if build.ok && build.sources == sources_stamp(deps0, name) => None
    1.68                    case _ => Some(name)
    1.69 @@ -560,7 +557,7 @@
    1.70                      ml_statistics = true,
    1.71                      task_statistics = true)
    1.72  
    1.73 -              using(SQLite.open_database(store.output_database(name)))(db =>
    1.74 +              using(store.open_output_database(name))(db =>
    1.75                  store.write_session_info(db, name,
    1.76                    build_log =
    1.77                      if (process_result.timeout) build_log.error("Timeout") else build_log,
    1.78 @@ -629,8 +626,7 @@
    1.79                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.80  
    1.81                    cleanup(name)
    1.82 -                  using(SQLite.open_database(store.output_database(name)))(db =>
    1.83 -                    store.init_session_info(db, name))
    1.84 +                  using(store.open_output_database(name))(db => store.init_session_info(db, name))
    1.85  
    1.86                    val numa_node = numa_nodes.next(used_node(_))
    1.87                    val job =