# HG changeset patch
# User wenzelm
# Date 1492693232 -7200
# Node ID 0910f1733909ddbae4757495659977048a4d318d
# Parent  4f2954adc2174774c26142d8350f6b5a1281a93d
tuned signature;

diff -r 4f2954adc217 -r 0910f1733909 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 20 14:59:57 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 20 15:00:32 2017 +0200
@@ -81,6 +81,9 @@
       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(_)))))
+
+    def get_file(file: JFile): Option[Document.Node.Name] =
+      files.getOrElse(file.getCanonicalFile, Nil).headOption
   }
 
   object Base
@@ -111,9 +114,6 @@
     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)
         yield (theory, node_name.node)
diff -r 4f2954adc217 -r 0910f1733909 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 20 14:59:57 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 20 15:00:32 2017 +0200
@@ -61,7 +61,7 @@
   def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
 
   def node_name(file: JFile): Document.Node.Name =
-    session_base.known_file(file) getOrElse {
+    session_base.known.get_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)
diff -r 4f2954adc217 -r 0910f1733909 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 14:59:57 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 20 15:00:32 2017 +0200
@@ -26,7 +26,7 @@
   /* document node name */
 
   def known_file(path: String): Option[Document.Node.Name] =
-    JEdit_Lib.check_file(path).flatMap(session_base.known_file(_))
+    JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
 
   def node_name(path: String): Document.Node.Name =
     known_file(path) getOrElse {