# HG changeset patch
# User wenzelm
# Date 1398890142 -7200
# Node ID c83eb2435b274a78ede702daeb3fb540cee21445
# Parent  939e88e797244963046ec51565ed481bca04eead# Parent  8dd9df88f647519c5dc5de664c4a3554763c485a
merged

diff -r 939e88e79724 -r c83eb2435b27 src/FOL/ROOT
--- a/src/FOL/ROOT	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/FOL/ROOT	Wed Apr 30 22:35:42 2014 +0200
@@ -15,7 +15,9 @@
 
     Michael Dummett, Elements of Intuitionism (Oxford, 1977)
   *}
-  theories FOL
+  global_theories
+    IFOL
+    FOL
   document_files "root.tex"
 
 session "FOL-ex" in ex = FOL +
diff -r 939e88e79724 -r c83eb2435b27 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/HOL/ROOT	Wed Apr 30 22:35:42 2014 +0200
@@ -5,7 +5,9 @@
     Classical Higher-order Logic.
   *}
   options [document_graph]
-  theories Complex_Main
+  global_theories
+    Main
+    Complex_Main
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -174,7 +174,7 @@
           (full_name, descr_name) =
             if (kind == "") (name, quote(decode(name)))
             else
-             (kind + "." + name,
+             (Long_Name.qualify(kind, name),
               Word.implode(Word.explode('_', kind)) + " " + quote(decode(name)))
           description = List(xname1, "(" + descr_name + ")")
         } yield Item(range, original, full_name, description, xname1, 0, true)
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/General/long_name.ML	Wed Apr 30 22:35:42 2014 +0200
@@ -26,6 +26,7 @@
 struct
 
 val separator = ".";
+
 val is_qualified = exists_string (fn s => s = separator);
 
 fun hidden name = "??." ^ name;
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/General/long_name.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/long_name.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -0,0 +1,28 @@
+/*  Title:      Pure/General/long_name.scala
+    Author:     Makarius
+
+Long names.
+*/
+
+package isabelle
+
+
+object Long_Name
+{
+  val separator = "."
+  val separator_char = '.'
+
+  def is_qualified(name: String): Boolean = name.contains(separator_char)
+
+  def implode(names: List[String]): String = names.mkString(separator)
+  def explode(name: String): List[String] = Library.space_explode(separator_char, name)
+
+  def qualify(qual: String, name: String): String =
+    if (qual == "" || name == "") name
+    else qual + separator + name
+
+  def base_name(name: String): String =
+    if (name == "") ""
+    else explode(name).last
+}
+
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/Isar/parse.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -71,6 +71,8 @@
       atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
     def theory_name: Parser[String] =
       atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
+    def theory_xname: Parser[String] =
+      atom("theory name reference", tok => tok.is_xname && Path.is_wellformed(tok.content))
 
     private def tag_name: Parser[String] =
       atom("tag name", tok =>
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 30 22:35:42 2014 +0200
@@ -429,7 +429,7 @@
 
 fun loaded_theory name =
   (case try (unsuffix ".thy") name of
-    SOME a => Thy_Info.lookup_theory a
+    SOME a => get_first Thy_Info.lookup_theory [a, Long_Name.base_name a]
   | NONE => NONE);
 
 fun init_theory deps node span =
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -123,6 +123,8 @@
 
       def is_theory: Boolean = !theory.isEmpty
       override def toString: String = if (is_theory) theory else node
+
+      def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
     }
 
 
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -395,6 +395,7 @@
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = Isabelle_System.posix_path_url(name.master_dir)
+              val theory = Long_Name.base_name(name.theory)
               val imports = header.imports.map(_.node)
               val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
               (Nil,
@@ -402,7 +403,7 @@
                   pair(list(pair(Encode.string,
                     option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
                   list(Encode.string)))))(
-                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -18,15 +18,18 @@
 }
 
 
-class Resources(val loaded_theories: Set[String] = Set.empty, val base_syntax: Prover.Syntax)
+class Resources(
+  val loaded_theories: Set[String],
+  val known_theories: Map[String, Document.Node.Name],
+  val base_syntax: Prover.Syntax)
 {
   /* document node names */
 
-  def node_name(raw_path: Path): Document.Node.Name =
+  def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
   {
     val path = raw_path.expand
     val node = path.implode
-    val theory = Thy_Header.thy_name(node).getOrElse("")
+    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)
   }
@@ -57,36 +60,50 @@
     }
     else Nil
 
