[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

@@ -54,6 +54,8 @@
    implementation is partial: we only take into account the first
    position, and we only return a single range (Coq sentence) without
    parents. (@ejgallego, #582)
+ - 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
 -----------------------------

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>
     </>
   );
 }

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>
   );

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;
+}

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.