tuned signature -- avoid intrusion of module Path in generic PIDE concepts;

--- a/src/Pure/PIDE/document.scala	Sun Nov 25 20:17:04 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Nov 25 20:31:49 2012 +0100
@@ -51,14 +51,6 @@
     object Name
     {
       val empty = Name("", "", "")
-      def apply(raw_path: Path): Name =
-      {
-        val path = raw_path.expand
-        val node = path.implode
-        val dir = path.dir.implode
-        val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
-        Name(node, dir, theory)
-      }
 
       object Ordering extends scala.math.Ordering[Name]
       {

--- a/src/Pure/System/build.scala	Sun Nov 25 20:17:04 2012 +0100
+++ b/src/Pure/System/build.scala	Sun Nov 25 20:31:49 2012 +0100
@@ -358,7 +358,7 @@
           val thy_deps =
             thy_info.dependencies(inlined_files,
               info.theories.map(_._2).flatten.
-                map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
+                map(thy => Thy_Load.external_node(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = thy_deps.loaded_theories
           val syntax = thy_deps.make_syntax

--- a/src/Pure/Thy/thy_load.scala	Sun Nov 25 20:17:04 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Sun Nov 25 20:31:49 2012 +0100
@@ -14,11 +14,25 @@
 
 object Thy_Load
 {
+  /* paths */
+
   def thy_path(path: Path): Path = path.ext("thy")
 
   def is_ok(str: String): Boolean =
     try { thy_path(Path.explode(str)); true }
     catch { case ERROR(_) => false }
+
+
+  /* node names */
+
+  def external_node(raw_path: Path): Document.Node.Name =
+  {
+    val path = raw_path.expand
+    val node = path.implode
+    val dir = path.dir.implode
+    val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
+    Document.Node.Name(node, dir, theory)
+  }
 }