From a6926c7e898da1742b0ddd3100cd48eaad5f0e9c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 29 Apr 2024 13:53:48 +0200
Subject: [PATCH] Ltac2: Expose message boxing primitives

cf #18923 (not sure we want to close without also interpreting format strings)
---
 .../18988-ltac2-message-box.rst               |  4 +++
 plugins/ltac2/tac2core.ml                     | 14 +++++++++
 user-contrib/Ltac2/Message.v                  | 30 +++++++++++++++++++
 3 files changed, 48 insertions(+)
 create mode 100644 doc/changelog/06-Ltac2-language/18988-ltac2-message-box.rst

diff --git a/doc/changelog/06-Ltac2-language/18988-ltac2-message-box.rst b/doc/changelog/06-Ltac2-language/18988-ltac2-message-box.rst
new file mode 100644
index 0000000000000..e5e791129b9ac
--- /dev/null
+++ b/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).
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index 89ad96f85d166..7cbec339fa1c9 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/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 () =
diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v
index e78376b926d8c..64c9d711f34e5 100644
--- a/user-contrib/Ltac2/Message.v
+++ b/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. *)