diff --git a/CHANGES.md b/CHANGES.md index 895093d4a..d0e06ec26 100644 --- a/CHANGES.md +++ b/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 ----------------------------- diff --git a/editor/code/views/info/ErrorBrowser.tsx b/editor/code/views/info/ErrorBrowser.tsx index 964968fa9..cb533bafc 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 | null = useRef(null); + useLayoutEffect(() => { + if (ref.current) { + FormatPrettyPrint.adjustBreaks($(ref.current)); + } + }); + return ( <>
Errors:
- ; +
+ ; +
); } diff --git a/editor/code/views/info/Message.tsx b/editor/code/views/info/Message.tsx index 3218ec86d..1b3e2334a 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; }) { + const ref: React.LegacyRef | 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 ( -
  • +
  • ); diff --git a/editor/code/views/info/media/goals.css b/editor/code/views/info/media/goals.css index 15838b7a1..6c520206d 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 000000000..c0105b071 --- /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.