src/Pure/Thy/sessions.scala
changeset 68205 9a8949f71fd4
parent 68204 a554da2811f2
child 68209 aeffd8f1f079
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu May 17 15:38:36 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu May 17 16:42:13 2018 +0200
     1.3 @@ -1025,6 +1025,9 @@
     1.4      def find_database(name: String): Option[Path] =
     1.5        input_dirs.map(_ + database(name)).find(_.is_file)
     1.6  
     1.7 +    def the_database(name: String): Path =
     1.8 +      find_database(name) getOrElse error("Missing database for session " + quote(name))
     1.9 +
    1.10      def heap(name: String): Path =
    1.11        input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse
    1.12          error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +