--- 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