# HG changeset patch
# User wenzelm
# Date 1343155310 -7200
# Node ID 45137257399ad116838165a42ba64e8ae5196c48
# Parent  2c828c830ad7358d864c84a2a7af9f71d011ef54
pass parent_base_name, which is required for Session.init sanity check;
tuned message;

diff -r 2c828c830ad7 -r 45137257399a src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 18:38:07 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 20:41:50 2012 +0200
@@ -41,7 +41,7 @@
 
 fun build args_file =
   let
-    val (save, (options, (timing, (verbose, (browser_info, (parent,
+    val (save, (options, (timing, (verbose, (browser_info, (parent_base_name,
         (name, (base_name, theories)))))))) =
       File.read (Path.explode args_file) |> YXML.parse_body |>
         let open XML.Decode in
@@ -55,7 +55,7 @@
         (Options.string options "document")
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
-        parent base_name
+        parent_base_name base_name
         (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
         (Options.string options "browser_info_remote")
         verbose;
diff -r 2c828c830ad7 -r 45137257399a src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Jul 24 18:38:07 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Jul 24 20:41:50 2012 +0200
@@ -45,6 +45,7 @@
       base_name: String,
       dir: Path,
       parent: Option[String],
+      parent_base_name: Option[String],
       description: String,
       options: Options,
       theories: List[(Options, List[Path])],
@@ -188,16 +189,19 @@
       try {
         if (entry.name == "") error("Bad session name")
 
-        val full_name =
+        val (full_name, parent_base_name) =
           if (is_pure(entry.name)) {
             if (entry.parent.isDefined) error("Illegal parent session")
-            else entry.name
+            else (entry.name, None: Option[String])
           }
           else
             entry.parent match {
               case Some(parent_name) if queue1.defined(parent_name) =>
-                if (entry.this_name) entry.name
-                else parent_name + "-" + entry.name
+                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)
               case _ => error("Bad parent session")
             }
 
@@ -218,7 +222,7 @@
         val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
 
         val info =
-          Session.Info(entry.name, dir + path, entry.parent,
+          Session.Info(entry.name, dir + path, entry.parent, parent_base_name,
             entry.description, session_options, theories, files, digest)
 
         queue1 + (key, info)
@@ -366,6 +370,7 @@
     }
 
     val parent = info.parent.getOrElse("")
+    val parent_base_name = info.parent_base_name.getOrElse("")
 
     val cwd = info.dir.file
     val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
@@ -396,7 +401,7 @@
       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)))))))))))(
-          (output.isDefined, (options, (timing, (verbose, (browser_info, (parent,
+          (output.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
             (name, (info.base_name, info.theories)))))))))
     }
     new Job(cwd, env, script, YXML.string_of_body(args_xml))
@@ -455,7 +460,6 @@
         pending.dequeue(running.isDefinedAt(_)) match {
           case Some((name, info)) =>
             if (no_build) {
-              if (verbose) echo(name + " in " + info.dir)
               loop(pending - name, running, results + (name -> 0))
             }
             else if (info.parent.map(results(_)).forall(_ == 0)) {