src/Pure/Thy/sessions.scala
changeset 62637 0189fe0f6452
parent 62636 e676ae9f1bf6
child 62704 478b49f0d726
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Mar 16 14:24:51 2016 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Mar 16 15:08:22 2016 +0100
     1.3 @@ -318,7 +318,8 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* persistent store */
     1.8 +
     1.9 +  /** persistent store **/
    1.10  
    1.11    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    1.12    def log_gz(name: String): Path = log(name).ext("gz")
    1.13 @@ -327,15 +328,22 @@
    1.14  
    1.15    class Store private [Sessions](system_mode: Boolean)
    1.16    {
    1.17 -    val output_dir: Path =
    1.18 -      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
    1.19 -      else Path.explode("$ISABELLE_OUTPUT")
    1.20 +    /* output */
    1.21  
    1.22      val browser_info: Path =
    1.23        if (system_mode) Path.explode("~~/browser_info")
    1.24        else Path.explode("$ISABELLE_BROWSER_INFO")
    1.25  
    1.26 -    val input_dirs =
    1.27 +    val output_dir: Path =
    1.28 +      if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
    1.29 +      else Path.explode("$ISABELLE_OUTPUT")
    1.30 +
    1.31 +    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    1.32 +
    1.33 +
    1.34 +    /* input */
    1.35 +
    1.36 +    private val input_dirs =
    1.37        if (system_mode) List(output_dir)
    1.38        else {
    1.39          val ml_ident = Path.explode("$ML_IDENTIFIER").expand
    1.40 @@ -346,15 +354,18 @@
    1.41        input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
    1.42          (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
    1.43  
    1.44 -    def find_heap(name: String): Option[Path] =
    1.45 -      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    1.46 -
    1.47      def find_log(name: String): Option[Path] =
    1.48        input_dirs.map(_ + log(name)).find(_.is_file)
    1.49  
    1.50      def find_log_gz(name: String): Option[Path] =
    1.51        input_dirs.map(_ + log_gz(name)).find(_.is_file)
    1.52  
    1.53 -    def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
    1.54 +    def find_heap(name: String): Option[Path] =
    1.55 +      input_dirs.map(_ + Path.basic(name)).find(_.is_file)
    1.56 +
    1.57 +    def heap(name: String): Path =
    1.58 +      find_heap(name) getOrElse
    1.59 +        error("Unknown logic " + quote(name) + " -- no heap file found in:\n" +
    1.60 +          cat_lines(input_dirs.map(dir => "  " + dir.implode)))
    1.61    }
    1.62  }