# HG changeset patch
# User wenzelm
# Date 1491677801 -7200
# Node ID 9425e4d8bdb68a5e7f79cee9f56b03b84b897976
# Parent  fd147f56d9bee33168a1c97fe2ce9807c7ab3c0e
more session_base information in ML;
tuned signature;

diff -r fd147f56d9be -r 9425e4d8bdb6 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 20:56:41 2017 +0200
@@ -6,8 +6,15 @@
 
 signature RESOURCES =
 sig
-  val set_session_base: {known_theories: (string * string) list} -> unit
+  val set_session_base:
+    {default_qualifier: string,
+     global_theories: string list,
+     loaded_theories: (string * string) list,
+     known_theories: (string * string) list} -> unit
   val reset_session_base: unit -> unit
+  val default_qualifier: unit -> string
+  val global_theory: string -> bool
+  val loaded_theory: string -> Path.T option
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
@@ -30,19 +37,32 @@
 
 (* session base *)
 
-val global_session_base =
-  Synchronized.var "Sessions.base"
-    ({known_theories = Symtab.empty: Path.T Symtab.table});
+val init_session_base =
+  {default_qualifier = "",
+   global_theories = Symtab.make_set [],
+   loaded_theories = Symtab.empty: Path.T Symtab.table,
+   known_theories = Symtab.empty: Path.T Symtab.table};
 
-fun set_session_base {known_theories} =
+val global_session_base =
+  Synchronized.var "Sessions.base" init_session_base;
+
+fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
-    (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+    (fn _ =>
+      {default_qualifier = default_qualifier,
+       global_theories = Symtab.make_set global_theories,
+       loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
+       known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun reset_session_base () =
-  set_session_base {known_theories = []};
+  Synchronized.change global_session_base (K init_session_base);
+
+fun get_session_base f = f (Synchronized.value global_session_base);
 
-fun known_theory name =
-  Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
+fun default_qualifier () = get_session_base #default_qualifier;
+fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
+fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
+fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 
 (* manage source files *)
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -14,8 +14,8 @@
 
 
 class Resources(
-  val session_name: String,
   val session_base: Sessions.Base,
+  val default_qualifier: String = "",
   val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
@@ -72,7 +72,7 @@
     val theory0 = Thy_Header.base_name(s)
     val theory =
       if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
-      else Long_Name.qualify(session_name, theory0)
+      else Long_Name.qualify(default_qualifier, theory0)
 
     session_base.loaded_theories.get(theory) orElse
     session_base.loaded_theories.get(theory0) orElse
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -58,6 +58,10 @@
     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)
 
+    def dest_loaded_theories: List[(String, String)] =
+      for ((theory, node_name) <- loaded_theories.toList)
+        yield (theory, node_name.node)
+
     def dest_known_theories: List[(String, String)] =
       for ((theory, node_name) <- known_theories.toList)
         yield (theory, node_name.node)
@@ -91,7 +95,7 @@
               case None => Base.bootstrap
               case Some(parent) => sessions(parent)
             }
-          val resources = new Resources(session_name, parent_base)
+          val resources = new Resources(parent_base, default_qualifier = session_name)
 
           if (verbose || list_files) {
             val groups =
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/build.ML	Sat Apr 08 20:56:41 2017 +0200
@@ -145,6 +145,8 @@
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
+  global_theories: string list,
+  loaded_theories: (string * string) list,
   known_theories: (string * string) list};
 
 fun decode_args yxml =
@@ -152,12 +154,13 @@
     open XML.Decode;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
-      (theories, known_theories)))))))))))) =
+      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
-              (list (pair string string)))))))))))))
+              (pair (list string)
+                (pair (list (pair string string)) (list (pair string string)))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -165,15 +168,22 @@
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
       name = name, master_dir = Path.explode master_dir, theories = theories,
+      global_theories = global_theories, loaded_theories = loaded_theories,
       known_theories = known_theories}
   end;
 
 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
-    document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
+    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
+    global_theories, loaded_theories, known_theories}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
-    val _ = Resources.set_session_base {known_theories = known_theories};
+    val _ =
+      Resources.set_session_base
+        {default_qualifier = name,
+         global_theories = global_theories,
+         loaded_theories = loaded_theories,
+         known_theories = known_theories};
 
     val _ =
       Session.init
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -196,7 +196,7 @@
     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(
             {
@@ -205,12 +205,14 @@
                 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 =
@@ -222,7 +224,7 @@
             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)
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -95,10 +95,15 @@
       session_base match {
         case None => Nil
         case Some(base) =>
-          List("Resources.set_session_base {known_theories = " +
+          def print_table(table: List[(String, String)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
+                ML_Syntax.print_string, ML_Syntax.print_string))(table)
+          List("Resources.set_session_base {default_qualifier = \"\"" +
+            ", global_theories = " +
+              ML_Syntax.print_list(ML_Syntax.print_string)(base.global_theories.toList) +
+            ", loaded_theories = " + print_table(base.dest_loaded_theories) +
+            ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 
     // process
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -43,7 +43,7 @@
     val options: Options,
     session_base: Sessions.Base,
     log: Logger = No_Logger)
-  extends Resources(session_name = "", session_base, log)
+  extends Resources(session_base, log = log)
 {
   private val state = Synchronized(VSCode_Resources.State())
 
diff -r fd147f56d9be -r 9425e4d8bdb6 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Apr 08 12:47:34 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Apr 08 20:56:41 2017 +0200
@@ -21,8 +21,7 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(session_base: Sessions.Base)
-  extends Resources(session_name = "", session_base)
+class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
 {
   /* document node name */