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.
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
authorwenzelm
Thu, 05 Jul 2012 15:40:57 +0200
changeset 48191 c1def7433a72
parent 48190 76b6207eb000
child 48192 07a32140ce0d
internalize error into command transaction -- relevant for commands that are declared via 'keywords', but not defined yet;
src/Pure/Isar/outer_syntax.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle