src/prekernel/Feedback.sig

3     type error_record = {origin_structure : string,
4                          origin_function  : string,
5                          message          : string}
8     val mk_HOL_ERR        : string -> string -> string -> exn
9     val mk_HOL_ERRloc     : string -> string -> locn.locn -> string -> exn
10     val wrap_exn          : string -> string -> exn -> exn
11     val wrap_exn_loc      : string -> string -> locn.locn -> exn -> exn
18     val ERR_outstream     : (string -> unit) ref
19     val MESG_outstream    : (string -> unit) ref
20     val WARNING_outstream : (string -> unit) ref
22     val format_ERR        : error_record -> string
23     val format_MESG       : string -> string
24     val format_WARNING    : string -> string -> string -> string
29     val ERR_to_string     : (error_record -> string) ref
30     val MESG_to_string    : (string -> string) ref
31     val WARNING_to_string : (string -> string -> string -> string) ref
32     val exn_to_string     : exn -> string
36     val failwith          : string -> 'a
37     val HOL_MESG          : string -> unit
38     val HOL_PROGRESS_MESG : string * string -> ('a -> 'b) -> 'a -> 'b
39     val HOL_WARNING       : string -> string -> string -> unit
40     val HOL_WARNINGloc    : string -> string -> locn.locn -> string -> unit
42     val traces            : unit -> {name:string, max : int,
43                                      aliases : string list,
45     val register_trace    : (string * int ref * int) -> unit
46     val register_alias_trace : {original:string,alias:string} -> unit
47     val register_ftrace   : (string * ((unit -> int) * (int -> unit)) * int)
49     val register_btrace   : (string * bool ref) -> unit
51     val current_trace     : string -> int
52     val get_tracefn       : string -> unit -> int
53     val set_trace         : string -> int -> unit
54     val reset_trace       : string -> unit
56     val trace             : string * int -> ('a -> 'b) -> 'a -> 'b