# HG changeset patch
# User wenzelm
# Date 1429091249 -7200
# Node ID 76a8400a58d9ed57192612c5a4e62f039ffec125
# Parent  dda1e781c7b48fc752080a79035b4eb185eb59a5
more robust error handling of commands that are declared but not yet defined;

diff -r dda1e781c7b4 -r 76a8400a58d9 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Apr 14 22:54:07 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Apr 15 11:47:29 2015 +0200
@@ -177,22 +177,18 @@
       | SOME (Command {command_parser = Limited_Parser parse, ...}) =>
           before_command :|-- (fn limited =>
             Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
-      | NONE =>
-          Scan.succeed
-            (tr0 |> Toplevel.imperative (fn () => err_command "Undefined command " name [pos])))
+      | NONE => Scan.fail_with (fn _ => fn _ => err_command "Undefined command " name [pos]))
     end);
 
 val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
 
-in
-
 fun commands_source thy =
   Token.source_proper #>
   Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #>
   Source.map_filter I #>
   Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs));
 
-end;
+in
 
 fun parse thy pos str =
   Source.of_string str
@@ -206,6 +202,8 @@
   |> commands_source thy
   |> Source.exhaust;
 
+end;
+
 
 (* parse spans *)