Module Topfmt

Console printing options

type pp_global_params = {
margin : int;
max_indent : int;
max_depth : int;
ellipsis : string;
}
val dflt_gp : pp_global_params
val deep_gp : pp_global_params
val set_gp : Stdlib.Format.formatter -> pp_global_params -> unit
val set_dflt_gp : Stdlib.Format.formatter -> unit
val get_gp : Stdlib.Format.formatter -> pp_global_params
Output functions of pretty-printing.
val with_output_to : Stdlib.out_channel -> Stdlib.Format.formatter
val std_ft : Stdlib.Format.formatter Stdlib.ref
val err_ft : Stdlib.Format.formatter Stdlib.ref
val deep_ft : Stdlib.Format.formatter Stdlib.ref
For parametrization through vernacular.
val set_depth_boxes : int option -> unit
val get_depth_boxes : unit -> int option
val set_margin : int option -> unit
val get_margin : unit -> int option
val std_logger : ?qf:Quickfix.t list -> ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit

Console display of feedback, we may add some location information

val emacs_logger : ?qf:Quickfix.t list -> ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
val default_styles : unit -> unit

Color output

val parse_color_config : string -> unit
val dump_tags : unit -> (string * Terminal.style) list
val set_emacs_print_strings : unit -> unit
val init_terminal_output : color:bool -> unit

Initialization of interpretation of tags

Error printing

type execution_phase =
| ParsingCommandLine
| Initialization
| LoadingPrelude
| LoadingRcFile
| InteractiveLoop
| CompilationPhase
val in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b
val pr_phase : ?loc:Loc.t -> unit -> Pp.t option
val print_err_exn : exn -> unit
val with_output_to_file : truncate:bool -> string -> ('a -> 'b) -> 'a -> 'b

with_output_to_file ~truncate file f x executes f x with logging redirected to a file file (starting empty if truncate:true, otherwise appending if it already exists).

val pr_cmd_header : Vernacexpr.vernac_control -> Pp.t