# HG changeset patch
# User wenzelm
# Date 1489568907 -3600
# Node ID 13a6c81534a85eab6bf0282cc42c9ae17b5a94a7
# Parent  c3ee88b9c3cbb7a5f8aef30b0048e2276035dedc
tuned signature;

diff -r c3ee88b9c3cb -r 13a6c81534a8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Mar 14 23:25:53 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Wed Mar 15 10:08:27 2017 +0100
@@ -15,8 +15,6 @@
 
 object Resources
 {
-  def thy_path(path: Path): Path = path.ext("thy")
-
   val empty: Resources = new Resources(Sessions.Base.empty)
 }
 
@@ -24,6 +22,8 @@
 {
   val thy_info = new Thy_Info(this)
 
+  def thy_path(path: Path): Path = path.ext("thy")
+
 
   /* document node names */
 
@@ -100,7 +100,7 @@
         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 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(no_qualifier, theory))
         }
@@ -128,7 +128,7 @@
         val (name, pos) = header.name
         if (base_name != name)
           error("Bad theory name " + quote(name) +
-            " for file " + Resources.thy_path(Path.basic(base_name)) + Position.here(pos) +
+            " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
diff -r c3ee88b9c3cb -r 13a6c81534a8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 14 23:25:53 2017 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 15 10:08:27 2017 +0100
@@ -135,7 +135,7 @@
                   case (global, _, thys) =>
                     thys.map(thy =>
                       (resources.node_name(
-                        if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos))
+                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
                 })
               val thy_deps = resources.thy_info.dependencies(name, root_theories)