equal
deleted
inserted
replaced
1130 def output_heap(name: String): Path = output_dir + heap(name) |
1130 def output_heap(name: String): Path = output_dir + heap(name) |
1131 def output_database(name: String): Path = output_dir + database(name) |
1131 def output_database(name: String): Path = output_dir + database(name) |
1132 def output_log(name: String): Path = output_dir + log(name) |
1132 def output_log(name: String): Path = output_dir + log(name) |
1133 def output_log_gz(name: String): Path = output_dir + log_gz(name) |
1133 def output_log_gz(name: String): Path = output_dir + log_gz(name) |
1134 |
1134 |
1135 def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) } |
1135 def prepare_output_dir() { Isabelle_System.make_directory(output_dir + Path.basic("log")) } |
1136 |
1136 |
1137 |
1137 |
1138 /* heap */ |
1138 /* heap */ |
1139 |
1139 |
1140 def find_heap(name: String): Option[Path] = |
1140 def find_heap(name: String): Option[Path] = |