src/Pure/Thy/sessions.scala
changeset 62636 e676ae9f1bf6
parent 62635 4854a38061de
child 62637 0189fe0f6452
equal deleted inserted replaced
62635:4854a38061de 62636:e676ae9f1bf6
   340       else {
   340       else {
   341         val ml_ident = Path.explode("$ML_IDENTIFIER").expand
   341         val ml_ident = Path.explode("$ML_IDENTIFIER").expand
   342         output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
   342         output_dir :: Path.split(Isabelle_System.getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
   343       }
   343       }
   344 
   344 
   345     //optional heap + log_gz
   345     def find(name: String): Option[(Path, Option[String])] =
   346     def find(name: String): Option[(Path, Path)] =
       
   347       input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
   346       input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
   348         (dir + Path.basic(name), dir + log_gz(name)))
   347         (dir + log_gz(name), File.time_stamp(dir + Path.basic(name))))
   349 
   348 
   350     def find_heap(name: String): Option[Path] =
   349     def find_heap(name: String): Option[Path] =
   351       input_dirs.map(_ + Path.basic(name)).find(_.is_file)
   350       input_dirs.map(_ + Path.basic(name)).find(_.is_file)
   352 
   351 
   353     def find_log(name: String): Option[Path] =
   352     def find_log(name: String): Option[Path] =