--- a/src/Pure/PIDE/command.scala Wed Aug 31 14:39:41 2011 +0200
+++ b/src/Pure/PIDE/command.scala Wed Aug 31 15:41:22 2011 +0200
@@ -80,10 +80,10 @@
/* dummy commands */
def unparsed(source: String): Command =
- new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
+ new Command(Document.no_id, "", List(Token(Token.Kind.UNPARSED, source)))
- def span(toks: List[Token]): Command =
- new Command(Document.no_id, toks)
+ def span(node_name: String, toks: List[Token]): Command =
+ new Command(Document.no_id, node_name, toks)
/* perspective */
@@ -110,6 +110,7 @@
class Command(
val id: Document.Command_ID,
+ val node_name: String,
val span: List[Token])
{
/* classification */