tuned signature;
authorwenzelm
Wed, 25 Jul 2012 22:30:18 +0200
changeset 49520d9e43ea3a045
parent 49519 21dfd6c04482
child 49521 af1dabad14c0
tuned signature;
src/Pure/System/build.scala
     1.1 --- a/src/Pure/System/build.scala	Wed Jul 25 22:25:07 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 25 22:30:18 2012 +0200
     1.3 @@ -420,14 +420,14 @@
     1.4  
     1.5    /* log files and corresponding heaps */
     1.6  
     1.7 -  val LOG = Path.explode("log")
     1.8 -  def log(name: String): Path = LOG + Path.basic(name)
     1.9 -  def log_gz(name: String): Path = log(name).ext("gz")
    1.10 +  private val LOG = Path.explode("log")
    1.11 +  private def log(name: String): Path = LOG + Path.basic(name)
    1.12 +  private def log_gz(name: String): Path = log(name).ext("gz")
    1.13  
    1.14 -  def sources_stamp(digests: List[SHA1.Digest]): String =
    1.15 +  private def sources_stamp(digests: List[SHA1.Digest]): String =
    1.16      digests.map(_.toString).sorted.mkString("sources: ", " ", "")
    1.17  
    1.18 -  def heap_stamp(output: Option[Path]): String =
    1.19 +  private def heap_stamp(output: Option[Path]): String =
    1.20    {
    1.21      "heap: " +
    1.22        (output match {
    1.23 @@ -439,7 +439,7 @@
    1.24        })
    1.25    }
    1.26  
    1.27 -  def check_stamps(dir: Path, name: String): Option[(String, Boolean)] =
    1.28 +  private def check_stamps(dir: Path, name: String): Option[(String, Boolean)] =
    1.29    {
    1.30      val file = (dir + log_gz(name)).file
    1.31      if (file.isFile) {