rename arg w -> width

src/Init/Data/Format/Basic.lean

@@ -300,11 +300,18 @@ instance : MonadPrettyFormat (StateM State) where
   startTag _         := return ()
   endTags _          := return ()
 
-/-- Pretty-print a `Format` object as a string with expected width `w`. -/
+/--
+Renders a `Format` to a string.
+* `width`: the total width
+* `indent`: the initial indentation to use for wrapped lines
+  (subsequent wrapping may increase the indentation)
+* `column`: begin the first line wrap `column` characters earlier than usual
+  (this is useful when the output String will be printed starting at `column`)
+-/
 @[export lean_format_pretty]
-def pretty (f : Format) (w : Nat := defWidth) : String :=
-  let act: StateM State Unit := prettyM f w
-  act {} |>.snd.out
+def pretty (f : Format) (width : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
+  let act : StateM State Unit := prettyM f width indent
+  State.out <| act (State.mk "" column) |>.snd
 
 end Format
 

src/library/trace.cpp

@@ -165,16 +165,16 @@ extern "C" object * lean_pp_expr(object * env, object * mctx, object * lctx, obj
 
 /*
 @[export lean_format_pretty]
-def pretty (f : Format) (w : Nat := defWidth) : String :=
+def pretty (f : Format) (w : Nat := defWidth) (indent : Nat := 0) (column := 0) : String :=
 */
-extern "C" object * lean_format_pretty(object * f, object * w);
+extern "C" object * lean_format_pretty(object * f, object * w, object * i, object * c);
 
 std::string pp_expr(environment const & env, options const & opts, local_ctx const & lctx, expr const & e) {
     options o = opts;
     // o = o.update(name{"pp", "proofs"}, true); --
     object_ref fmt = get_io_result<object_ref>(lean_pp_expr(env.to_obj_arg(), lean_mk_metavar_ctx(lean_box(0)), lctx.to_obj_arg(), o.to_obj_arg(),
                                                             e.to_obj_arg(), io_mk_world()));
-    string_ref str(lean_format_pretty(fmt.to_obj_arg(), lean_unsigned_to_nat(80)));
+    string_ref str(lean_format_pretty(fmt.to_obj_arg(), lean_unsigned_to_nat(80), lean_unsigned_to_nat(0), lean_unsigned_to_nat(0)));
     return str.to_std_string();
 }