-  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
+  private def dummy_name(theory: String): Document.Node.Name =
+    Document.Node.Name(theory + ".thy", "", theory)
+
+  def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
   {
-    val theory = Thy_Header.base_name(s)
-    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
-    else {
-      val path = Path.explode(s)
-      val node = append(master.master_dir, Resources.thy_path(path))
-      val master_dir = append(master.master_dir, path.dir)
-      Document.Node.Name(node, master_dir, theory)
+    val thy1 = Thy_Header.base_name(s)
+    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
+    (known_theories.get(thy1) orElse
+     known_theories.get(thy2) orElse
+     known_theories.get(Long_Name.base_name(thy1))) match {
+      case Some(name) if loaded_theories(name.theory) => dummy_name(name.theory)
+      case Some(name) => name
+      case None =>
+        val path = Path.explode(s)
+        val theory = path.base.implode
+        if (Long_Name.is_qualified(theory)) dummy_name(theory)
+        else {
+          val node = append(master.master_dir, Resources.thy_path(path))
+          val master_dir = append(master.master_dir, path.dir)
+          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
+        }
     }
   }
 
-  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
+  def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence)
+    : Document.Node.Header =
   {
     try {
       val header = Thy_Header.read(text)
 
+      val base_name = Long_Name.base_name(name.theory)
       val name1 = header.name
-      if (name.theory != name1)
-        error("Bad file name " + Resources.thy_path(Path.basic(name.theory)) +
+      if (base_name != name1)
+        error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
           " for theory " + quote(name1))
 
-      val imports = header.imports.map(import_name(name, _))
+      val imports = header.imports.map(import_name(qualifier, name, _))
       Document.Node.Header(imports, header.keywords, Nil)
     }
     catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   }
 
-  def check_thy(name: Document.Node.Name): Document.Node.Header =
-    with_thy_text(name, check_thy_text(name, _))
+  def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
+    with_thy_text(name, check_thy_text(qualifier, name, _))
 
 
   /* document changes */
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -8,7 +8,6 @@
 package isabelle
 
 
-import scala.collection.mutable
 import scala.collection.immutable.Queue
 
 
@@ -95,7 +94,6 @@
   }
 
 
-
   /* protocol handlers */
 
   abstract class Protocol_Handler
@@ -201,31 +199,18 @@
 
 
 
-  /** pipelined change parsing **/
+  /** main protocol manager **/
 
-  private case class Text_Edits(
-    previous: Future[Document.Version],
-    doc_blobs: Document.Blobs,
-    text_edits: List[Document.Edit_Text],
-    version_result: Promise[Document.Version])
+  /* internal messages */
 
-  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
-  {
-    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
-      val prev = previous.get_finished
-      val change =
-        Timing.timeit("parse_change", timing) {
-          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
-        }
-      version_result.fulfill(change.version)
-      manager.send(change)
-      true
-  }
+  private case class Start(name: String, args: List[String])
+  private case object Stop
+  private case class Cancel_Exec(exec_id: Document_ID.Exec)
+  private case class Protocol_Command(name: String, args: List[String])
+  private case class Update_Options(options: Options)
+  private case object Prune_History
 
 
-
-  /** main protocol manager **/
-
   /* global state */
 
   private val syslog = new Session.Syslog(syslog_limit)
@@ -249,10 +234,6 @@
     version.syntax getOrElse resources.base_syntax
   }
 
-  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
-      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
-    global_state.value.snapshot(name, pending_edits)
-
 
   /* protocol handlers */
 
@@ -274,14 +255,26 @@
   }
 
 
-  /* internal messages */
+  /* pipelined change parsing */
+
+  private case class Text_Edits(
+    previous: Future[Document.Version],
+    doc_blobs: Document.Blobs,
+    text_edits: List[Document.Edit_Text],
+    version_result: Promise[Document.Version])
 
-  private case class Start(name: String, args: List[String])
-  private case object Stop
-  private case class Cancel_Exec(exec_id: Document_ID.Exec)
-  private case class Protocol_Command(name: String, args: List[String])
-  private case class Update_Options(options: Options)
-  private case object Prune_History
+  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
+  {
+    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
+      val prev = previous.get_finished
+      val change =
+        Timing.timeit("parse_change", timing) {
+          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
+        }
+      version_result.fulfill(change.version)
+      manager.send(change)
+      true
+  }
 
 
   /* buffered changes */
@@ -573,7 +566,11 @@
   }
 
 
-  /* actions */
+  /* main operations */
+
+  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
+      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
+    global_state.value.snapshot(name, pending_edits)
 
   def start(name: String, args: List[String])
   { manager.send(Start(name, args)) }
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/ROOT	Wed Apr 30 22:35:42 2014 +0200
@@ -26,7 +26,7 @@
     "ML-Systems/use_context.ML"
 
 session Pure =
-  theories Pure
+  global_theories Pure
   files
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/Thy/thy_header.ML	Wed Apr 30 22:35:42 2014 +0200
@@ -83,8 +83,9 @@
 local
 
 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
+val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
 
-val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name);
+val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
 
 val opt_files =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -67,7 +67,7 @@
 
     val args =
       theory_name ~
