1.1 --- a/src/Pure/System/build.scala	Mon Jul 23 22:35:10 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Tue Jul 24 00:29:36 2012 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4      /* Info */
     1.5  
     1.6      sealed case class Info(
     1.7 +      base_name: String,
     1.8        dir: Path,
     1.9        parent: Option[String],
    1.10        description: String,
    1.11 @@ -214,7 +215,7 @@
    1.12          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    1.13  
    1.14          val info =
    1.15 -          Session.Info(dir + path, entry.parent,
    1.16 +          Session.Info(entry.name, dir + path, entry.parent,
    1.17              entry.description, options ++ entry.options, theories, files, digest)
    1.18  
    1.19          queue1 + (key, info)
    1.20 @@ -340,7 +341,8 @@
    1.21      def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
    1.22    }
    1.23  
    1.24 -  private def start_job(name: String, info: Session.Info, output: Option[String]): Job =
    1.25 +  private def start_job(name: String, info: Session.Info, output: Option[String],
    1.26 +    options: Options, verbose: Boolean, browser_info: Path): Job =
    1.27    {
    1.28      val parent = info.parent.getOrElse("")
    1.29  
    1.30 @@ -371,8 +373,10 @@
    1.31      val args_xml =
    1.32      {
    1.33        import XML.Encode._
    1.34 -      pair(bool, pair(string, pair(string, list(string))))(
    1.35 -        output.isDefined, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
    1.36 +          pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
    1.37 +            pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))(
    1.38 +          (output.isDefined, (options, (verbose, (browser_info, (parent,
    1.39 +            (name, (info.base_name, info.theories))))))))
    1.40      }
    1.41      new Job(cwd, env, script, YXML.string_of_body(args_xml))
    1.42    }
    1.43 @@ -454,7 +458,7 @@
    1.44                    Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
    1.45                  else None
    1.46                echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
    1.47 -              val job = start_job(name, info, output)
    1.48 +              val job = start_job(name, info, output, options, verbose, browser_info)
    1.49                loop(pending, running + (name -> job), results)
    1.50              }
    1.51              else {