tuned signature;
authorwenzelm
Thu Mar 16 21:22:01 2017 +0100 (2017-03-16)
changeset 65278b553d0edc440
parent 65277 e9f9f962828d
child 65279 fa62e095d8f1
tuned signature;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Mar 16 21:09:13 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Mar 16 21:22:01 2017 +0100
     1.3 @@ -515,13 +515,16 @@
     1.4  
     1.5    /** persistent store **/
     1.6  
     1.7 -  def log(name: String): Path = Path.basic("log") + Path.basic(name)
     1.8 -  def log_gz(name: String): Path = log(name).ext("gz")
     1.9 -
    1.10    def store(system_mode: Boolean = false): Store = new Store(system_mode)
    1.11  
    1.12    class Store private[Sessions](system_mode: Boolean)
    1.13    {
    1.14 +    /* file names */
    1.15 +
    1.16 +    def log(name: String): Path = Path.basic("log") + Path.basic(name)
    1.17 +    def log_gz(name: String): Path = log(name).ext("gz")
    1.18 +
    1.19 +
    1.20      /* output */
    1.21  
    1.22      val browser_info: Path =
     2.1 --- a/src/Pure/Tools/build.scala	Thu Mar 16 21:09:13 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Mar 16 21:22:01 2017 +0100
     2.3 @@ -372,7 +372,7 @@
     2.4      if (clean_build) {
     2.5        for (name <- full_tree.graph.all_succs(selected)) {
     2.6          val files =
     2.7 -          List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)).
     2.8 +          List(Path.basic(name), store.log(name), store.log_gz(name)).
     2.9              map(store.output_dir + _).filter(_.is_file)
    2.10          if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
    2.11          if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
    2.12 @@ -429,18 +429,18 @@
    2.13                val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
    2.14                process_result.copy(
    2.15                  out_lines =
    2.16 -                  "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" ::
    2.17 +                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
    2.18                    lines1)
    2.19              }
    2.20  
    2.21              val heap_stamp =
    2.22                if (process_result.ok) {
    2.23 -                (store.output_dir + Sessions.log(name)).file.delete
    2.24 +                (store.output_dir + store.log(name)).file.delete
    2.25                  val heap_stamp =
    2.26                    for (path <- job.output_path if path.is_file)
    2.27                      yield Sessions.write_heap_digest(path)
    2.28  
    2.29 -                File.write_gzip(store.output_dir + Sessions.log_gz(name),
    2.30 +                File.write_gzip(store.output_dir + store.log_gz(name),
    2.31                    terminate_lines(
    2.32                      session_sources_stamp(name) ::
    2.33                      input_heaps.map(INPUT_HEAP + _) :::
    2.34 @@ -451,9 +451,9 @@
    2.35                }
    2.36                else {
    2.37                  (store.output_dir + Path.basic(name)).file.delete
    2.38 -                (store.output_dir + Sessions.log_gz(name)).file.delete
    2.39 +                (store.output_dir + store.log_gz(name)).file.delete
    2.40  
    2.41 -                File.write(store.output_dir + Sessions.log(name),
    2.42 +                File.write(store.output_dir + store.log(name),
    2.43                    terminate_lines(process_result.out_lines))
    2.44                  progress.echo(name + " FAILED")
    2.45                  if (!process_result.interrupted) progress.echo(process_result_tail.out)