# HG changeset patch
# User wenzelm
# Date 1492078768 -7200
# Node ID a72ae9eb44626be96484556968f936f0868bab93
# Parent  4519c8cc4bececb29697e3459b9046febc15f167
tuned signature (again);

diff -r 4519c8cc4bec -r a72ae9eb4462 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Apr 12 23:44:33 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Apr 13 12:19:28 2017 +0200
@@ -108,7 +108,7 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
-fun loaded_theory_name qualifier theory0 =
+fun theory_name qualifier theory0 =
   (case loaded_theory theory0 of
     SOME theory => (true, theory)
   | NONE =>
@@ -119,7 +119,7 @@
       in (false, theory) end);
 
 fun import_name qualifier dir s =
-  (case loaded_theory_name qualifier (Thy_Header.import_name s) of
+  (case theory_name qualifier (Thy_Header.import_name s) of
     (true, theory) =>
       {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
   | (false, theory) =>
diff -r 4519c8cc4bec -r a72ae9eb4462 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Apr 12 23:44:33 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Apr 13 12:19:28 2017 +0200
@@ -70,7 +70,7 @@
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
-  def loaded_theory_name(qualifier: String, theory0: String): (Boolean, String) =
+  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
     session_base.loaded_theories.get(theory0) match {
       case Some(theory) => (true, theory)
       case None =>
@@ -82,7 +82,7 @@
     }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
-    loaded_theory_name(qualifier, Thy_Header.import_name(s)) match {
+    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 {
diff -r 4519c8cc4bec -r a72ae9eb4462 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 23:44:33 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Apr 13 12:19:28 2017 +0200
@@ -63,7 +63,7 @@
   def node_name(file: JFile): Document.Node.Name =
   {
     val node = file.getPath
-    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+    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
diff -r 4519c8cc4bec -r a72ae9eb4462 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 23:44:33 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Apr 13 12:19:28 2017 +0200
@@ -29,7 +29,7 @@
   {
     val vfs = VFSManager.getVFSForPath(path)
     val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    loaded_theory_name(default_qualifier, Thy_Header.theory_name(node)) match {
+    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)