Ltac2: Expose message boxing primitives

cf coq#18923 (not sure we want to close without also interpreting format strings)

doc/changelog/06-Ltac2-language/18988-ltac2-message-box.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  APIs in `Ltac2.Message` to interact with the boxing system of the pretty printer
+  (`#18988 <https://github.com/coq/coq/pull/18988>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -281,6 +281,20 @@ let () =
 
 let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app
 
+let () = define "message_force_new_line" (ret pp) (Pp.fnl ())
+
+let () = define "message_break" (int @-> int @-> ret pp) (fun i j -> Pp.brk (i,j))
+
+let () = define "message_space" (ret pp) (Pp.spc())
+
+let () = define "message_hbox" (pp @-> ret pp) Pp.h
+
+let () = define "message_vbox" (int @-> pp @-> ret pp) Pp.v
+
+let () = define "message_hvbox" (int @-> pp @-> ret pp) Pp.hv
+
+let () = define "message_hovbox" (int @-> pp @-> ret pp) Pp.hov
+
 let () = define "format_stop" (ret format) []
 
 let () =

user-contrib/Ltac2/Message.v

@@ -28,6 +28,36 @@ Ltac2 @ external of_exn : exn -> message := "coq-core.plugins.ltac2" "message_of
 
 Ltac2 @ external concat : message -> message -> message := "coq-core.plugins.ltac2" "message_concat".
 
+Ltac2 @external force_new_line : message := "coq-core.plugins.ltac2" "message_force_new_line".
+(** Force writing on a new line after this. *)
+
+Ltac2 @external break : int -> int -> message := "coq-core.plugins.ltac2" "message_break".
+(** General break hint: [break n i] either prints [n] spaces or splits
+    the line adding [i] to the current indentation. *)
+
+Ltac2 @external space : message := "coq-core.plugins.ltac2" "message_space".
+(** Breaking space. Equivalent to [break 1 0]. *)
+
+Ltac2 @external hbox : message -> message := "coq-core.plugins.ltac2" "message_hbox".
+(** Horizontal box. Break hints in a horizontal box never split the
+    line (nested boxes inside the horizontal box may allow line
+    splitting). *)
+
+Ltac2 @external vbox : int -> message -> message := "coq-core.plugins.ltac2" "message_vbox".
+(** Vertical box. Every break hint in a vertical box splits the line.
+    The [int] is added to the current indentation when splitting the line. *)
+
+Ltac2 @external hvbox : int -> message -> message := "coq-core.plugins.ltac2" "message_hvbox".
+(** Horizontal/vertical box. Behaves as a horizontal box if it fits on
+    a single line, otherwise behaves as a vertical box (using the
+    given [int]). *)
+
+Ltac2 @external hovbox : int -> message -> message := "coq-core.plugins.ltac2" "message_hovbox".
+(** Horizonal-or-vertical box. Prints as much as possible on each
+    line, splitting the line at break hints when there is no more room
+    on the line (see "Printing Width" option). The [int] is added to
+    the indentation when splitting the line. *)
+
 Module Format.
 
 (** Only for internal use. *)