From eadd9bcdb0eff1d4b125f96f3b650d5fa114214e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 22 Jun 2018 17:36:22 +0200
Subject: [PATCH] Open a box and use infinite width when displaying warnings.

Otherwise we get ugly line breaks. Example:

warning: termination of this expression cannot be proved, but there is no
`diverges' \\
clause in the outer \\
specification
---
 src/util/warning.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/util/warning.ml b/src/util/warning.ml
index a44af1295..c2b239864 100644
--- a/src/util/warning.ml
+++ b/src/util/warning.ml
@@ -21,6 +21,8 @@ let set_hook = (:=) hook
 let emit ?loc p =
   let b = Buffer.create 100 in
   let fmt = formatter_of_buffer b in
+  pp_set_margin fmt 1000000000;
+  pp_open_box fmt 0;
   let handle fmt =
-    Format.pp_print_flush fmt (); !hook ?loc (Buffer.contents b) in
+    pp_print_flush fmt (); !hook ?loc (Buffer.contents b) in
   kfprintf handle fmt p
-- 
GitLab