# HG changeset patch
# User wenzelm
# Date 1492458656 -7200
# Node ID c05bec5d01ad6660f7825f6a8315f9aa350a7a67
# Parent  d801126a14cb510f8c5ff435685b3bf5abe662eb# Parent  b42743f5b5951ee7628c58b3700314de09954d07
merged

diff -r d801126a14cb -r c05bec5d01ad src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Apr 17 21:50:56 2017 +0200
@@ -101,16 +101,15 @@
   for syntactic completion. The default for a new keyword is just its name,
   but completion may be avoided by defining @{keyword "abbrevs"} with empty
   text.
-  
+
   \<^descr> @{command (global) "end"} concludes the current theory definition. Note
   that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
   may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "end"},
   according to the usual rules for nested blocks.
 
   \<^descr> \<^theory_text>\<open>thy_deps\<close> visualizes the theory hierarchy as a directed acyclic graph.
-  By default, all imported theories are shown, taking the base session as a
-  starting point. Alternatively, it is possibly to restrict the full theory
-  graph by giving bounds, analogously to @{command_ref class_deps}.
+  By default, all imported theories are shown. This may be restricted by
+  specifying bounds wrt. the theory inclusion relation.
 \<close>
 
 
@@ -157,11 +156,11 @@
   means any results stemming from definitions and proofs in the extended
   context will be exported into the enclosing target by lifting over extra
   parameters and premises.
-  
+
   \<^descr> @{command (local) "end"} concludes the current local theory, according to
   the nesting of contexts. Note that a global @{command (global) "end"} has a
   different meaning: it concludes the theory itself (\secref{sec:begin-thy}).
-  
+
   \<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be given as modifiers before any local
   theory command. This restricts name space accesses to the local scope, as
   determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outside its scope,
@@ -189,7 +188,7 @@
   on the underlying target infrastructure (locale, type class etc.). The
   general idea is as follows, considering a context named \<open>c\<close> with parameter
   \<open>x\<close> and assumption \<open>A[x]\<close>.
-  
+
   Definitions are exported by introducing a global version with additional
   arguments; a syntactic abbreviation links the long form with the abstract
   version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
@@ -321,7 +320,7 @@
   object-logic. This usually covers object-level equality \<open>x = y\<close> and
   equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{attribute
   defn} setup.
-  
+
   Definitions may be presented with explicit arguments on the LHS, as well as
   additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0
   \<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.
@@ -331,18 +330,18 @@
 
   \<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant which is
   associated with a certain term according to the meta-level equality \<open>eq\<close>.
-  
+
   Abbreviations participate in the usual type-inference process, but are
   expanded before the logic ever sees them. Pretty printing of terms involves
   higher-order rewriting with rules stemming from reverted abbreviations. This
   needs some care to avoid overlapping or looping syntactic replacements!
-  
+
   The optional \<open>mode\<close> specification restricts output to a particular print
   mode; using ``\<open>input\<close>'' here achieves the effect of one-way abbreviations.
   The mode may also include an ``\<^theory_text>\<open>output\<close>'' qualifier that affects the
   concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in
   \secref{sec:syn-trans}.
-  
+
   \<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the current context;
   the ``\<open>!\<close>'' option indicates extra verbosity.
 \<close>
@@ -574,12 +573,12 @@
   the locale specification. When defining an operation derived from the
   parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more
   appropriate.
-  
+
   Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element
   "assumes"} and @{element "defines"} above are illegal in locale definitions.
   In the long goal format of \secref{sec:goals}, term bindings may be included
   as expected, though.
-  
+
   \<^medskip>
   Locale specifications are ``closed up'' by turning the given text into a
   predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as
@@ -587,7 +586,7 @@
   the newly specified assumptions, omitting the content of included locale
   expressions. The full cumulative view is only provided on export, involving
   another predicate \<open>loc\<close> that refers to the complete specification text.
-  
+
   In any case, the predicate arguments are those locale parameters that
   actually occur in the respective piece of text. Also these predicates
   operate at the meta-level in theory, but the locale packages attempts to
