--- 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 *)