From 88c8cd5cf29a74a7cdb21db78791644e52401b95 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 8 Dec 2022 11:20:14 +0100
Subject: [PATCH] fix: show correct goal state after an empty `by`

---
 src/Lean/Server/InfoUtils.lean                    |  7 ++++++-
 tests/lean/interactive/plainGoal.lean             | 15 +++++++++++++++
 .../lean/interactive/plainGoal.lean.expected.out  | 14 +++++++++++++-
 3 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 273a8aecab..3a0e69bb93 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -299,7 +299,8 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
               ctxInfo := ctx
               tacticInfo := ti
               useAfter := hoverPos > pos && !cs.any (hasNestedTactic pos tailPos)
-              indented := (text.toPosition pos).column > (text.toPosition hoverPos).column
+              -- consider every position unindented after an empty `by` to support "hanging" `by` uses
+              indented := (text.toPosition pos).column > (text.toPosition hoverPos).column && !isEmptyBy ti.stx
               -- use goals just before cursor as fall-back only
               -- thus for `(by foo)`, placing the cursor after `foo` shows its state as long
               -- as there is no state on `)`
@@ -322,6 +323,10 @@ where
     | InfoTree.node (Info.ofMacroExpansionInfo _) cs =>
       cs.any (hasNestedTactic pos tailPos)
     | _ => false
+  isEmptyBy (stx : Syntax) : Bool :=
+    -- there are multiple `by` kinds with the same structure
+    stx.getNumArgs == 2 && stx[0].isToken "by" && stx[1].getNumArgs == 1 && stx[1][0].isMissing
+
 
 partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) :=
   -- In the case `f a b`, where `f` is an identifier, the term goal at `f` should be the goal for the full application `f a b`.
diff --git a/tests/lean/interactive/plainGoal.lean b/tests/lean/interactive/plainGoal.lean
index dfa8945e00..43d825a031 100644
--- a/tests/lean/interactive/plainGoal.lean
+++ b/tests/lean/interactive/plainGoal.lean
@@ -102,6 +102,21 @@ example : True = True := by
   --
 --^ $/lean/plainGoal
 
+example : True := by
+  have : True := by
+    -- type here
+  --^ $/lean/plainGoal
+-- no `this` here either, but seems okay
+--^ $/lean/plainGoal
+
+example : True := by
+  have : True := by
+    -- type here
+  --^ $/lean/plainGoal
+  apply this
+--^ $/lean/plainGoal
+-- note: no output here at all because of parse error
+
 example : False := by
 -- EOF test
 --^ $/lean/plainGoal
diff --git a/tests/lean/interactive/plainGoal.lean.expected.out b/tests/lean/interactive/plainGoal.lean.expected.out
index 0243b5037d..659892bc3b 100644
--- a/tests/lean/interactive/plainGoal.lean.expected.out
+++ b/tests/lean/interactive/plainGoal.lean.expected.out
@@ -142,5 +142,17 @@ null
  "position": {"line": 101, "character": 2}}
 {"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 105, "character": 2}}
+ "position": {"line": 106, "character": 4}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 108, "character": 2}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 113, "character": 4}}
+{"rendered": "```lean\n⊢ True\n```", "goals": ["⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 115, "character": 2}}
+null
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 120, "character": 2}}
 {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]}