@@ -1111,7 +1110,7 @@
   \<^descr> \<^theory_text>\<open>ML_val\<close> and \<^theory_text>\<open>ML_command\<close> are diagnostic versions of \<^theory_text>\<open>ML\<close>, which means
   that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced
   at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent.
-  
+
   \<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>,
   which refers to an ML expression of type @{ML_type "theory -> theory"}. This
   enables to initialize any object-logic specific tools and packages written
@@ -1223,7 +1222,7 @@
   \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in
   Isabelle/HOL, type synonyms are merely syntactic abbreviations without any
   logical significance. Internally, type synonyms are fully expanded.
-  
+
   \<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the
   object-logic defines a base sort \<open>s\<close>, then the constructor is declared to
   operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.
diff -r d801126a14cb -r c05bec5d01ad src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -451,8 +451,7 @@
         val blobs =
           files.map(file =>
             (Exn.capture {
-              val name =
-                Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+              val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
               val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
               (name, blob)
             }).user_error)
diff -r d801126a14cb -r c05bec5d01ad src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -423,6 +423,9 @@
       rev_infos.filter(p => p._1 == important).reverse.map(_._2)
   }
 
+  def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
+    if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
+
   def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
   {
     val results =
@@ -448,7 +451,7 @@
             Some(info + (r0, true, XML.Text(txt1 + txt2)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
-            val file = session.resources.append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             val text =
               if (name == file) "file " + quote(file)
               else "path " + quote(name) + "\nfile " + quote(file)
diff -r d801126a14cb -r c05bec5d01ad src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Mon Apr 17 21:50:56 2017 +0200
@@ -254,7 +254,7 @@
           warning ("Cannot present theory with skipped proofs: " ^ quote name)
         else
           let val tex_source = Thy_Output.present_thy thy res toks |> Buffer.content;
-          in if document then Present.theory_output name tex_source else () end
+          in if document then Present.theory_output (Long_Name.base_name name) tex_source else () end
       end;
 
   in (thy, present, size text) end;
diff -r d801126a14cb -r c05bec5d01ad src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -28,10 +28,8 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
-  def append_file(dir: String, raw_name: String): String =
-    if (Path.is_valid(raw_name)) append(dir, Path.explode(raw_name))
-    else raw_name
-
+  def append(node_name: Document.Node.Name, source_path: Path): String =
+    append(node_name.master_dir, source_path)
 
 
   /* source files of Isabelle/ML bootstrap */
@@ -85,7 +83,7 @@
     theory_name(qualifier, Thy_Header.import_name(s)) match {
       case (true, theory) => Document.Node.Name.loaded_theory(theory)
       case (false, theory) =>
-        session_base.known_theories.get(theory) match {
+        session_base.known_theory(theory) match {
           case Some(node_name) => node_name
           case None =>
             val path = Path.explode(s)
@@ -95,11 +93,12 @@
         }
     }
 
+  def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
+    import_name(theory_qualifier(node_name), node_name.master_dir, s)
+
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
-    val path = Path.explode(name.node)
-    if (!path.is_file) error("No such file: " + path.toString)
-
+    val path = File.check_file(Path.explode(name.node))
     val reader = Scan.byte_reader(path.file)
     try { f(reader) } finally { reader.close }
   }
@@ -118,9 +117,7 @@
             " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
-        val imports =
-          header.imports.map({ case (s, pos) =>
-            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
+        val imports = 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)) }
@@ -137,16 +134,10 @@
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   {
-    val qualifier = theory_qualifier(name)
-    val dir = name.master_dir
-
     val imports =
-      if (Thy_Header.is_ml_root(name.theory))
-        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
-      else if (Thy_Header.is_bootstrap(name.theory))
-        List(import_name(qualifier, dir, Thy_Header.PURE))
+      if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
+      else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
       else Nil
-
     if (imports.isEmpty) None
     else Some(Document.Node.Header(imports.map((_, Position.none))))
   }
diff -r d801126a14cb -r c05bec5d01ad src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Thy/present.ML	Mon Apr 17 21:50:56 2017 +0200
@@ -7,7 +7,6 @@
 signature PRESENT =
 sig
   val session_name: theory -> string
-  val session_graph: string -> (string -> bool) -> theory -> Graph_Display.entry list
   val document_enabled: string -> bool
   val document_variants: string -> (string * string) list
   val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -55,28 +54,6 @@
 val session_name = #name o Browser_Info.get;
 
 
-(* session graph *)
-
-fun session_graph parent_session parent_loaded =
-  let
-    val parent_session_name = "session." ^ parent_session;
-    val parent_session_node = Graph_Display.content_node ("[" ^ parent_session ^ "]") [];
-    fun node_name name = if parent_loaded name then parent_session_name else "theory." ^ name;
-    fun theory_entry thy =
-      let
-        val name = Context.theory_name thy;
-        val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
-      in
-        if parent_loaded (Context.theory_long_name thy) then NONE
-        else SOME ((node_name name, Graph_Display.content_node name []), deps)
-      end;
-  in
-    fn thy =>
-      ((parent_session_name, parent_session_node), []) ::
-        map_filter theory_entry (Theory.nodes_of thy)
-  end;
-
-
 
 (** global browser info state **)
 
diff -r d801126a14cb -r c05bec5d01ad src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -24,30 +24,16 @@
 
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
-  sealed case class Known_Theories(
-    known_theories: Map[String, Document.Node.Name] = Map.empty,
-    known_theories_local: Map[String, Document.Node.Name] = Map.empty,
-    known_files: Map[JFile, List[Document.Node.Name]] = Map.empty)
-
-  object Base
+  object Known
   {
-    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+    val empty: Known = Known()
 
-    def bootstrap(global_theories: Map[String, String]): Base =
-      Base(
-        global_theories = global_theories,
-        keywords = Thy_Header.bootstrap_header,
-        syntax = Thy_Header.bootstrap_syntax)
-
-    private[Sessions] def known_theories(
-        local_dir: Path,
-        bases: List[Base],
-        theories: List[Document.Node.Name]): Known_Theories =
+    def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
     {
       def bases_iterator(local: Boolean) =
         for {
           base <- bases.iterator
-          (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator
+          (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
         } yield name
 
       def local_theories_iterator =
@@ -81,42 +67,59 @@
               known
             else known + (file -> (name :: theories1))
         })
-      Known_Theories(known_theories, known_theories_local,
+      Known(known_theories, known_theories_local,
         known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
     }
   }
 
+  sealed case class Known(
+    theories: Map[String, Document.Node.Name] = Map.empty,
+    theories_local: Map[String, Document.Node.Name] = Map.empty,
+    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
+  {
+    def platform_path: Known =
+      copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
+        theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
+        files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+  }
+
+  object Base
+  {
+    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+
+    def bootstrap(global_theories: Map[String, String]): Base =
+      Base(
+        global_theories = global_theories,
+        keywords = Thy_Header.bootstrap_header,
+        syntax = Thy_Header.bootstrap_syntax)
+  }
+
   sealed case class Base(
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Map[String, String] = Map.empty,
-    known_theories: Map[String, Document.Node.Name] = Map.empty,
-    known_theories_local: Map[String, Document.Node.Name] = Map.empty,
-    known_files: Map[JFile, List[Document.Node.Name]] = Map.empty,
+    known: Known = Known.empty,
     keywords: Thy_Header.Keywords = Nil,
     syntax: Outer_Syntax = Outer_Syntax.empty,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
   {
-    def platform_path: Base =
-      copy(
-        known_theories =
-          for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
-        known_theories_local =
-          for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))),
-        known_files =
-          for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+    def platform_path: Base = copy(known = known.platform_path)
 
     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)
 
+    def known_theory(name: String): Option[Document.Node.Name] =
+      known.theories.get(name)
+
+    def known_file(file: JFile): Option[Document.Node.Name] =
+      known.files.getOrElse(file.getCanonicalFile, Nil).headOption
+
     def dest_known_theories: List[(String, String)] =
-      for ((theory, node_name) <- known_theories.toList)
+      for ((theory, node_name) <- known.theories.toList)
         yield (theory, node_name.node)
   }
 
-  sealed case class Deps(
-    session_bases: Map[String, Base],
-    all_known_theories: Known_Theories)
+  sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
   {
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
@@ -130,7 +133,7 @@
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty,
       global_theories: Map[String, String] = Map.empty,
-      all_known_theories: Boolean = false): Deps =
+      all_known: Boolean = false): Deps =
   {
     val session_bases =
       (Map.empty[String, Base] /: sessions.imports_topological_order)({
@@ -138,12 +141,16 @@
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
-            val parent_base =
+            val parent_base: Sessions.Base =
               info.parent match {
                 case None => Base.bootstrap(global_theories)
                 case Some(parent) => session_bases(parent)
               }
-            val resources = new Resources(parent_base,
+            val imports_base: Sessions.Base =
+              parent_base.copy(known =
+                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
+
+            val resources = new Resources(imports_base,
               default_qualifier = info.theory_qualifier(session_name))
 
             if (verbose || list_files) {
@@ -168,11 +175,6 @@
               }
             }
 
-            val known_theories =
-              Base.known_theories(info.dir,
-                parent_base :: info.imports.map(session_bases(_)),
-                thy_deps.deps.map(_.name))
-
             val syntax = thy_deps.syntax
 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
@@ -205,13 +207,11 @@
             val base =
               Base(global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
-                known_theories = known_theories.known_theories,
-                known_theories_local = known_theories.known_theories_local,
-                known_files = known_theories.known_files,
+                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
                 keywords = thy_deps.keywords,
                 syntax = syntax,
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
-                session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
+                session_graph = thy_deps.session_graph(info.parent getOrElse "", imports_base))
 
             session_bases + (session_name -> base)
           }
@@ -222,31 +222,25 @@
           }
       })
 
-    val known_theories =
-      if (all_known_theories)
-        Base.known_theories(Path.current, session_bases.toList.map(_._2), Nil)
-      else Known_Theories()
-
-    Deps(session_bases, known_theories)
+    Deps(session_bases,
+      if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
+      else Known.empty)
   }
 
   def session_base(
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
-    all_known_theories: Boolean = false): Base =
+    all_known: Boolean = false): Base =
   {
     val full_sessions = load(options, dirs = dirs)
     val global_theories = full_sessions.global_theories
     val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
 
-    if (all_known_theories) {
+    if (all_known) {
       val deps = Sessions.deps(
-        full_sessions, global_theories = global_theories, all_known_theories = all_known_theories)
-      deps(session).copy(
-        known_theories = deps.all_known_theories.known_theories,
-        known_theories_local = deps.all_known_theories.known_theories_local,
-        known_files = deps.all_known_theories.known_files)
+        full_sessions, global_theories = global_theories, all_known = all_known)
+      deps(session).copy(known = deps.all_known)
     }
     else
       deps(selected_sessions, global_theories = global_theories)(session)
@@ -387,7 +381,7 @@
       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
     def global_theories: Map[String, String] =
-      (Map.empty[String, String] /:
+      (Thy_Header.bootstrap_global_theories.toMap /:
         (for {
           (session_name, (info, _)) <- imports_graph.iterator
           thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
diff -r d801126a14cb -r c05bec5d01ad src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -73,10 +73,11 @@
 
   val PURE = "Pure"
   val ML_BOOTSTRAP = "ML_Bootstrap"
-  val ML_ROOT = "ML_Root"
-  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
+  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
+  val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
+
   private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
   private val Import_Name = new Regex(""".*?([^/\\:]+)""")
 
diff -r d801126a14cb -r c05bec5d01ad src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Pure/Tools/thy_deps.ML	Mon Apr 17 21:50:56 2017 +0200
@@ -6,7 +6,8 @@
 
 signature THY_DEPS =
 sig
-  val thy_deps: Proof.context -> theory list option * theory list option -> Graph_Display.entry list
+  val thy_deps: Proof.context -> theory list option * theory list option ->
+    Graph_Display.entry list
   val thy_deps_cmd: Proof.context ->
     (string * Position.T) list option * (string * Position.T) list option -> unit
 end;
@@ -14,26 +15,21 @@
 structure Thy_Deps: THY_DEPS =
 struct
 
-fun gen_thy_deps _ ctxt (NONE, NONE) =
-      let
-        val parent_session = Session.get_name ();
-        val parent_loaded = is_some o Thy_Info.lookup_theory;
-      in Present.session_graph parent_session parent_loaded (Proof_Context.theory_of ctxt) end
-  | gen_thy_deps prep_thy ctxt bounds =
-      let
-        val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
-        val rel = Context.subthy o swap;
-        val pred =
-          (case upper of
-            SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
-          | NONE => K true) andf
-          (case lower of
-            SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
-          | NONE => K true);
-        fun node thy =
-          ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
-            map Context.theory_name (filter pred (Theory.parents_of thy)));
-      in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
+fun gen_thy_deps prep_thy ctxt bounds =
+  let
+    val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
+    val rel = Context.subthy o swap;
+    val pred =
+      (case upper of
+        SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
+      | NONE => K true) andf
+      (case lower of
+        SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
+      | NONE => K true);
+    fun node thy =
+      ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
+        map Context.theory_name (filter pred (Theory.parents_of thy)));
+  in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
 
 val thy_deps =
   gen_thy_deps (fn ctxt => fn thy =>
diff -r d801126a14cb -r c05bec5d01ad src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -237,7 +237,7 @@
       range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
-            val file = model.resources.append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             Some(Line.Node_Range(file) :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
diff -r d801126a14cb -r c05bec5d01ad src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -61,15 +61,15 @@
   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
 
   def node_name(file: JFile): Document.Node.Name =
-  {
-    val node = file.getPath
-    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
-      case (true, theory) => Document.Node.Name.loaded_theory(theory)
-      case (false, theory) =>
-        val master_dir = if (theory == "") "" else file.getParent
-        Document.Node.Name(node, master_dir, theory)
+    session_base.known_file(file) getOrElse {
+      val node = file.getPath
+      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+        case (true, theory) => Document.Node.Name.loaded_theory(theory)
+        case (false, theory) =>
+          val master_dir = if (theory == "") "" else file.getParent
+          Document.Node.Name(node, master_dir, theory)
+      }
     }
-  }
 
   override def append(dir: String, source_path: Path): String =
   {
diff -r d801126a14cb -r c05bec5d01ad src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -195,8 +195,7 @@
             if (text == "" || text.endsWith("/")) (path, "")
             else (path.dir, path.base.implode)
 
-          val directory =
-            new JFile(PIDE.resources.append(rendering.snapshot.node_name.master_dir, dir))
+          val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
           val files = directory.listFiles
           if (files == null) Nil
           else {
diff -r d801126a14cb -r c05bec5d01ad src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -304,7 +304,7 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val file = PIDE.resources.append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             val link = JEdit_Editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
diff -r d801126a14cb -r c05bec5d01ad src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -25,17 +25,20 @@
 {
   /* document node name */
 
+  def known_file(path: String): Option[Document.Node.Name] =
+    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
+
   def node_name(path: String): Document.Node.Name =
-  {
-    val vfs = VFSManager.getVFSForPath(path)
-    val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
-      case (true, theory) => Document.Node.Name.loaded_theory(theory)
-      case (false, theory) =>
-        val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
-        Document.Node.Name(node, master_dir, theory)
+    known_file(path) getOrElse {
+      val vfs = VFSManager.getVFSForPath(path)
+      val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
+      theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+        case (true, theory) => Document.Node.Name.loaded_theory(theory)
+        case (false, theory) =>
+          val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
+          Document.Node.Name(node, master_dir, theory)
+      }
     }
-  }
 
   def node_name(buffer: Buffer): Document.Node.Name =
     node_name(JEdit_Lib.buffer_name(buffer))
diff -r d801126a14cb -r c05bec5d01ad src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 17 16:39:01 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Apr 17 21:50:56 2017 +0200
@@ -172,7 +172,7 @@
       val component = Node_Renderer_Component
       component.node_name = name
       component.checkbox.selected = nodes_required.contains(name)
-      component.label.text = name.theory
+      component.label.text = name.theory_base_name
       component
     }
   }