From 4d8859140c4988911ffa48a4479367c878b5cccd Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 6 Feb 2021 17:25:26 +0100
Subject: [PATCH] feat: improve goal display markup

---
 src/Lean/Server/FileWorker.lean | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 32df89e883..b15eda79ae 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -436,11 +436,16 @@ section RequestHandling
         for t in snap.toCmdState.infoState.trees do
           if let some (ci, ti) := t.goalsAt? hoverPos then
             let ci := { ci with mctx := ti.mctxAfter }
-            let goals ← ci.ppGoals ti.goalsAfter
-            let fmt := f!"```lean
-{goals}
+            let md ←
+              if ti.goalsAfter.isEmpty then
+                "no goals"
+              else
+                let goals ← ci.runMetaM {} <| ti.goalsAfter.mapM Meta.ppGoal
+                let goals := goals.map fun goal => s!"```lean
+{goal}
 ```"
-            return some { rendered := toString fmt }
+                String.intercalate "\n---\n" goals
+            return some { rendered := md }
 
         return none