src/Pure/Tools/build.scala

     catch { case ERROR(_) => /*error should be exposed in ML*/ }
 
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
-
+        val base = deps(name)
         val args_yxml =
           YXML.string_of_body(
             {
               import XML.Encode._
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(string))),
-                list(pair(string, string))))))))))))))(
+                pair(list(string),
+                pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
                 (info.theories,
-                deps(name).dest_known_theories)))))))))))))
+                (base.global_theories.toList,
+                (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
             })
 
         val env =
           Isabelle_System.settings() +
             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)

         def save_heap: String =
           "ML_Heap.share_common_data (); ML_Heap.save_child " +
             ML_Syntax.print_string0(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
-          val resources = new Resources(name, deps(parent))
+          val resources = new Resources(deps(parent), default_qualifier = name)
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
 
           val session_result = Future.promise[Process_Result]