1.1 --- a/src/Pure/System/build.scala	Fri Jul 27 08:52:40 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Fri Jul 27 12:29:07 2012 +0200
     1.3 @@ -28,7 +28,6 @@
     1.4        groups: List[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 @@ -165,10 +164,10 @@
    1.12        try {
    1.13          if (entry.name == "") error("Bad session name")
    1.14  
    1.15 -        val (full_name, parent_base_name) =
    1.16 +        val full_name =
    1.17            if (is_pure(entry.name)) {
    1.18              if (entry.parent.isDefined) error("Illegal parent session")
    1.19 -            else (entry.name, None: Option[String])
    1.20 +            else entry.name
    1.21            }
    1.22            else
    1.23              entry.parent match {
    1.24 @@ -176,8 +175,7 @@
    1.25                  val full_name =
    1.26                    if (entry.this_name) entry.name
    1.27                    else parent_name + "-" + entry.name
    1.28 -                val parent_base_name = Some(queue1(parent_name).base_name)
    1.29 -                (full_name, parent_base_name)
    1.30 +                full_name
    1.31                case _ => error("Bad parent session")
    1.32              }
    1.33  
    1.34 @@ -196,7 +194,7 @@
    1.35          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    1.36  
    1.37          val info =
    1.38 -          Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name,
    1.39 +          Session.Info(entry.name, entry.groups, dir + path, entry.parent,
    1.40              entry.description, session_options, theories, files, digest)
    1.41  
    1.42          queue1 + (full_name, info)
    1.43 @@ -351,7 +349,6 @@
    1.44      }
    1.45  
    1.46      val parent = info.parent.getOrElse("")
    1.47 -    val parent_base_name = info.parent_base_name.getOrElse("")
    1.48  
    1.49      val cwd = info.dir.file
    1.50      val env =
    1.51 @@ -389,9 +386,9 @@
    1.52      {
    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 -          (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
    1.57 -            (name, (info.base_name, info.theories)))))))))
    1.58 +            pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
    1.59 +          (do_output, (options, (timing, (verbose, (browser_info, (parent,
    1.60 +            (name, info.theories))))))))
    1.61      }
    1.62      new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
    1.63    }