1.1 --- a/src/Pure/System/build.ML	Fri Jul 27 08:52:40 2012 +0200
     1.2 +++ b/src/Pure/System/build.ML	Fri Jul 27 12:29:07 2012 +0200
     1.3 @@ -56,12 +56,12 @@
     1.4  
     1.5  fun build args_file =
     1.6    let
     1.7 -    val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
     1.8 -        (name, (base_name, theories)))))))) =
     1.9 +    val (do_output, (options, (timing, (verbose, (browser_info, (parent_name,
    1.10 +        (name, theories))))))) =
    1.11        File.read (Path.explode args_file) |> YXML.parse_body |>
    1.12          let open XML.Decode in
    1.13            pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
    1.14 -            (pair string (pair string ((list (pair Options.decode (list string)))))))))))
    1.15 +            (pair string ((list (pair Options.decode (list string))))))))))
    1.16          end;
    1.17  
    1.18      val _ =
    1.19 @@ -70,7 +70,7 @@
    1.20          (Options.string options "document")
    1.21          (Options.bool options "document_graph")
    1.22          (space_explode ":" (Options.string options "document_variants"))
    1.23 -        parent_base_name base_name
    1.24 +        parent_name name
    1.25          (Options.string options "document_dump", Options.string options "document_dump_mode")
    1.26          "" verbose;
    1.27      val _ = Session.with_timing name timing (List.app use_theories) theories;

     2.1 --- a/src/Pure/System/build.scala	Fri Jul 27 08:52:40 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Fri Jul 27 12:29:07 2012 +0200
     2.3 @@ -28,7 +28,6 @@
     2.4        groups: List[String],
     2.5        dir: Path,
     2.6        parent: Option[String],
     2.7 -      parent_base_name: Option[String],
     2.8        description: String,
     2.9        options: Options,
    2.10        theories: List[(Options, List[Path])],
    2.11 @@ -165,10 +164,10 @@
    2.12        try {
    2.13          if (entry.name == "") error("Bad session name")
    2.14  
    2.15 -        val (full_name, parent_base_name) =
    2.16 +        val full_name =
    2.17            if (is_pure(entry.name)) {
    2.18              if (entry.parent.isDefined) error("Illegal parent session")
    2.19 -            else (entry.name, None: Option[String])
    2.20 +            else entry.name
    2.21            }
    2.22            else
    2.23              entry.parent match {
    2.24 @@ -176,8 +175,7 @@
    2.25                  val full_name =
    2.26                    if (entry.this_name) entry.name
    2.27                    else parent_name + "-" + entry.name
    2.28 -                val parent_base_name = Some(queue1(parent_name).base_name)
    2.29 -                (full_name, parent_base_name)
    2.30 +                full_name
    2.31                case _ => error("Bad parent session")
    2.32              }
    2.33  
    2.34 @@ -196,7 +194,7 @@
    2.35          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    2.36  
    2.37          val info =
    2.38 -          Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name,
    2.39 +          Session.Info(entry.name, entry.groups, dir + path, entry.parent,
    2.40              entry.description, session_options, theories, files, digest)
    2.41  
    2.42          queue1 + (full_name, info)
    2.43 @@ -351,7 +349,6 @@
    2.44      }
    2.45  
    2.46      val parent = info.parent.getOrElse("")
    2.47 -    val parent_base_name = info.parent_base_name.getOrElse("")
    2.48  
    2.49      val cwd = info.dir.file
    2.50      val env =
    2.51 @@ -389,9 +386,9 @@
    2.52      {
    2.53        import XML.Encode._
    2.54            pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
    2.55 -            pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
    2.56 -          (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
    2.57 -            (name, (info.base_name, info.theories)))))))))
    2.58 +            pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
    2.59 +          (do_output, (options, (timing, (verbose, (browser_info, (parent,
    2.60 +            (name, info.theories))))))))
    2.61      }
    2.62      new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
    2.63    }