ANTIQUOTE_FAIL;

--- a/src/Pure/Isar/antiquote.ML	Tue Feb 12 20:33:37 2002 +0100
+++ b/src/Pure/Isar/antiquote.ML	Tue Feb 12 20:34:02 2002 +0100
@@ -8,6 +8,7 @@
 
 signature ANTIQUOTE =
 sig
+  exception ANTIQUOTE_FAIL of (string * Position.T) * exn
   datatype antiquote = Text of string | Antiq of string * Position.T
   val is_antiq: antiquote -> bool
   val antiquotes_of: string * Position.T -> antiquote list
@@ -18,6 +19,8 @@
 
 (* datatype antiquote *)
 
+exception ANTIQUOTE_FAIL of (string * Position.T) * exn;
+
 datatype antiquote =
   Text of string |
   Antiq of string * Position.T;

--- a/src/Pure/Isar/isar_output.ML	Tue Feb 12 20:33:37 2002 +0100
+++ b/src/Pure/Isar/isar_output.ML	Tue Feb 12 20:34:02 2002 +0100
@@ -63,7 +63,7 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_commands, name) of
       None => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | Some f => transform_failure (curry Comment.OUTPUT_FAIL (name, pos)) (f src))
+    | Some f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
   end;
 
 fun option (name, s) f () =

--- a/src/Pure/Isar/toplevel.ML	Tue Feb 12 20:33:37 2002 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Feb 12 20:34:02 2002 +0100
@@ -385,7 +385,7 @@
   | exn_message (ProofHistory.FAIL msg) = msg
   | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info
   | exn_message (Method.METHOD_FAIL info) = fail_message "method" info
-  | exn_message (Comment.OUTPUT_FAIL info) = fail_message "antiquotation" info
+  | exn_message (Antiquote.ANTIQUOTE_FAIL info) = fail_message "antiquotation" info
   | exn_message (Syntax.AST (msg, _)) = raised_msg "AST" msg
   | exn_message (TYPE (msg, _, _)) = raised_msg "TYPE" msg
   | exn_message (TERM (msg, _)) = raised_msg "TERM" msg
@@ -471,9 +471,9 @@
 
 type isar =
   (transition, (transition option,
-    (OuterLex.token, (OuterLex.token,
+    (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
       Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
-          Source.source) Source.source) Source.source) Source.source;
+          Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
 
 
 (* apply transformers to global state *)