# HG changeset patch
# User wenzelm
# Date 1218485209 -7200
# Node ID 20aea331137fb6d7dcfe89207c9f53ab6ef3dbd1
# Parent  68de2a2780b335910c2a04dbcc94b11f4b51da65
Isar.command: OuterSyntax.prepare_command_failsafe defers syntax errors until execution time;

diff -r 68de2a2780b3 -r 20aea331137f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 11 20:56:32 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 11 22:06:49 2008 +0200
@@ -723,7 +723,7 @@
   OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
     (props_text >> (fn (pos, str) =>
       Toplevel.no_timing o Toplevel.imperative (fn () =>
-        ignore (Isar.create_command (OuterSyntax.prepare_command pos str)))));
+        ignore (Isar.create_command (OuterSyntax.prepare_command_failsafe pos str)))));
 
 val _ =
   OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control
diff -r 68de2a2780b3 -r 20aea331137f src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 11 20:56:32 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 11 22:06:49 2008 +0200
@@ -25,6 +25,7 @@
   val scan: string -> OuterLex.token list
   val parse: Position.T -> string -> Toplevel.transition list
   val prepare_command: Position.T -> string -> Toplevel.transition
+  val prepare_command_failsafe: Position.T -> string -> Toplevel.transition
   val process_file: Path.T -> theory -> theory
   type isar
   val isar: bool -> isar
@@ -201,6 +202,11 @@
     [transition] => transition
   | _ => error "exactly one command expected");
 
+fun prepare_command_failsafe pos str = prepare_command pos str
+  handle ERROR msg =>
+    Toplevel.empty |> Toplevel.name "<malformed>" |> Toplevel.position pos
+    |> Toplevel.imperative (fn () => error msg);
+
 
 (* process file *)