src/Pure/Tools/build.scala
changeset 65441 9425e4d8bdb6
parent 65432 d938705819bb
child 65456 31e8a86971a8
     1.1 --- a/src/Pure/Tools/build.scala	Sat Apr 08 12:47:34 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat Apr 08 20:56:41 2017 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4      private val future_result: Future[Process_Result] =
     1.5        Future.thread("build") {
     1.6          val parent = info.parent.getOrElse("")
     1.7 -
     1.8 +        val base = deps(name)
     1.9          val args_yxml =
    1.10            YXML.string_of_body(
    1.11              {
    1.12 @@ -205,12 +205,14 @@
    1.13                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    1.14                  pair(string, pair(string, pair(string, pair(Path.encode,
    1.15                  pair(list(pair(Options.encode, list(string))),
    1.16 -                list(pair(string, string))))))))))))))(
    1.17 +                pair(list(string),
    1.18 +                pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
    1.19                (Symbol.codes, (command_timings, (do_output, (verbose,
    1.20                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    1.21                  (parent, (info.chapter, (name, (Path.current,
    1.22                  (info.theories,
    1.23 -                deps(name).dest_known_theories)))))))))))))
    1.24 +                (base.global_theories.toList,
    1.25 +                (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
    1.26              })
    1.27  
    1.28          val env =
    1.29 @@ -222,7 +224,7 @@
    1.30              ML_Syntax.print_string0(File.platform_path(output))
    1.31  
    1.32          if (pide && !Sessions.is_pure(name)) {
    1.33 -          val resources = new Resources(name, deps(parent))
    1.34 +          val resources = new Resources(deps(parent), default_qualifier = name)
    1.35            val session = new Session(options, resources)
    1.36            val handler = new Handler(progress, session, name)
    1.37            session.init_protocol_handler(handler)