1.1 --- a/src/Pure/System/build.scala	Tue Jul 24 11:39:22 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Tue Jul 24 12:14:16 2012 +0200
     1.3 @@ -209,14 +209,17 @@
     1.4  
     1.5          val key = Session.Key(full_name, entry.order)
     1.6  
     1.7 +        val session_options = options ++ entry.options
     1.8 +
     1.9          val theories =
    1.10 -          entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
    1.11 +          entry.theories.map({ case (opts, thys) =>
    1.12 +            (session_options ++ opts, thys.map(Path.explode(_))) })
    1.13          val files = entry.files.map(Path.explode(_))
    1.14          val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
    1.15  
    1.16          val info =
    1.17            Session.Info(entry.name, dir + path, entry.parent,
    1.18 -            entry.description, options ++ entry.options, theories, files, digest)
    1.19 +            entry.description, session_options, theories, files, digest)
    1.20  
    1.21          queue1 + (key, info)
    1.22        }
    1.23 @@ -344,6 +347,18 @@
    1.24    private def start_job(name: String, info: Session.Info, output: Option[String],
    1.25      options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
    1.26    {
    1.27 +    // global browser info dir
    1.28 +    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
    1.29 +    {
    1.30 +      browser_info.file.mkdirs()
    1.31 +      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    1.32 +        browser_info + Path.explode("isabelle.gif"))
    1.33 +      File.write(browser_info + Path.explode("index.html"),
    1.34 +        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    1.35 +        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    1.36 +        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    1.37 +    }
    1.38 +
    1.39      val parent = info.parent.getOrElse("")
    1.40  
    1.41      val cwd = info.dir.file
    1.42 @@ -399,18 +414,6 @@
    1.43        if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
    1.44        else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
    1.45  
    1.46 -    // prepare browser info dir
    1.47 -    if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
    1.48 -    {
    1.49 -      browser_info.file.mkdirs()
    1.50 -      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
    1.51 -        browser_info + Path.explode("isabelle.gif"))
    1.52 -      File.write(browser_info + Path.explode("index.html"),
    1.53 -        File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    1.54 -        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    1.55 -        File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    1.56 -    }
    1.57 -
    1.58      // prepare log dir
    1.59      val log_dir = output_dir + Path.explode("log")
    1.60      log_dir.file.mkdirs()
    1.61 @@ -458,7 +461,7 @@
    1.62                    Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
    1.63                  else None
    1.64                echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
    1.65 -              val job = start_job(name, info, output, options, timing, verbose, browser_info)
    1.66 +              val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
    1.67                loop(pending, running + (name -> job), results)
    1.68              }
    1.69              else {

     2.1 --- a/src/Pure/System/session.ML	Tue Jul 24 11:39:22 2012 +0200
     2.2 +++ b/src/Pure/System/session.ML	Tue Jul 24 12:14:16 2012 +0200
     2.3 @@ -112,8 +112,9 @@
     2.4  
     2.5  fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
     2.6   (init_name reset parent name;
     2.7 -  Present.init build info info_path doc doc_graph doc_variants (path ()) name
     2.8 -    (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ())));
     2.9 +  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
    2.10 +    (path ()) name (dumping dump) (get_rpath rpath) verbose
    2.11 +    (map Thy_Info.get_theory (Thy_Info.get_names ())));
    2.12  
    2.13  fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    2.14      name dump rpath level timing verbose max_threads trace_threads