more abstract database access;
authorwenzelm
Fri May 18 21:50:46 2018 +0200 (14 months ago)
changeset 68214b0e2a19df95b
parent 68213 bb93511c7e8f
child 68215 a477f78a9365
more abstract database access;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 18 21:08:24 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 18 21:50:46 2018 +0200
     1.3 @@ -1005,10 +1005,12 @@
     1.4  
     1.5      def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
     1.6  
     1.7 -    def output_database(name: String): Path = output_dir + database(name)
     1.8      def output_log(name: String): Path = output_dir + log(name)
     1.9      def output_log_gz(name: String): Path = output_dir + log_gz(name)
    1.10  
    1.11 +    def open_output_database(name: String): SQL.Database =
    1.12 +      SQLite.open_database(output_dir + database(name))
    1.13 +
    1.14  
    1.15      /* input */
    1.16  
     2.1 --- a/src/Pure/Tools/build.scala	Fri May 18 21:08:24 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Fri May 18 21:50:46 2018 +0200
     2.3 @@ -38,32 +38,29 @@
     2.4      {
     2.5        val no_timings: Timings = (Nil, 0.0)
     2.6  
     2.7 -      store.find_database(name) match {
     2.8 +      store.try_open_database(name) match {
     2.9          case None => no_timings
    2.10 -        case Some(database) =>
    2.11 +        case Some(db) =>
    2.12            def ignore_error(msg: String) =
    2.13            {
    2.14 -            progress.echo_warning("Ignoring bad database: " +
    2.15 -              database.expand + (if (msg == "") "" else "\n" + msg))
    2.16 +            progress.echo_warning("Ignoring bad database " + db + (if (msg == "") "" else "\n" + msg))
    2.17              no_timings
    2.18            }
    2.19            try {
    2.20 -            using(SQLite.open_database(database))(db =>
    2.21 -            {
    2.22 -              val command_timings = store.read_command_timings(db, name)
    2.23 -              val session_timing =
    2.24 -                store.read_session_timing(db, name) match {
    2.25 -                  case Markup.Elapsed(t) => t
    2.26 -                  case _ => 0.0
    2.27 -                }
    2.28 -              (command_timings, session_timing)
    2.29 -            })
    2.30 +            val command_timings = store.read_command_timings(db, name)
    2.31 +            val session_timing =
    2.32 +              store.read_session_timing(db, name) match {
    2.33 +                case Markup.Elapsed(t) => t
    2.34 +                case _ => 0.0
    2.35 +              }
    2.36 +            (command_timings, session_timing)
    2.37            }
    2.38            catch {
    2.39              case ERROR(msg) => ignore_error(msg)
    2.40              case exn: java.lang.Error => ignore_error(Exn.message(exn))
    2.41              case _: XML.Error => ignore_error("")
    2.42            }
    2.43 +          finally { db.close }
    2.44        }
    2.45      }
    2.46  
    2.47 @@ -195,7 +192,7 @@
    2.48      isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
    2.49  
    2.50      private val export_tmp_dir = Isabelle_System.tmp_dir("export")
    2.51 -    private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
    2.52 +    private val export_consumer = Export.consumer(store.open_output_database(name))
    2.53  
    2.54      private val future_result: Future[Process_Result] =
    2.55        Future.thread("build") {
    2.56 @@ -422,9 +419,9 @@
    2.57        if (soft_build && !fresh_build) {
    2.58          val outdated =
    2.59            deps0.sessions_structure.build_topological_order.flatMap(name =>
    2.60 -            store.find_database(name) match {
    2.61 -              case Some(database) =>
    2.62 -                using(SQLite.open_database(database))(store.read_build(_, name)) match {
    2.63 +            store.try_open_database(name) match {
    2.64 +              case Some(db) =>
    2.65 +                (try { store.read_build(db, name) } finally { db.close }) match {
    2.66                    case Some(build)
    2.67                    if build.ok && build.sources == sources_stamp(deps0, name) => None
    2.68                    case _ => Some(name)
    2.69 @@ -560,7 +557,7 @@
    2.70                      ml_statistics = true,
    2.71                      task_statistics = true)
    2.72  
    2.73 -              using(SQLite.open_database(store.output_database(name)))(db =>
    2.74 +              using(store.open_output_database(name))(db =>
    2.75                  store.write_session_info(db, name,
    2.76                    build_log =
    2.77                      if (process_result.timeout) build_log.error("Timeout") else build_log,
    2.78 @@ -629,8 +626,7 @@
    2.79                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    2.80  
    2.81                    cleanup(name)
    2.82 -                  using(SQLite.open_database(store.output_database(name)))(db =>
    2.83 -                    store.init_session_info(db, name))
    2.84 +                  using(store.open_output_database(name))(db => store.init_session_info(db, name))
    2.85  
    2.86                    val numa_node = numa_nodes.next(used_node(_))
    2.87                    val job =