aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/pp_control.ml6
-rw-r--r--lib/pp_control.mli3
2 files changed, 9 insertions, 0 deletions
diff --git a/lib/pp_control.ml b/lib/pp_control.ml
index 44f351458..caa985c18 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.ml
@@ -96,7 +96,13 @@ 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 =
+ Format.pp_set_margin !std_ft (match v with None -> default_margin | Some v -> v)
+
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 256cc26de..b7cc42d11 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -44,3 +44,6 @@ val deep_ft : Format.formatter
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