debug.mli 2.72 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2012   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
(** Debug flag handling *)
13

14 15
type flag

16
val register_flag : desc:Pp.formatted -> string -> flag
17
(** register a new flag. It is allowed to register twice the same flag *)
18

19
val register_info_flag : desc:Pp.formatted -> string -> flag
20
(** register a new info flag. It is allowed to register twice the same flag.
21
    Info flags are set by --debug-all and must not change the behaviour. *)
22

23
val list_flags : unit -> (string * flag * bool * Pp.formatted) list
24
(** list the known flags *)
25

26 27 28 29 30
val lookup_flag : string -> flag
(** get the flag *)

val is_info_flag : string -> bool
(** test if the flag is an info flag *)
31

32 33 34
val flag_desc : string -> Pp.formatted
(** get the description of the flag *)

35
(** Modify the state of a flag *)
36 37 38 39
val set_flag : flag -> unit
val unset_flag : flag -> unit
val toggle_flag : flag -> unit

40
(** Return the state of the flag *)
41
val test_flag : flag -> bool
42
val test_noflag : flag -> bool
43 44 45 46

val set_debug_formatter : Format.formatter -> unit
(** Set the formatter used when printing debug material *)

47 48 49
val get_debug_formatter : unit -> Format.formatter
(** Get the formatter used when printing debug material *)

50 51
val dprintf : flag -> ('a, Format.formatter, unit) format -> 'a
(** Print only if the flag is set *)
52

53
val stack_trace : flag
54
(** stack_trace flag *)
55 56

(** Command line arguments *)
57
module Args : sig
58 59 60 61 62 63
  type spec = (Arg.key * Arg.spec * Arg.doc)

  val desc_debug_list : spec
  (** Option for printing the list of debug flags *)

  val option_list : unit -> bool
64
  (** Print the list of flags if requested (in this case return [true]).
65
      You should run this function after the plugins have been loaded. *)
66 67

  val desc_debug_all : spec
68
  (** Option for setting all info flags *)
69 70 71 72 73 74 75 76 77

  val desc_debug : spec
  (** Option for specifying a debug flag to set *)

  val desc_shortcut : string -> Arg.key -> Arg.doc -> spec
  (** Option for setting a specific flag *)

  val set_flags_selected : unit -> unit
  (** Set the flags selected by debug_all, debug or a shortcut.
78
      You should run this function after the plugins have been loaded. *)
79
end