# HG changeset patch
# User wenzelm
# Date 1491230205 -7200
# Node ID 9ca34f0407a9ece35c396b5f459133202a2e0fc5
# Parent  e345e94201093b00fcb3a7f0dae4489508a68f2b
provide session qualifier via resources;

diff -r e345e9420109 -r 9ca34f0407a9 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -435,7 +435,7 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val reader = Scan.char_reader(Token.implode(span.content))
-        val header = resources.check_thy_reader("", node_name, reader)
+        val header = resources.check_thy_reader(node_name, reader)
         val errors =
           for ((imp, pos) <- header.imports if !can_import(imp)) yield {
             val msg =
diff -r e345e9420109 -r 9ca34f0407a9 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -13,25 +13,16 @@
 import java.io.{File => JFile}
 
 
-class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
+class Resources(
+  val session_name: String,
+  val base: Sessions.Base,
+  val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
 
   def thy_path(path: Path): Path = path.ext("thy")
 
 
-  /* document node names */
-
-  def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
-  {
-    val path = raw_path.expand
-    val node = path.implode
-    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
-    val master_dir = if (theory == "") "" else path.dir.implode
-    Document.Node.Name(node, master_dir, theory)
-  }
-
-
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
@@ -76,10 +67,20 @@
     }
     else Nil
 
-  def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
+  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
+  {
+    val path = raw_path.expand
+    val node = path.implode
+    val qualifier = if (global) "" else session_name
+    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+    val master_dir = if (theory == "") "" else path.dir.implode
+    Document.Node.Name(node, master_dir, theory)
+  }
+
+  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val thy1 = Thy_Header.base_name(s)
-    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
+    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
     (base.known_theories.get(thy1) orElse
      base.known_theories.get(thy2) orElse
      base.known_theories.get(Long_Name.base_name(thy1))) match {
@@ -92,7 +93,7 @@
         else {
           val node = append(master.master_dir, thy_path(path))
           val master_dir = append(master.master_dir, path.dir)
-          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
+          Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
         }
     }
   }
@@ -106,9 +107,8 @@
     try { f(reader) } finally { reader.close }
   }
 
-  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
-      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
-    : Document.Node.Header =
+  def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
+    start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
@@ -122,7 +122,7 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
+          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -130,18 +130,18 @@
     else Document.Node.no_header
   }
 
-  def check_thy(qualifier: String, name: Document.Node.Name,
-      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
-    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
+  def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
+      strict: Boolean = true): Document.Node.Header =
+    with_thy_reader(name, check_thy_reader(name, _, start, strict))
 
 
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
     if (Thy_Header.is_ml_root(name.theory))
-      Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
+      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
     else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
+      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
     else None
 
 
diff -r e345e9420109 -r 9ca34f0407a9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -71,12 +71,12 @@
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
-            val resources =
-              new Resources(
-                info.parent match {
-                  case None => Base.bootstrap
-                  case Some(parent) => deps(parent)
-                })
+            val parent_base =
+              info.parent match {
+                case None => Base.bootstrap
+                case Some(parent) => deps(parent)
+              }
+            val resources = new Resources(name, parent_base)
 
             if (verbose || list_files) {
               val groups =
@@ -91,10 +91,9 @@
                 info.theories.flatMap({
                   case (global, _, thys) =>
                     thys.map(thy =>
-                      (resources.node_name(
-                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
+                      (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
                 })
-              val thy_deps = resources.thy_info.dependencies(name, root_theories)
+              val thy_deps = resources.thy_info.dependencies(root_theories)
 
               thy_deps.errors match {
                 case Nil => thy_deps
@@ -103,7 +102,7 @@
             }
 
             val known_theories =
-              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
+              (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) =>
                 val name = dep.name
                 known.get(name.theory) match {
                   case Some(name1) if name != name1 =>
@@ -142,7 +141,7 @@
 
             val session_graph =
               Present.session_graph(info.parent getOrElse "",
-                resources.base.loaded_theories, thy_deps.deps)
+                parent_base.loaded_theories, thy_deps.deps)
 
             val base =
               Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
diff -r e345e9420109 -r 9ca34f0407a9 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -104,12 +104,12 @@
     override def toString: String = deps.toString
   }
 
-  private def require_thys(session: String, initiators: List[Document.Node.Name],
-      required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    (required /: thys)(require_thy(session, initiators, _, _))
+  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
+      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    (required /: thys)(require_thy(initiators, _, _))
 
-  private def require_thy(session: String, initiators: List[Document.Node.Name],
-      required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
+  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
+    thy: (Document.Node.Name, Position.T)): Dependencies =
   {
     val (name, require_pos) = thy
 
@@ -123,10 +123,9 @@
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
-          try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
+          try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
           catch { case ERROR(msg) => cat_error(msg, message) }
-        Thy_Info.Dep(name, header) ::
-          require_thys(session, name :: initiators, required1, header.imports)
+        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
       }
       catch {
         case e: Throwable =>
@@ -135,6 +134,6 @@
     }
   }
 
-  def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    require_thys(session, Nil, Dependencies.empty, thys)
+  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    require_thys(Nil, Dependencies.empty, thys)
 }
diff -r e345e9420109 -r 9ca34f0407a9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -220,7 +220,7 @@
             ML_Syntax.print_string0(File.platform_path(output))
 
         if (pide && !Sessions.pure_name(name)) {
-          val resources = new Resources(deps(parent))
+          val resources = new Resources(name, deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
diff -r e345e9420109 -r 9ca34f0407a9 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Tools/VSCode/src/document_model.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -73,7 +73,7 @@
 
   def node_header: Document.Node.Header =
     resources.special_header(node_name) getOrElse
-      resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
+      resources.check_thy_reader(node_name, Scan.char_reader(content.text))
 
 
   /* perspective */
diff -r e345e9420109 -r 9ca34f0407a9 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -42,7 +42,7 @@
 class VSCode_Resources(
   val options: Options,
   base: Sessions.Base,
-  log: Logger = No_Logger) extends Resources(base, log)
+  log: Logger = No_Logger) extends Resources(session_name = "", base, log)
 {
   private val state = Synchronized(VSCode_Resources.State())
 
@@ -165,7 +165,7 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
+        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
 
 
         /* auxiliary files */
diff -r e345e9420109 -r 9ca34f0407a9 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -235,7 +235,7 @@
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
-            val retain = PIDE.resources.thy_info.dependencies("", imports).deps.map(_.name).toSet
+            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
 
             for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
               yield edit
@@ -331,7 +331,7 @@
 
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
-      PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
+      PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
 
 
   /* content */
@@ -396,8 +396,7 @@
 
     PIDE.resources.special_header(node_name) getOrElse
       JEdit_Lib.buffer_lock(buffer) {
-        PIDE.resources.check_thy_reader(
-          "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
+        PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
       }
   }
 
diff -r e345e9420109 -r 9ca34f0407a9 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -21,7 +21,7 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(base: Sessions.Base) extends Resources(base)
+class JEdit_Resources(base: Sessions.Base) extends Resources(session_name = "", base)
 {
   /* document node name */
 
diff -r e345e9420109 -r 9ca34f0407a9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 14:29:44 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 16:36:45 2017 +0200
@@ -135,7 +135,7 @@
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList
-          val thy_files = resources.thy_info.dependencies("", thys).deps.map(_.name)
+          val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {