1.1 --- a/src/Pure/System/build.scala	Tue Jul 24 18:38:07 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Tue Jul 24 20:41:50 2012 +0200
     1.3 @@ -45,6 +45,7 @@
     1.4        base_name: String,
     1.5        dir: Path,
     1.6        parent: Option[String],
     1.7 +      parent_base_name: Option[String],
     1.8        description: String,
     1.9        options: Options,
    1.10        theories: List[(Options, List[Path])],
    1.11 @@ -188,16 +189,19 @@
    1.12        try {
    1.13          if (entry.name == "") error("Bad session name")
    1.14  
    1.15 -        val full_name =
    1.16 +        val (full_name, parent_base_name) =
    1.17            if (is_pure(entry.name)) {
    1.18              if (entry.parent.isDefined) error("Illegal parent session")
    1.19 -            else entry.name
    1.20 +            else (entry.name, None: Option[String])
    1.21            }
    1.22            else
    1.23              entry.parent match {
    1.24                case Some(parent_name) if queue1.defined(parent_name) =>
    1.25 -                if (entry.this_name) entry.name
    1.26 -                else parent_name + "-" + entry.name
    1.27 +                val full_name =
    1.28 +                  if (entry.this_name) entry.name
    1.29 +                  else parent_name + "-" + entry.name
    1.30 +                val parent_base_name = Some(queue1(parent_name).base_name)
    1.31 +                (full_name, parent_base_name)
    1.32                case _ => error("Bad parent session")
    1.33              }
    1.34  
    1.35 @@ -218,7 +222,7 @@
    1.36          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    1.37  
    1.38          val info =
    1.39 -          Session.Info(entry.name, dir + path, entry.parent,
    1.40 +          Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
    1.41              entry.description, session_options, theories, files, digest)
    1.42  
    1.43          queue1 + (key, info)
    1.44 @@ -366,6 +370,7 @@
    1.45      }
    1.46  
    1.47      val parent = info.parent.getOrElse("")
    1.48 +    val parent_base_name = info.parent_base_name.getOrElse("")
    1.49  
    1.50      val cwd = info.dir.file
    1.51      val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
    1.52 @@ -396,7 +401,7 @@
    1.53        import XML.Encode._
    1.54            pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
    1.55              pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
    1.56 -          (output.isDefined, (options, (timing, (verbose, (browser_info, (parent,
    1.57 +          (output.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
    1.58              (name, (info.base_name, info.theories)))))))))
    1.59      }
    1.60      new Job(cwd, env, script, YXML.string_of_body(args_xml))
    1.61 @@ -455,7 +460,6 @@
    1.62          pending.dequeue(running.isDefinedAt(_)) match {
    1.63            case Some((name, info)) =>
    1.64              if (no_build) {
    1.65 -              if (verbose) echo(name + " in " + info.dir)
    1.66                loop(pending - name, running, results + (name -> 0))
    1.67              }
    1.68              else if (info.parent.map(results(_)).forall(_ == 0)) {