# 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)) {