From 07dac6784705fdd4a5e060ca569f247bed7b3f58 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 12 Mar 2024 17:35:14 +0100
Subject: [PATCH] feat: guard_msgs to escapes trailing newlines (#3617)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This makes trailing whitespace visible and protectes them against
trimming by the editor, by appending the symbol ⏎ to such a line (and
also to any line that ends with such a symbol, to avoid ambiguities in
the case the message already had that symbol).

(Only the code action output / docstring parsing is affected; the error
message as sent
to the InfoView is unaffected.)

Fixes #3571
---
 src/Lean/Elab/GuardMsgs.lean   | 25 +++++++++++++++---
 tests/lean/run/guard_msgs.lean | 46 ++++++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean
index b56889bea9..ecdca448c4 100644
--- a/src/Lean/Elab/GuardMsgs.lean
+++ b/src/Lean/Elab/GuardMsgs.lean
@@ -73,9 +73,28 @@ structure GuardMsgFailure where
   res : String
 deriving TypeName
 
+/--
+Makes trailing whitespace visible and protectes them against trimming by the editor, by appending
+the symbol ⏎ to such a line (and also to any line that ends with such a symbol, to avoid
+ambiguities in the case the message already had that symbol).
+-/
+def revealTrailingWhitespace (s : String) : String :=
+  s.replace "⏎\n" "⏎⏎\n" |>.replace "\t\n" "\t⏎\n" |>.replace " \n" " ⏎\n"
+
+/- The inverse of `revealTrailingWhitespace` -/
+def removeTrailingWhitespaceMarker (s : String) : String :=
+  s.replace "⏎\n" "\n"
+
+/--
+Strings are compared up to newlines, to allow users to break long lines.
+-/
+def equalUpToNewlines (exp res : String) : Bool :=
+  exp.replace "\n" " " == res.replace "\n" " "
+
 @[builtin_command_elab Lean.guardMsgsCmd] def elabGuardMsgs : CommandElab
   | `(command| $[$dc?:docComment]? #guard_msgs%$tk $(spec?)? in $cmd) => do
-    let expected : String := (← dc?.mapM (getDocStringText ·)).getD "" |>.trim
+    let expected : String := (← dc?.mapM (getDocStringText ·)).getD ""
+        |>.trim |> removeTrailingWhitespaceMarker
     let specFn ← parseGuardMsgsSpec spec?
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     elabCommandTopLevel cmd
@@ -88,8 +107,7 @@ deriving TypeName
       | .drop        => pure ()
       | .passthrough => toPassthrough := toPassthrough.add msg
     let res := "---\n".intercalate (← toCheck.toList.mapM (messageToStringWithoutPos ·)) |>.trim
-    -- We do some whitespace normalization here to allow users to break long lines.
-    if expected.replace "\n" " " == res.replace "\n" " " then
+    if equalUpToNewlines expected res then
       -- Passed. Only put toPassthrough messages back on the message log
       modify fun st => { st with messages := initMsgs ++ toPassthrough }
     else
@@ -119,6 +137,7 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
     lazy? := some do
       let some start := stx.getPos? true | return eager
       let some tail := stx.setArg 0 mkNullNode |>.getPos? true | return eager
+      let res := revealTrailingWhitespace res
       let newText := if res.isEmpty then
         ""
       else if res.length ≤ 100-7 && !res.contains '\n' then -- TODO: configurable line length?
diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean
index c7e85438e1..2e4faa99dc 100644
--- a/tests/lean/run/guard_msgs.lean
+++ b/tests/lean/run/guard_msgs.lean
@@ -1,3 +1,5 @@
+import Lean.Elab.Command
+
 #guard_msgs in
 /-- error: unknown identifier 'x' -/
 #guard_msgs in
@@ -49,3 +51,47 @@ error: failed to synthesize instance
 -/
 #guard_msgs(error) in
 example : α := 22
+
+-- Trailing whitespace
+
+/--
+info: foo ⏎
+bar
+---
+error: ❌ Docstring on `#guard_msgs` does not match generated message:
+
+info: foo ⏎
+bar
+-/
+#guard_msgs in
+#guard_msgs in
+run_meta Lean.logInfo "foo \nbar"
+
+#guard_msgs in
+/--
+info: foo ⏎
+bar
+-/
+#guard_msgs in
+run_meta Lean.logInfo "foo \nbar"
+
+/--
+info: foo ⏎⏎
+bar
+---
+error: ❌ Docstring on `#guard_msgs` does not match generated message:
+
+info: foo ⏎⏎
+bar
+-/
+#guard_msgs in
+#guard_msgs in
+run_meta Lean.logInfo "foo ⏎\nbar"
+
+#guard_msgs in
+/--
+info: foo ⏎⏎
+bar
+-/
+#guard_msgs in
+run_meta Lean.logInfo "foo ⏎\nbar"