honor Set Margin Width

Author: gares

src/coq_elpi_HOAS.ml

@@ -345,13 +345,13 @@ type options = {
   redflags : CClosure.RedFlags.reds option;
 }
 
-let default_options = {
+let default_options () = {
   hoas_holes = Some Verbatim;
   local = None;
   deprecation = None;
   primitive = None;
   failsafe = false;
-  ppwidth = 80;
+  ppwidth = Option.default 80 (Topfmt.get_margin ());
   pp = Normal;
   pplevel = Constrexpr.LevelSome;
   using = None;
@@ -1360,7 +1360,7 @@ and under_coq2elpi_ctx ~calldepth state ctx ?(mk_ctx_item=fun decl -> mk_pi_arro
   in
   let state, coq_ctx, hyps =
       let state, coq_ctx, hyps =
-        aux 0 ~depth:calldepth (mk_coq_context ~options:default_options state) [] state (List.rev ctx) in
+        aux 0 ~depth:calldepth (mk_coq_context ~options:(default_options ()) state) [] state (List.rev ctx) in
       state, coq_ctx, hyps in
   let state, t, gls_t = kont coq_ctx hyps ~depth:(calldepth + List.length hyps) state in
   gls := gls_t @ !gls;

src/coq_elpi_HOAS.mli

@@ -72,7 +72,7 @@ type 'a coq_context = {
 }
 val mk_coq_context : options:options -> State.t -> empty coq_context
 val get_options : depth:int -> Data.hyps -> State.t -> options
-val default_options : options
+val default_options : unit -> options
 val upcast : [> `Options ] coq_context -> full coq_context
 
 val get_current_env_sigma : depth:int ->

src/coq_elpi_builtins.ml

@@ -1667,7 +1667,7 @@ Supported attributes:
     Out(list constant, "GlobalObjects",
     Read(unit_ctx, "lists the global objects that are marked as to be abstracted at the end of the enclosing sections")),
   (fun _ ~depth _ _ state ->
-     let { section } = mk_coq_context ~options:default_options state in
+     let { section } = mk_coq_context ~options:(default_options ()) state in
      !: (section |> List.map (fun x -> Variable x)) )),
   DocAbove);
 

src/coq_elpi_glob_quotation.ml

@@ -60,7 +60,7 @@ let is_restricted_name =
 
 (* XXX: I don't get why we use a coq_ctx here *)
 let under_ctx name ty bo gterm2lp ~depth state x =
-  let coq_ctx, hyps as orig_ctx = Option.default (upcast @@ mk_coq_context ~options:default_options state,[]) (get_ctx state) in
+  let coq_ctx, hyps as orig_ctx = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state,[]) (get_ctx state) in
   let state, name =
     let id =
       match name with
@@ -149,7 +149,7 @@ let rec gterm2lp ~depth state x =
     end
   | GRef(gr,_ul) -> state, in_elpi_gr ~depth state gr
   | GVar(id) ->
-      let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:default_options state, []) (get_ctx state) in
+      let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
       if not (Id.Map.mem id ctx.name2db) then
         CErrors.user_err ?loc:x.CAst.loc
           Pp.(str"Free Coq variable " ++ Names.Id.print id ++ str " in context: " ++
@@ -178,7 +178,7 @@ let rec gterm2lp ~depth state x =
         match oty with
         | None ->
             let state, uv = F.Elpi.make state in
-            let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:default_options state, []) (get_ctx state) in
+            let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
             let args = List.map (fun (_,x) -> E.mkBound x) (Id.Map.bindings ctx.name2db) in
             state, E.mkUnifVar uv ~args state
         | Some ty -> gterm2lp ~depth state ty in
@@ -191,7 +191,7 @@ let rec gterm2lp ~depth state x =
       let s, x =
         match E.look ~depth x with
         | E.App(c,call,[]) when c == E.Constants.spillc ->
-          let _, hyps = Option.default (upcast @@ mk_coq_context ~options:default_options state, []) (get_ctx state) in
+          let _, hyps = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
           let hyps = List.map (fun { ctx_entry = t; depth = from } ->
             U.move ~from ~to_:depth t) hyps in
           s, E.mkApp c (E.mkApp E.Constants.implc (U.list_to_lp_list hyps) [call]) []
@@ -215,7 +215,7 @@ let rec gterm2lp ~depth state x =
 
   | GHole (_,_,None) ->
       let state, uv = F.Elpi.make state in
-      let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:default_options state, []) (get_ctx state) in
+      let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:(default_options ()) state, []) (get_ctx state) in
       let args =
         Id.Map.bindings ctx.name2db |>
         List.filter (fun (n,_) -> not(is_restricted_name n)) |>

src/coq_elpi_utils.ml

@@ -57,6 +57,7 @@ let nYI s = err Pp.(str"Not Yet Implemented: " ++ str s)
 let pp2string pp x =
   let b = Buffer.create 80 in
   let fmt = Format.formatter_of_buffer b in
+  Format.pp_set_margin fmt (Option.default 80 (Topfmt.get_margin ()));
   Format.fprintf fmt "%a%!" pp x;
   Buffer.contents b
 

src/coq_elpi_vernacular.ml

@@ -693,7 +693,7 @@ let run_program loc name ~atts args =
   in
   let query ~depth state =
     let state, args, gls = EU.map_acc
-      (Coq_elpi_arg_HOAS.in_elpi_cmd ~depth ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:default_options state))
+      (Coq_elpi_arg_HOAS.in_elpi_cmd ~depth ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state))
       state args in
     let state, q = atts2impl loc ~depth state atts (ET.mkApp mainc (EU.list_to_lp_list args) []) in
     let state = API.State.set Coq_elpi_builtins.tactic_mode state false in