# HG changeset patch
# User wenzelm
# Date 1316293443 -7200
# Node ID 9476c856c4b945cc965425f8720c2c4b9c869cf4
# Parent  86e4916825ee0f7b6bbcb6bafb52dc48c4d13367
Document.Node.Name convenience;

diff -r 86e4916825ee -r 9476c856c4b9 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Sep 17 22:13:15 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Sep 17 23:04:03 2011 +0200
@@ -80,7 +80,7 @@
   /* dummy commands */
 
   def unparsed(source: String): Command =
-    new Command(Document.no_id, Document.Node.Name("", "", ""),
+    new Command(Document.no_id, Document.Node.Name.empty,
       List(Token(Token.Kind.UNPARSED, source)))
 
   def span(node_name: Document.Node.Name, toks: List[Token]): Command =
diff -r 86e4916825ee -r 9476c856c4b9 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)
     {