# HG changeset patch
# User wenzelm
# Date 1278364056 -7200
# Node ID c82cf6e1166966c3b81c81e0e481f0e16baf0f23
# Parent  7f25bf4b4bca3d6ca5188291848167e6968e1f7d
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;

diff -r 7f25bf4b4bca -r c82cf6e11669 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 05 22:26:20 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 05 23:07:36 2010 +0200
@@ -240,7 +240,10 @@
     val _ = List.app Thy_Syntax.report_token toks;
   in
     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
-      [tr] => (tr, true)
+      [tr] =>
+        if Keyword.is_control (Toplevel.name_of tr) then
+          (Toplevel.malformed range_pos "Illegal control command", true)
+        else (tr, true)
     | [] => (Toplevel.ignored range_pos, false)
     | _ => (Toplevel.malformed range_pos not_singleton, true))
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)