--- a/src/Pure/PIDE/command.ML Tue Dec 09 21:14:11 2014 +0100
+++ b/src/Pure/PIDE/command.ML Tue Dec 09 22:13:48 2014 +0100
@@ -162,7 +162,7 @@
SOME tok => Token.pos_of tok
| NONE => #1 proper_range);
- val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
+ val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens keywords span;
val _ = Position.reports_text (token_reports @ maps command_reports span);
in
if is_malformed then Toplevel.malformed pos "Malformed command syntax"