chore: further refine goal state heuristics

src/Lean/Server/InfoUtils.lean

@@ -257,7 +257,8 @@ partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String
         let trailSize := i.stx.getTrailingSize
         -- show info at EOF even if strictly outside token + trail
         let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
-        if pos ≤ hoverPos ∧ (hoverPos.byteIdx <= tailPos.byteIdx + trailSize || atEOF) then
+        -- include at least one trailing character (see also `priority` below)
+        if pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + max 1 trailSize || atEOF) then
           -- overwrite bottom-up results according to "innermost" heuristics documented above
           if gs.isEmpty || hoverPos ≥ tailPos && gs.all (·.indented) then
             return [{

tests/lean/interactive/plainGoal.lean

@@ -85,6 +85,9 @@ example (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs) := by
 example : True := (by exact True.intro)
                                     --^ $/lean/plainGoal
 
+example : True := (by exact True.intro )
+                                     --^ $/lean/plainGoal
+
 example : False := by
 -- EOF test
 --^ $/lean/plainGoal

tests/lean/interactive/plainGoal.lean.expected.out

@@ -111,5 +111,8 @@
  "position": {"line": 84, "character": 38}}
 {"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file://plainGoal.lean"},
- "position": {"line": 88, "character": 2}}
+ "position": {"line": 87, "character": 39}}
+null
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 91, "character": 2}}
 {"rendered": "```lean\n⊢ False\n```", "goals": ["⊢ False"]}