From d13d83eb7a35c8f53ee1c91d861dde68c57c161d Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Thu, 30 Jan 2025 14:14:51 +0100
Subject: [PATCH] fix: redundant line breaks in trace messages (#571)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR ensures that there are no redundant line breaks when the trace
formatter is including a newline at the end of a trace line.

Example (from `whnfProj.lean`):
```lean
import Lean

def h (x : Nat) := x
def f (x : Nat) := x + 1
def g (x : Nat) := (x, x+1).fst


open Lean
open Lean.Meta

def tst (declName : Name) : MetaM Unit := do
  let c ← getConstInfo declName
  lambdaTelescope c.value! fun _ b => do
    trace[Meta.debug] "1. {b}"
    trace[Meta.debug] "2. {← withReducible <| whnf b}"
    trace[Meta.debug] "3. {← withReducibleAndInstances <| whnf b}"
    trace[Meta.debug] "4. {← withDefault <| whnf b}"
    pure ()

set_option trace.Meta.debug true
#eval tst `f
#eval tst `g
```
---
 lean4-infoview/package.json           | 2 +-
 lean4-infoview/src/infoview/index.css | 3 +++
 package-lock.json                     | 4 ++--
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json
index b2a1210a4..4732b93fc 100644
--- a/lean4-infoview/package.json
+++ b/lean4-infoview/package.json
@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.8.0",
+    "version": "0.8.1",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css
index 513ecdadc..079b29bb5 100644
--- a/lean4-infoview/src/infoview/index.css
+++ b/lean4-infoview/src/infoview/index.css
@@ -58,6 +58,9 @@ body {
 }
 
 /* Interactive traces */
+.trace-line {
+    display: inline-block;
+}
 .trace-line:hover {
     background-color: #dbeeff;
 }
diff --git a/package-lock.json b/package-lock.json
index e3c7d2174..ca6992faf 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -28,7 +28,7 @@
         },
         "lean4-infoview": {
             "name": "@leanprover/infoview",
-            "version": "0.8.0",
+            "version": "0.8.1",
             "license": "Apache-2.0",
             "dependencies": {
                 "@leanprover/infoview-api": "~0.5.0",
@@ -16903,7 +16903,7 @@
         },
         "vscode-lean4": {
             "name": "lean4",
-            "version": "0.0.189",
+            "version": "0.0.191",
             "license": "Apache-2.0",
             "dependencies": {
                 "@leanprover/infoview": "~0.8.0",