fix: log tactic analysis messages on correct range (leanprover-community#28919)

The tactic analysis framework attempts to log messages on a synthetic concatenation of tactics (`` `(tactic|$tacticSeq;*)``). However, this inserts position info from the current ref in the tactic sequence nodes, and so messages are logged on the current ref (in this case, the whole command).

This PR works around this by setting the ref to the input array of tactics via `mkNullNode`.

(Note that VS code cannot log on disjoint ranges, so Lean's `log*` family of functions only logs on the first line of multiline ranges. Hence, logging on the full tactic sequence range results in a squiggly line under only the first line of the tactic. This is unrelated to the current fix.)

Author: thorimur

Mathlib/Tactic/TacticAnalysis.lean

@@ -282,18 +282,21 @@ from the start of the sequence. -/
 def testTacticSeq (config : ComplexConfig) (tacticSeq : Array (TSyntax `tactic))
     (ctxI : ContextInfo) (i : TacticInfo) (ctx : config.ctx) :
     CommandElabM Unit := do
-  let stx ← `(tactic| $(tacticSeq);*)
-  -- TODO: support more than 1 goal. Probably by requiring all tests to succeed in a row
-  if let [goal] := i.goalsBefore then
-    let (oldGoals, oldHeartbeats) ← withHeartbeats <|
-      try
-        ctxI.runTacticCode i goal stx
-      catch e =>
-        logWarningAt stx m!"original tactic '{stx}' failed: {e.toMessageData}"
-        return [goal]
-    let (new, newHeartbeats) ← withHeartbeats <| ctxI.runTactic i goal <| config.test ctx
-    if let some msg := config.tell stx oldGoals oldHeartbeats new newHeartbeats  then
-      logWarningAt stx msg
+  /- Syntax quotations use the current ref's position info even for nodes which do not usually
+  carry position info. We set the ref here to ensure we log messages on the correct range. -/
+  withRef (mkNullNode tacticSeq) do
+    let stx ← `(tactic| $tacticSeq;*)
+    -- TODO: support more than 1 goal. Probably by requiring all tests to succeed in a row
+    if let [goal] := i.goalsBefore then
+      let (oldGoals, oldHeartbeats) ← withHeartbeats <|
+        try
+          ctxI.runTacticCode i goal stx
+        catch e =>
+          logWarning m!"original tactic '{stx}' failed: {e.toMessageData}"
+          return [goal]
+      let (new, newHeartbeats) ← withHeartbeats <| ctxI.runTactic i goal <| config.test ctx
+      if let some msg := config.tell stx oldGoals oldHeartbeats new newHeartbeats  then
+        logWarning msg
 
 /-- Run the `config` against a sequence of tactics, using the `trigger` to determine which
 subsequences should be `test`ed. -/