# HG changeset patch
# User wenzelm
# Date 1341495657 -7200
# Node ID c1def7433a72ae4ac0d751628ba89fc90ac0f8ea
# Parent  76b6207eb000a197c169e56d25eb86f1e4a43a50
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;

diff -r 76b6207eb000 -r c1def7433a72 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jul 05 14:13:14 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jul 05 15:40:57 2012 +0200
@@ -69,7 +69,9 @@
   (case cmd name of
     SOME (Command {int_only, parse, ...}) =>
       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
-  | NONE => raise Fail ("No parser for outer syntax command " ^ quote name));
+  | NONE =>
+      Scan.succeed (false, Toplevel.imperative (fn () =>
+        error ("Bad parser for outer syntax command " ^ quote name))));
 
 in