-      (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       keyword(BEGIN) ^^
       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -95,11 +95,11 @@
     }
   }
 
-  private def require_thys(initiators: List[Document.Node.Name],
+  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(initiators, _, _))
+    (required /: thys)(require_thy(session, initiators, _, _))
 
-  private def require_thy(initiators: List[Document.Node.Name],
+  private def require_thy(session: String, initiators: List[Document.Node.Name],
       required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
   {
     val (name, require_pos) = thy
@@ -116,10 +116,10 @@
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
         val header =
-          try { resources.check_thy(name).cat_errors(message) }
+          try { resources.check_thy(session, name).cat_errors(message) }
           catch { case ERROR(msg) => cat_error(msg, message) }
         val imports = header.imports.map((_, Position.File(name.node)))
-        Dep(name, header) :: require_thys(name :: initiators, required1, imports)
+        Dep(name, header) :: require_thys(session, name :: initiators, required1, imports)
       }
       catch {
         case e: Throwable =>
@@ -128,6 +128,6 @@
     }
   }
 
-  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
-    require_thys(Nil, Dependencies.empty, thys)
+  def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
+    require_thys(session, Nil, Dependencies.empty, thys)
 }
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -56,7 +56,7 @@
     parent: Option[String],
     description: String,
     options: List[Options.Spec],
-    theories: List[(List[Options.Spec], List[String])],
+    theories: List[(Boolean, List[Options.Spec], List[String])],
     files: List[String],
     document_files: List[(String, String)]) extends Entry
 
@@ -70,7 +70,7 @@
     parent: Option[String],
     description: String,
     options: Options,
-    theories: List[(Options, List[Path])],
+    theories: List[(Boolean, Options, List[Path])],
     files: List[Path],
     document_files: List[(Path, Path)],
     entry_digest: SHA1.Digest)
@@ -89,8 +89,8 @@
       val session_options = options ++ entry.options
 
       val theories =
-        entry.theories.map({ case (opts, thys) =>
-          (session_options ++ opts, thys.map(Path.explode(_))) })
+        entry.theories.map({ case (global, opts, thys) =>
+          (global, session_options ++ opts, thys.map(Path.explode(_))) })
       val files = entry.files.map(Path.explode(_))
       val document_files =
         entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
@@ -179,8 +179,8 @@
         if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
         else pre_selected
 
-      val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
-      (selected, tree1)
+      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
+      (selected, new Session_Tree(graph1))
     }
 
     def topological_order: List[(String, Session_Info)] =
@@ -199,6 +199,7 @@
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val OPTIONS = "options"
+  private val GLOBAL_THEORIES = "global_theories"
   private val THEORIES = "theories"
   private val FILES = "files"
   private val DOCUMENT_FILES = "document_files"
@@ -206,7 +207,7 @@
   lazy val root_syntax =
     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
       (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
-      IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
+      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
 
   object Parser extends Parse.Parser
   {
@@ -226,8 +227,9 @@
       val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
 
       val theories =
-        keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
-          { case _ ~ (x ~ y) => (x, y) }
+        (keyword(GLOBAL_THEORIES) | keyword(THEORIES)) ~!
+          ((options | success(Nil)) ~ rep(theory_xname)) ^^
+          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
 
       val document_files =
         keyword(DOCUMENT_FILES) ~!
@@ -407,6 +409,7 @@
 
   sealed case class Session_Content(
     loaded_theories: Set[String],
+    known_theories: Map[String, Document.Node.Name],
     keywords: Thy_Header.Keywords,
     syntax: Outer_Syntax,
     sources: List[(Path, SHA1.Digest)])
@@ -425,15 +428,14 @@
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
-            val (preloaded, parent_syntax) =
-              info.parent match {
+            val (loaded_theories0, known_theories0, syntax0) =
+              info.parent.map(deps(_)) match {
                 case None =>
-                  (Set.empty[String], Outer_Syntax.init())
-                case Some(parent_name) =>
-                  val parent = deps(parent_name)
-                  (parent.loaded_theories, parent.syntax)
+                  (Set.empty[String], Map.empty[String, Document.Node.Name], Outer_Syntax.init())
+                case Some(parent) =>
+                  (parent.loaded_theories, parent.known_theories, parent.syntax)
               }
-            val resources = new Resources(preloaded, parent_syntax)
+            val resources = new Resources(loaded_theories0, known_theories0, syntax0)
             val thy_info = new Thy_Info(resources)
 
             if (verbose || list_files) {
@@ -444,15 +446,33 @@
             }
 
             val thy_deps =
-              thy_info.dependencies(
-                info.theories.map(_._2).flatten.
-                  map(thy => (resources.node_name(info.dir + Resources.thy_path(thy)), info.pos)))
+            {
+              val root_theories =
+                info.theories.flatMap({
+                  case (global, _, thys) =>
+                    thys.map(thy =>
+                      (resources.node_name(
+                        if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos))
+                })
+              val thy_deps = thy_info.dependencies(name, root_theories)
 
-            thy_deps.errors match {
-              case Nil =>
-              case errs => error(cat_lines(errs))
+              thy_deps.errors match {
+                case Nil => thy_deps
+                case errs => error(cat_lines(errs))
+              }
             }
 
+            val known_theories =
+              (known_theories0 /: thy_deps.deps)({ case (known, dep) =>
+                val name = dep.name
+                known.get(name.theory) match {
+                  case Some(name1) if name != name1 =>
+                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
+                  case _ =>
+                    known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
+                }
+              })
+
             val loaded_theories = thy_deps.loaded_theories
             val keywords = thy_deps.keywords
             val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
@@ -480,7 +500,9 @@
 
             val sources = all_files.map(p => (p, SHA1.digest(p.file)))
 
-            deps + (name -> Session_Content(loaded_theories, keywords, syntax, sources))
+            val content =
+              Session_Content(loaded_theories, known_theories, keywords, syntax, sources)
+            deps + (name -> content)
           }
           catch {
             case ERROR(msg) =>
@@ -528,12 +550,13 @@
       if (is_pure(name)) Options.encode(info.options)
       else
         {
+          val theories = info.theories.map(x => (x._2, x._3))
           import XML.Encode._
               pair(list(properties), pair(bool, pair(Options.encode, pair(bool, pair(Path.encode,
                 pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string,
                   list(pair(Options.encode, list(Path.encode))))))))))))(
               (command_timings, (do_output, (info.options, (verbose, (browser_info,
-                (info.document_files, (parent, (info.chapter, (name, info.theories))))))))))
+                (info.document_files, (parent, (info.chapter, (name, theories))))))))))
         }))
 
     private val env =
