# HG changeset patch
# User wenzelm
# Date 1343384947 -7200
# Node ID f31ef1a0285a66d113a4b44cf0b113d08fc870b1
# Parent  122e67e77493718024bdf841cd5a71f401b5abb1
more precise imitation of usedir wrt. Session.name (cf. 45137257399a);

diff -r 122e67e77493 -r f31ef1a0285a src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/Pure/System/build.ML	Fri Jul 27 12:29:07 2012 +0200
@@ -56,12 +56,12 @@
 
 fun build args_file =
   let
-    val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
-        (name, (base_name, theories)))))))) =
+    val (do_output, (options, (timing, (verbose, (browser_info, (parent_name,
+        (name, theories))))))) =
       File.read (Path.explode args_file) |> YXML.parse_body |>
         let open XML.Decode in
           pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string
-            (pair string (pair string ((list (pair Options.decode (list string)))))))))))
+            (pair string ((list (pair Options.decode (list string))))))))))
         end;
 
     val _ =
@@ -70,7 +70,7 @@
         (Options.string options "document")
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
-        parent_base_name base_name
+        parent_name name
         (Options.string options "document_dump", Options.string options "document_dump_mode")
         "" verbose;
     val _ = Session.with_timing name timing (List.app use_theories) theories;
diff -r 122e67e77493 -r f31ef1a0285a src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/Pure/System/build.scala	Fri Jul 27 12:29:07 2012 +0200
@@ -28,7 +28,6 @@
       groups: List[String],
       dir: Path,
       parent: Option[String],
-      parent_base_name: Option[String],
       description: String,
       options: Options,
       theories: List[(Options, List[Path])],
@@ -165,10 +164,10 @@
       try {
         if (entry.name == "") error("Bad session name")
 
-        val (full_name, parent_base_name) =
+        val full_name =
           if (is_pure(entry.name)) {
             if (entry.parent.isDefined) error("Illegal parent session")
-            else (entry.name, None: Option[String])
+            else entry.name
           }
           else
             entry.parent match {
@@ -176,8 +175,7 @@
                 val full_name =
                   if (entry.this_name) entry.name
                   else parent_name + "-" + entry.name
-                val parent_base_name = Some(queue1(parent_name).base_name)
-                (full_name, parent_base_name)
+                full_name
               case _ => error("Bad parent session")
             }
 
@@ -196,7 +194,7 @@
         val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
 
         val info =
-          Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name,
+          Session.Info(entry.name, entry.groups, dir + path, entry.parent,
             entry.description, session_options, theories, files, digest)
 
         queue1 + (full_name, info)
@@ -351,7 +349,6 @@
     }
 
     val parent = info.parent.getOrElse("")
-    val parent_base_name = info.parent_base_name.getOrElse("")
 
     val cwd = info.dir.file
     val env =
@@ -389,9 +386,9 @@
     {
       import XML.Encode._
           pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
-            pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
-          (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name,
-            (name, (info.base_name, info.theories)))))))))
+            pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
+          (do_output, (options, (timing, (verbose, (browser_info, (parent,
+            (name, info.theories))))))))
     }
     new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output)
   }