src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sat Sep 17 22:13:15 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Sep 17 23:04:03 2011 +0200
@@ -42,6 +42,13 @@
     object Name
     {
       val empty = Name("", "", "")
+      def apply(path: Path): Name =
+      {
+        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)
+      }
     }
     sealed case class Name(node: String, dir: String, theory: String)
     {