refactor: revert completion assertion mode, use plain completion directives

Remove the completion assertion mode (has/is empty) from the test runner
and use plain `completion` directives in the empty-by tests instead.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Server/Test/Runner.lean

@@ -641,13 +641,13 @@ def processGenericRequest : RunnerM Unit := do
   let params := params.setObjVal! "position" (toJson s.pos)
   logResponse s.method params
 
-def processDirective (ws directive : String) (directiveTargetLineNo : Nat) : RunnerM Unit := do
+def processDirective (_ws directive : String) (directiveTargetLineNo : Nat)
+    (directiveTargetColumn : Nat) : RunnerM Unit := do
   let directive := directive.drop 1
   let colon := directive.find ':'
   let method := directive.sliceTo colon |>.trimAscii |>.copy
   -- TODO: correctly compute in presence of Unicode
-  let directiveTargetColumn := ws.rawEndPos + "--"
-  let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn.byteIdx }
+  let pos : Lsp.Position := { line := directiveTargetLineNo, character := directiveTargetColumn }
   let params :=
     if h : ¬colon.IsAtEnd then
       directive.sliceFrom (colon.next h) |>.trimAscii.copy
@@ -686,10 +686,15 @@ def processLine (line : String) : RunnerM Unit := do
     match directive.front with
     | 'v' => pure <| (← get).lineNo + 1  -- TODO: support subsequent 'v'... or not
     | '^' => pure <| (← get).lastActualLineNo
+    -- `⬑` is like `^` but targets the column of the `--` marker itself (i.e. column 0 when the
+    -- marker is at the start of the line), rather than the column after `--`.
+    | '⬑' => pure <| (← get).lastActualLineNo
     | _ =>
       skipLineWithoutDirective
       return
-  processDirective ws directive directiveTargetLineNo
+  let directiveTargetColumn :=
+    if directive.front == '⬑' then ws.rawEndPos.byteIdx else (ws.rawEndPos + "--").byteIdx
+  processDirective ws directive directiveTargetLineNo (directiveTargetColumn := directiveTargetColumn)
   skipLineWithDirective
 
 

tests/server_interactive/completionEmptyBy.lean

@@ -0,0 +1,122 @@
+prelude
+import Init.Notation
+
+/-
+Tests for tactic completion in empty `by` blocks (no indented tactics follow).
+
+Tests cover:
+- Top-level `by`
+- Nested `by` inside expressions (e.g. `id <| have := by`)
+- Completion at various columns on the line below `by`
+
+Note: `--^` tests at the column of `^`; `--⬑` tests at the column of `--` itself (for column 0).
+To test a column on the line below `by`, we place an indented comment there so that the tested
+column falls within the leading whitespace (matching how completionTactics.lean works).
+-/
+
+/-- A docstring -/
+syntax (name := skip) "skip" : tactic
+
+-- ===== On the `by` token itself (no completions expected) =====
+
+-- column 20 on `by` line (end of `by` token, before whitespace)
+example : True := by
+                  --^ completion
+
+-- column 20 on nested `by` line (end of `by` token, before whitespace)
+example : True := id <|
+  have : True := by
+                 --^ completion
+
+-- ===== Top-level `by`, non-indented content following =====
+
+-- column 21 on line below `by`
+example : True := by
+                      -- below by
+                   --^ completion
+sorry
+
+-- column 0 on line below `by`
+example : True := by
+   -- below by
+--⬑ completion
+sorry
+
+-- column 2 on line below `by`
+example : True := by
+   -- below by
+--^ completion
+sorry
+
+-- ===== Top-level `by`, no tactics following =====
+
+-- column 21 on line below `by`
+example : True := by
+                      -- below by
+                   --^ completion
+
+-- column 0 on line below `by`
+example : True := by
+   -- below by
+--⬑ completion
+
+-- column 2 on line below `by`
+example : True := by
+   -- below by
+--^ completion
+
+-- ===== Nested `by`, content following =====
+
+-- column 21 on line below `by`
+example : True := id <|
+  have : True := by
+                      -- below by
+                   --^ completion
+  sorry
+
+-- column 2 on line below `by` (at column of `have` line)
+example : True := id <|
+  have : True := by
+     -- below by
+  --^ completion
+  sorry
+
+-- column 0 on line below `by`
+example : True := id <|
+  have : True := by
+   -- below by
+--⬑ completion
+  sorry
+
+-- column 4 on line below `by` (indented past `have` but not past `by`)
+example : True := id <|
+  have : True := by
+       -- below by
+    --^ completion
+  sorry
+
+-- ===== Nested `by`, no tactics following =====
+
+-- column 21 on line below `by`
+example : True := id <|
+  have : True := by
+                      -- below by
+                   --^ completion
+
+-- column 2 on line below `by` (at column of `have` line)
+example : True := id <|
+  have : True := by
+     -- below by
+  --^ completion
+
+-- column 0 on line below `by`
+example : True := id <|
+  have : True := by
+   -- below by
+--⬑ completion
+
+-- column 4 on line below `by`
+example : True := id <|
+  have : True := by
+       -- below by
+    --^ completion