tuned signature;
authorwenzelm
Tue Feb 26 19:58:27 2013 +0100 (2013-02-26 ago)
changeset 512850859bd338c9b
parent 51284 59a03019f3bf
child 51286 44a521ff87cf
tuned signature;
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_compiler.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Tue Feb 26 19:44:26 2013 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Tue Feb 26 19:58:27 2013 +0100
     1.3 @@ -12,7 +12,8 @@
     1.4    exception TOPLEVEL_ERROR
     1.5    val debug: bool Unsynchronized.ref
     1.6    val exn_context: Proof.context option -> exn -> exn
     1.7 -  val exn_messages_ids: (exn -> Position.T) -> exn -> ((serial * string) * string option) list
     1.8 +  type error = ((serial * string) * string option)
     1.9 +  val exn_messages_ids: (exn -> Position.T) -> exn -> error list
    1.10    val exn_messages: (exn -> Position.T) -> exn -> (serial * string) list
    1.11    val exn_message: (exn -> Position.T) -> exn -> string
    1.12    val debugging: ('a -> 'b) -> 'a -> 'b
    1.13 @@ -43,6 +44,8 @@
    1.14  
    1.15  (* exn_message *)
    1.16  
    1.17 +type error = ((serial * string) * string option);
    1.18 +
    1.19  local
    1.20  
    1.21  fun if_context NONE _ _ = []
     2.1 --- a/src/Pure/Isar/toplevel.ML	Tue Feb 26 19:44:26 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Feb 26 19:58:27 2013 +0100
     2.3 @@ -95,8 +95,7 @@
     2.4    val put_timing: Time.time -> transition -> transition
     2.5    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     2.6    val command_exception: bool -> transition -> state -> state
     2.7 -  val command_errors: bool -> transition -> state ->
     2.8 -    ((serial * string) * string option) list * state option
     2.9 +  val command_errors: bool -> transition -> state -> Runtime.error list * state option
    2.10    val element_result: transition Thy_Syntax.element -> state ->
    2.11      (transition * state) list future * state
    2.12  end;
     3.1 --- a/src/Pure/ML/ml_compiler.ML	Tue Feb 26 19:44:26 2013 +0100
     3.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Feb 26 19:58:27 2013 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  signature ML_COMPILER =
     3.5  sig
     3.6    val exn_position: exn -> Position.T
     3.7 -  val exn_messages_ids: exn -> ((serial * string) * string option) list
     3.8 +  val exn_messages_ids: exn -> Runtime.error list
     3.9    val exn_messages: exn -> (serial * string) list
    3.10    val exn_message: exn -> string
    3.11    val eval: bool -> Position.T -> ML_Lex.token list -> unit