fix: cdot parser error message range (#4528)

as #4527 describes there is inconsistency between `by`, `case` and
`next` on the one hand who, if the goal isn’t closed, put squiggly
underlines on the first line, and `.`, which so far only squiggled the
dot (which is a very short symbol!)

With this change the same mechanism as used by `case`, namely
`withCaseRef`, is also used for `.`.

There is an argument for the status quo: The `.` tactic is more commonly
used
with further tactics on the same line, and thus there is now a higher
risk that
the user might think that the first tactic is broken. But 

* the same argument does apply to `by` and `case` where there was an
intentional
  choice to do it this way
* consistency and
* a squiggly line just under the short `.` is easy to miss, so it is
actually
better to underlining more here (at least until we have a better way to
  indicate incomplete proofs, which I have hopes for)

Fixes #4527, at least most of it.

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -199,7 +199,7 @@ def evalTacticCDot : Tactic := fun stx => do
   -- but the token antiquotation does not copy trailing whitespace, leading to
   -- differences in the goal display (#2153)
   let initInfo ← mkInitialTacticInfo stx[0]
-  withRef stx[0] <| closeUsingOrAdmit do
+  withCaseRef stx[0] stx[1] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `·`
     withInfoContext (pure ()) initInfo
     Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx

tests/lean/interactive/issue4527.lean

@@ -0,0 +1,5 @@
+example : True :=  by
+  . skip
+    --^ collectDiagnostics
+    skip
+    -- foo

tests/lean/interactive/issue4527.lean.expected.out

@@ -0,0 +1,10 @@
+{"version": 1,
+ "uri": "file:///issue4527.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 1, "character": 2}, "end": {"line": 2, "character": 0}},
+   "message": "unsolved goals\n⊢ True",
+   "fullRange":
+   {"start": {"line": 1, "character": 2}, "end": {"line": 3, "character": 8}}}]}

tests/lean/refineFiltersOldMVars.lean.expected.out

@@ -9,12 +9,12 @@ h : Type
 case a
 ⊢ Type
 refineFiltersOldMVars.lean:66:4-66:11: error: no goals to be solved
-refineFiltersOldMVars.lean:101:2-101:3: error: unsolved goals
+refineFiltersOldMVars.lean:101:2-101:13: error: unsolved goals
 case d
 ⊢ Bool
-refineFiltersOldMVars.lean:102:2-102:3: error: unsolved goals
+refineFiltersOldMVars.lean:102:2-102:13: error: unsolved goals
 case e
 ⊢ Nat
-refineFiltersOldMVars.lean:109:2-109:3: error: unsolved goals
+refineFiltersOldMVars.lean:109:2-109:13: error: unsolved goals
 case e
 ⊢ Bool

tests/lean/tacUnsolvedGoalsErrors.lean.expected.out

@@ -32,13 +32,13 @@ p q r : Prop
 h2 : p → q
 h✝ : q
 ⊢ q
-tacUnsolvedGoalsErrors.lean:26:2-26:3: error: unsolved goals
+tacUnsolvedGoalsErrors.lean:26:2-27:8: error: unsolved goals
 case inl
 p q r : Prop
 h2 : p → q
 h✝ : p
 ⊢ q
-tacUnsolvedGoalsErrors.lean:28:2-28:3: error: unsolved goals
+tacUnsolvedGoalsErrors.lean:28:2-29:8: error: unsolved goals
 case inr
 p q r : Prop
 h2 : p → q