--- a/src/Pure/PIDE/command.ML Fri Oct 31 21:35:11 2014 +0100
+++ b/src/Pure/PIDE/command.ML Fri Oct 31 21:48:40 2014 +0100
@@ -162,10 +162,7 @@
if is_malformed then Toplevel.malformed pos "Malformed command syntax"
else
(case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
- [tr] =>
- if Keyword.is_control (Toplevel.name_of tr) then
- Toplevel.malformed pos "Illegal control command"
- else Toplevel.modify_init init tr
+ [tr] => Toplevel.modify_init init tr
| [] => Toplevel.ignored (#1 (Token.range_of span))
| _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
handle ERROR msg => Toplevel.malformed (#1 proper_range) msg