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 =