diff -r 939e88e79724 -r c83eb2435b27 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Pure/build-jars	Wed Apr 30 22:35:42 2014 +0200
@@ -24,6 +24,7 @@
   General/graph.scala
   General/graphics_file.scala
   General/linear_set.scala
+  General/long_name.scala
   General/multi_map.scala
   General/output.scala
   General/path.scala
diff -r 939e88e79724 -r c83eb2435b27 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -70,7 +70,7 @@
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
         Exn.capture {
-          PIDE.resources.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
+          PIDE.resources.check_thy_text("", node_name, buffer.getSegment(0, buffer.getLength))
         } match {
           case Exn.Res(header) => header
           case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
diff -r 939e88e79724 -r c83eb2435b27 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -82,7 +82,9 @@
   {
     val dirs = session_dirs()
     val name = session_args().last
-    Build.session_content(PIDE.options.value, inlined_files, dirs, name)
+    val content = Build.session_content(PIDE.options.value, inlined_files, dirs, name)
+    content.copy(known_theories =
+      content.known_theories.mapValues(name => name.map(Isabelle_System.jvm_path(_))))
   }
 }
 
diff -r 939e88e79724 -r c83eb2435b27 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -19,8 +19,11 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
-  extends Resources(loaded_theories, base_syntax)
+class JEdit_Resources(
+    loaded_theories: Set[String],
+    known_theories: Map[String, Document.Node.Name],
+    base_syntax: Outer_Syntax)
+  extends Resources(loaded_theories, known_theories, base_syntax)
 {
   /* document node names */
 
diff -r 939e88e79724 -r c83eb2435b27 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Apr 30 15:43:44 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Apr 30 22:35:42 2014 +0200
@@ -35,7 +35,8 @@
   @volatile var startup_notified = false
 
   @volatile var plugin: Plugin = null
-  @volatile var session: Session = new Session(new JEdit_Resources(Set.empty, Outer_Syntax.empty))
+  @volatile var session: Session =
+    new Session(new JEdit_Resources(Set.empty, Map.empty, Outer_Syntax.empty))
 
   def options_changed() { plugin.options_changed() }
   def deps_changed() { plugin.deps_changed() }
@@ -210,7 +211,7 @@
 
           val thy_info = new Thy_Info(PIDE.resources)
           // FIXME avoid I/O in Swing thread!?!
-          val files = thy_info.dependencies(thys).deps.map(_.name.node).
+          val files = thy_info.dependencies("", thys).deps.map(_.name.node).
             filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
 
           if (!files.isEmpty) {
@@ -350,7 +351,8 @@
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
       val content = Isabelle_Logic.session_content(false)
-      val resources = new JEdit_Resources(content.loaded_theories, content.syntax)
+      val resources =
+        new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
 
       PIDE.session = new Session(resources) {
         override def output_delay = PIDE.options.seconds("editor_output_delay")