diff -r 226fb165833e -r 21be4832c362 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon May 17 10:20:55 2010 +0200 +++ b/src/Pure/PIDE/document.scala Mon May 17 14:23:54 2010 +0200 @@ -46,7 +46,7 @@ /* unparsed dummy commands */ def unparsed(source: String) = - new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source))) + new Command(null, List(Token(Token.Kind.UNPARSED, source))) def is_unparsed(command: Command) = command.id == null