diff options
Diffstat (limited to 'lib/pp_control.ml')
-rw-r--r-- | lib/pp_control.ml | 93 |
1 files changed, 0 insertions, 93 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml deleted file mode 100644 index 890ffe0a..00000000 --- a/lib/pp_control.ml +++ /dev/null @@ -1,93 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* Parameters of pretty-printing *) - -type pp_global_params = { - margin : int; - max_indent : int; - max_depth : int; - ellipsis : string } - -(* Default parameters of pretty-printing *) - -let dflt_gp = { - margin = 78; - max_indent = 50; - max_depth = 50; - ellipsis = "..." } - -(* A deeper pretty-printer to print proof scripts *) - -let deep_gp = { - margin = 78; - max_indent = 50; - max_depth = 10000; - ellipsis = "..." } - -(* set_gp : Format.formatter -> pp_global_params -> unit - * set the parameters of a formatter *) - -let set_gp ft gp = - Format.pp_set_margin ft gp.margin ; - Format.pp_set_max_indent ft gp.max_indent ; - Format.pp_set_max_boxes ft gp.max_depth ; - Format.pp_set_ellipsis_text ft gp.ellipsis - -let set_dflt_gp ft = set_gp ft dflt_gp - -let get_gp ft = - { margin = Format.pp_get_margin ft (); - max_indent = Format.pp_get_max_indent ft (); - max_depth = Format.pp_get_max_boxes ft (); - ellipsis = Format.pp_get_ellipsis_text ft () } - -(* with_fp : 'a pp_formatter_params -> Format.formatter - * returns of formatter for given formatter functions *) - -let with_fp chan out_function flush_function = - let ft = Format.make_formatter out_function flush_function in - Format.pp_set_formatter_out_channel ft chan; - ft - -(* Output on a channel ch *) - -let with_output_to ch = - let ft = with_fp ch (output ch) (fun () -> flush ch) in - set_gp ft deep_gp; - ft - -let std_ft = ref Format.std_formatter -let _ = set_dflt_gp !std_ft - -let err_ft = ref Format.err_formatter -let _ = set_gp !err_ft deep_gp - -let deep_ft = ref (with_output_to stdout) -let _ = set_gp !deep_ft deep_gp - -(* For parametrization through vernacular *) -let default = Format.pp_get_max_boxes !std_ft () -let default_margin = Format.pp_get_margin !std_ft () - -let get_depth_boxes () = Some (Format.pp_get_max_boxes !std_ft ()) -let set_depth_boxes v = - Format.pp_set_max_boxes !std_ft (match v with None -> default | Some v -> v) - -let get_margin () = Some (Format.pp_get_margin !std_ft ()) -let set_margin v = - let v = match v with None -> default_margin | Some v -> v in - Format.pp_set_margin Format.str_formatter v; - Format.pp_set_margin !std_ft v; - Format.pp_set_margin !deep_ft v; - (* Heuristic, based on usage: the column on the right of max_indent - column is 20% of width, capped to 30 characters *) - let m = max (64 * v / 100) (v-30) in - Format.pp_set_max_indent Format.str_formatter m; - Format.pp_set_max_indent !std_ft m; - Format.pp_set_max_indent !deep_ft m |