fix: getInteractiveDiagnostics off-by-one error (#3608)

This bug is the real cause of leanprover/vscode-lean4#392. 
At the end of a tactic state, the client calls
`getInteractiveDiagnostics` with a range `[last line of proof, last line
of proof + 1)`. The `fullRange` span of the `unresolved goals` error
however is something like `[(first line of proof, start character),
(last line of proof, nonzero end character)).
Since it operates on line numbers, `getInteractiveDiagnostics` would
then check whether `[last line of proof, last line of proof + 1)` and
`[first line of proof, last line of proof)` intersect, which is false
because of the excluded upper bound on the latter interval, despite the
fact that the end character in the last line may be nonzero.

This fix adjusts the intersection logic to use `[first line of proof,
last line of proof]` if the end character is nonzero.

Closes leanprover/vscode-lean4#392.

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -110,10 +110,17 @@ def getInteractiveDiagnostics (params : GetInteractiveDiagnosticsParams) : Reque
   pure <| t.map fun (snaps, _) =>
     let diags? := snaps.getLast?.map fun snap =>
       snap.interactiveDiags.toArray.filter fun diag =>
+        let r := diag.fullRange
+        let diagStartLine := r.start.line
+        let diagEndLine   :=
+          if r.end.character == 0 then
+            r.end.line
+          else
+            r.end.line + 1
         params.lineRange?.all fun ⟨s, e⟩ =>
-          -- does [s,e) intersect [diag.fullRange.start.line,diag.fullRange.end.line)?
-          s ≤ diag.fullRange.start.line ∧ diag.fullRange.start.line < e ∨
-          diag.fullRange.start.line ≤ s ∧ s < diag.fullRange.end.line
+          -- does [s,e) intersect [diagStartLine,diagEndLine)?
+          s ≤ diagStartLine ∧ diagStartLine < e ∨
+          diagStartLine ≤ s ∧ s < diagEndLine
     pure <| diags?.getD #[]
 
 builtin_initialize