Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
authorwenzelm
Mon, 05 Jul 2010 23:07:36 +0200
changeset 37713 c82cf6e11669
parent 37712 7f25bf4b4bca
child 37727 8244558af8a5
Outer_Syntax.prepare_command: disallow control commands here, and consequently in Isar documents;
src/Pure/Isar/outer_syntax.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle