Merge pull request #586 from ejgallego/adjust_in_messages_and_errors

[info view] Adjust breaks in errors and messages panels.

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

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.