clarified heap vs. database operations: discontinued correlation of directory;
authorwenzelm
Fri May 18 21:05:10 2018 +0200 (14 months ago)
changeset 682125a59fded83c7
parent 68211 1e7defef8c8a
child 68213 bb93511c7e8f
clarified heap vs. database operations: discontinued correlation of directory;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 18 21:00:15 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 18 21:05:10 2018 +0200
     1.3 @@ -1019,21 +1019,26 @@
     1.4          output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
     1.5        }
     1.6  
     1.7 -    def find_database_heap(name: String): Option[(Path, Option[String])] =
     1.8 -      input_dirs.find(dir => (dir + database(name)).is_file).map(dir =>
     1.9 -        (dir + database(name), read_heap_digest(dir + Path.basic(name))))
    1.10 +    def find_heap(name: String): Option[Path] =
    1.11 +      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    1.12 +
    1.13 +    def find_heap_digest(name: String): Option[String] =
    1.14 +      find_heap(name).flatMap(read_heap_digest(_))
    1.15  
    1.16      def find_database(name: String): Option[Path] =
    1.17        input_dirs.map(_ + database(name)).find(_.is_file)
    1.18  
    1.19 -    def open_database(name: String): SQL.Database =
    1.20 -      SQLite.open_database(
    1.21 -        find_database(name) getOrElse error("Missing database for session " + quote(name)))
    1.22 +    def try_open_database(name: String): Option[SQL.Database] =
    1.23 +      find_database(name).map(SQLite.open_database(_))
    1.24 +
    1.25 +    private def error_input(msg: String): Nothing =
    1.26 +      error(msg + " -- expected in:\n" + cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
    1.27  
    1.28      def heap(name: String): Path =
    1.29 -      input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
    1.30 -        error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
    1.31 -          cat_lines(input_dirs.map(dir => "  " + dir.expand.implode)))
    1.32 +      find_heap(name) getOrElse error_input("Missing heap image for session " + quote(name))
    1.33 +
    1.34 +    def open_database(name: String): SQL.Database =
    1.35 +      try_open_database(name) getOrElse error("Missing database file for session " + quote(name))
    1.36  
    1.37  
    1.38      /* session info */
     2.1 --- a/src/Pure/Tools/build.scala	Fri May 18 21:00:15 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Fri May 18 21:05:10 2018 +0200
     2.3 @@ -595,20 +595,23 @@
     2.4  
     2.5                  val (current, heap_stamp) =
     2.6                  {
     2.7 -                  store.find_database_heap(name) match {
     2.8 -                    case Some((database, heap_stamp)) =>
     2.9 -                      using(SQLite.open_database(database))(store.read_build(_, name)) match {
    2.10 -                        case Some(build) =>
    2.11 -                          val current =
    2.12 -                            !fresh_build &&
    2.13 -                            build.ok &&
    2.14 -                            build.sources == sources_stamp(deps, name) &&
    2.15 -                            build.input_heaps == ancestor_heaps &&
    2.16 -                            build.output_heap == heap_stamp &&
    2.17 -                            !(do_output && heap_stamp.isEmpty)
    2.18 -                          (current, heap_stamp)
    2.19 -                        case None => (false, None)
    2.20 -                      }
    2.21 +                  store.try_open_database(name) match {
    2.22 +                    case Some(db) =>
    2.23 +                      try {
    2.24 +                        store.read_build(db, name) match {
    2.25 +                          case Some(build) =>
    2.26 +                            val heap_stamp = store.find_heap_digest(name)
    2.27 +                            val current =
    2.28 +                              !fresh_build &&
    2.29 +                              build.ok &&
    2.30 +                              build.sources == sources_stamp(deps, name) &&
    2.31 +                              build.input_heaps == ancestor_heaps &&
    2.32 +                              build.output_heap == heap_stamp &&
    2.33 +                              !(do_output && heap_stamp.isEmpty)
    2.34 +                            (current, heap_stamp)
    2.35 +                          case None => (false, None)
    2.36 +                        }
    2.37 +                      } finally { db.close }
    2.38                      case None => (false, None)
    2.39                    }
    2.40                  }