# HG changeset patch
# User wenzelm
# Date 1361905107 -3600
# Node ID 0859bd338c9bedb915833a0c6a535e03b80a5a63
# Parent  59a03019f3bfe4da6795163ff37e007001b8c58a
tuned signature;

diff -r 59a03019f3bf -r 0859bd338c9b src/Pure/Isar/runtime.ML
--- 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 _ _ = []
diff -r 59a03019f3bf -r 0859bd338c9b src/Pure/Isar/toplevel.ML
--- 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;
diff -r 59a03019f3bf -r 0859bd338c9b src/Pure/ML/ml_compiler.ML
--- 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