--- a/src/Pure/Isar/runtime.ML Tue Feb 26 19:44:26 2013 +0100
+++ b/src/Pure/Isar/runtime.ML Tue Feb 26 19:58:27 2013 +0100
@@ -12,7 +12,8 @@
exception TOPLEVEL_ERROR
val debug: bool Unsynchronized.ref
val exn_context: Proof.context option -> exn -> exn
- val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
+ type error = ((serial * string) * string option)
+ val exn_messages_ids: (exn -> Position.T) -> exn -> error list
val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
val exn_message: (exn -> Position.T) -> exn -> string
val debugging: ('a -> 'b) -> 'a -> 'b
@@ -43,6 +44,8 @@
(* exn_message *)
+type error = ((serial * string) * string option);
+
local
fun if_context NONE _ _ = []
--- a/src/Pure/Isar/toplevel.ML Tue Feb 26 19:44:26 2013 +0100
+++ b/src/Pure/Isar/toplevel.ML Tue Feb 26 19:58:27 2013 +0100
@@ -95,8 +95,7 @@
val put_timing: Time.time -> transition -> transition
val transition: bool -> transition -> state -> (state * (exn * string) option) option
val command_exception: bool -> transition -> state -> state
- val command_errors: bool -> transition -> state ->
- ((serial * string) * string option) list * state option
+ val command_errors: bool -> transition -> state -> Runtime.error list * state option
val element_result: transition Thy_Syntax.element -> state ->
(transition * state) list future * state
end;
--- a/src/Pure/ML/ml_compiler.ML Tue Feb 26 19:44:26 2013 +0100
+++ b/src/Pure/ML/ml_compiler.ML Tue Feb 26 19:58:27 2013 +0100
@@ -7,7 +7,7 @@
signature ML_COMPILER =
sig
val exn_position: exn -> Position.T
- val exn_messages_ids: exn -> ((serial * string) * string option) list
+ val exn_messages_ids: exn -> Runtime.error list
val exn_messages: exn -> (serial * string) list
val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit