changeset 44959 | 9476c856c4b9 |
parent 44615 | a4ff8a787202 |
child 45455 | 4f974c0c5c2f |
--- 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 =