From 59c921ee308f69be72dcd2478fa16cc31b96c29c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 25 Oct 2023 17:42:06 +0200
Subject: [PATCH] [info view] Adjust breaks in errors and messages panels.

Fixes #457 , fixes #458 , fixes #571

This is a hotfix, but we should actually move this logic to the CoqPp
component, as adjusting the breaks at every use doesn't scale.

However this fix should be good for now, as the above fix requires a
bit more thinking about the structure of the HTML that contains `Pp`
---
 CHANGES.md                              |  2 ++
 editor/code/views/info/ErrorBrowser.tsx | 14 +++++++++++++-
 editor/code/views/info/Message.tsx      | 12 +++++++++++-
 editor/code/views/info/media/goals.css  | 10 ++++++++++
 examples/record_print.v                 | 24 ++++++++++++++++++++++++
 5 files changed, 60 insertions(+), 2 deletions(-)
 create mode 100644 examples/record_print.v

diff --git a/CHANGES.md b/CHANGES.md
index 1ab98686..ebc66cd5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -56,6 +56,8 @@
    parents. (@ejgallego, #582)
  - Be more robust to mixed-separator windows paths in workspace
    detection (@ejgallego, #583, fixes #569)
+ - Adjust printing breaks in error and message panels (@ejgallego,
+   @Alizter, #586, fixes #457 , fixes #458 , fixes #571)
 
 # coq-lsp 0.1.7: Just-in-time
 -----------------------------
diff --git a/editor/code/views/info/ErrorBrowser.tsx b/editor/code/views/info/ErrorBrowser.tsx
index 964968fa..cb533baf 100644
--- a/editor/code/views/info/ErrorBrowser.tsx
+++ b/editor/code/views/info/ErrorBrowser.tsx
@@ -1,13 +1,25 @@
 import { PpString } from "../../lib/types";
 import { CoqPp } from "./CoqPp";
+import { FormatPrettyPrint } from "../../lib/format-pprint/js/main";
+import $ from "jquery";
+import { useLayoutEffect, useRef } from "react";
 
 export type ErrorBrowserParams = { error: PpString };
 
 export function ErrorBrowser({ error }: ErrorBrowserParams) {
+  const ref: React.LegacyRef<HTMLDivElement> | null = useRef(null);
+  useLayoutEffect(() => {
+    if (ref.current) {
+      FormatPrettyPrint.adjustBreaks($(ref.current));
+    }
+  });
+
   return (
     <>
       <header>Errors:</header>
-      <CoqPp content={error} inline={true} />;
+      <div className="coq-error" ref={ref}>
+        <CoqPp content={error} inline={true} />;
+      </div>
     </>
   );
 }
diff --git a/editor/code/views/info/Message.tsx b/editor/code/views/info/Message.tsx
index 3218ec86..1b3e2334 100644
--- a/editor/code/views/info/Message.tsx
+++ b/editor/code/views/info/Message.tsx
@@ -1,7 +1,10 @@
 // import objectHash from "object-hash";
+import { useLayoutEffect, useRef } from "react";
 import { Message } from "../../lib/types";
 import { PpString } from "../../lib/types";
 import { CoqPp } from "./CoqPp";
+import { FormatPrettyPrint } from "../../lib/format-pprint/js/main";
+import $ from "jquery";
 
 export function Message({
   key,
@@ -10,6 +13,13 @@ export function Message({
   key: React.Key;
   message: PpString | Message<PpString>;
 }) {
+  const ref: React.LegacyRef<HTMLLIElement> | null = useRef(null);
+  useLayoutEffect(() => {
+    if (ref.current) {
+      FormatPrettyPrint.adjustBreaks($(ref.current));
+    }
+  });
+
   let text =
     typeof message === "string"
       ? message
@@ -18,7 +28,7 @@ export function Message({
       : message;
 
   return (
-    <li key={key}>
+    <li key={key} className={"coq-message"} ref={ref}>
       <CoqPp content={text} inline={true} />
     </li>
   );
diff --git a/editor/code/views/info/media/goals.css b/editor/code/views/info/media/goals.css
index 15838b7a..6c520206 100644
--- a/editor/code/views/info/media/goals.css
+++ b/editor/code/views/info/media/goals.css
@@ -53,8 +53,18 @@ p.num-goals + p.aside {
   margin-bottom: 1em;
 }
 
+/* XXX: We need to handle the white-space: pre that all Pp stuff needs
+   better */
 .coq-goal-env {
   padding-top: 1ex;
   padding-bottom: 1ex;
   white-space: pre;
 }
+
+.coq-message {
+  white-space: pre;
+}
+
+.coq-error {
+  white-space: pre;
+}
diff --git a/examples/record_print.v b/examples/record_print.v
new file mode 100644
index 00000000..c0105b07
--- /dev/null
+++ b/examples/record_print.v
@@ -0,0 +1,24 @@
+Record t : Type := {
+  carrier :> Type;
+  unit : carrier;
+  mult : carrier -> carrier -> carrier;
+  assoc : forall a b c, mult a (mult b c) = mult (mult a b) c;
+  unit_l : forall a, mult unit a = a;
+  unit_r : forall a, mult a unit = a;
+}.
+
+Print t.
+
+Module A.
+Axiom A : Type.
+Axiom B : Type.
+Axiom C : Type.
+Axiom D : Type.
+Axiom E : Type.
+End A.
+
+Print A.
+
+Goal True /\ True /\ True /\ True /\ True /\ True /\ True /\ True /\ True /\ True /\ True.
+apply I.
+Qed.