fix: use sensible notion of indentation in structure instance field c…

…ompletion (#6279)

This PR fixes a bug in structure instance field completion that caused
it to not function correctly for bracketed structure instances written
in Mathlib style.

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -100,20 +100,6 @@ private def findSyntheticIdentifierCompletion?
       HoverInfo.after
   some { hoverInfo, ctx, info := .id stx id danglingDot info.lctx none }
 
-private partial def getIndentationAmount (fileMap : FileMap) (line : Nat) : Nat := Id.run do
-  let lineStartPos := fileMap.lineStart line
-  let lineEndPos := fileMap.lineStart (line + 1)
-  let mut it : String.Iterator := ⟨fileMap.source, lineStartPos⟩
-  let mut indentationAmount := 0
-  while it.pos < lineEndPos do
-    let c := it.curr
-    if c = ' ' || c = '\t' then
-      indentationAmount := indentationAmount + 1
-    else
-      break
-    it := it.next
-  return indentationAmount
-
 private partial def isCursorOnWhitespace (fileMap : FileMap) (hoverPos : String.Pos) : Bool :=
   fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace
 
@@ -127,15 +113,10 @@ private partial def isSyntheticTacticCompletion
     (cmdStx   : Syntax)
     : Bool := Id.run do
   let hoverFilePos := fileMap.toPosition hoverPos
-  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
-  if hoverFilePos.column < hoverLineIndentation then
-    -- Ignore trailing whitespace after the cursor
-    hoverLineIndentation := hoverFilePos.column
-  go hoverFilePos hoverLineIndentation cmdStx 0
+  go hoverFilePos cmdStx 0
 where
   go
       (hoverFilePos : Position)
-      (hoverLineIndentation : Nat)
       (stx : Syntax)
       (leadingWs : Nat)
       : Bool := Id.run do
@@ -148,7 +129,7 @@ where
         return false
       let mut wsBeforeArg := leadingWs
       for arg in stx.getArgs do
-        if go hoverFilePos hoverLineIndentation arg wsBeforeArg then
+        if go hoverFilePos arg wsBeforeArg then
           return true
         -- We must account for the whitespace before an argument because the syntax nodes we use
         -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
@@ -158,7 +139,7 @@ where
         wsBeforeArg := arg.getTrailingSize
       return isCompletionInEmptyTacticBlock stx
         || isCompletionAfterSemicolon stx
-        || isCompletionOnTacticBlockIndentation hoverFilePos hoverLineIndentation stx
+        || isCompletionOnTacticBlockIndentation hoverFilePos stx
     | _, _ =>
       -- Empty tactic blocks typically lack ranges since they do not contain any tokens.
       -- We do not perform more precise range checking in this case because we assume that empty
@@ -169,24 +150,17 @@ where
 
   isCompletionOnTacticBlockIndentation
       (hoverFilePos : Position)
-      (hoverLineIndentation : Nat)
       (stx : Syntax)
       : Bool := Id.run do
-    let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
-    if ! isCursorInIndentation then
-      -- Do not trigger tactic completion at the end of a properly indented tactic block line since
-      -- that line might already have entered term mode by that point.
-      return false
     let some tacticsNode := getTacticsNode? stx
       | return false
     let some firstTacticPos := tacticsNode.getPos?
       | return false
-    let firstTacticLine := fileMap.toPosition firstTacticPos |>.line
-    let firstTacticIndentation := getIndentationAmount fileMap firstTacticLine
+    let firstTacticColumn := fileMap.toPosition firstTacticPos |>.column
     -- This ensures that we do not accidentally provide tactic completions in a term mode proof -
     -- tactic completions are only provided at the same indentation level as the other tactics in
     -- that tactic block.
-    let isCursorInTacticBlock := hoverLineIndentation == firstTacticIndentation
+    let isCursorInTacticBlock := hoverFilePos.column == firstTacticColumn
     return isCursorInProperWhitespace fileMap hoverPos && isCursorInTacticBlock
 
   isCompletionAfterSemicolon (stx : Syntax) : Bool := Id.run do
@@ -315,10 +289,6 @@ private def isSyntheticStructFieldCompletion
     return false
 
   let hoverFilePos := fileMap.toPosition hoverPos
-  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
-  if hoverFilePos.column < hoverLineIndentation then
-    -- Ignore trailing whitespace after the cursor
-    hoverLineIndentation := hoverFilePos.column
 
   return Option.isSome <| findWithLeadingToken? (stx := cmdStx) fun leadingToken? stx => Id.run do
     let some leadingToken := leadingToken?
@@ -355,14 +325,10 @@ private def isSyntheticStructFieldCompletion
     let isCompletionOnIndentation := Id.run do
       if ! isCursorInProperWhitespace then
         return false
-      let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
-      if ! isCursorInIndentation then
-        return false
       let some firstFieldPos := stx.getPos?
         | return false
-      let firstFieldLine := fileMap.toPosition firstFieldPos |>.line
-      let firstFieldIndentation := getIndentationAmount fileMap firstFieldLine
-      let isCursorInBlock := hoverLineIndentation == firstFieldIndentation
+      let firstFieldColumn := fileMap.toPosition firstFieldPos |>.column
+      let isCursorInBlock := hoverFilePos.column == firstFieldColumn
       return isCursorInBlock
     return isCompletionOnIndentation
 

tests/lean/interactive/completionStructureInstance.lean

@@ -74,11 +74,11 @@ example : S := {
 --^ textDocument/completion
 }
 
-example : S := {
-  foo := 1
-    -- All field completions expected
---^ textDocument/completion
-}
+example : S :=
+  { foo := 1
+     } -- All field completions expected
+  --^ textDocument/completion
+
 
 example : S := { foo := 1,  } -- All field completions expected
                          --^ textDocument/completion

tests/lean/interactive/completionStructureInstance.lean.expected.out

@@ -416,7 +416,7 @@
     "cPos": 0}}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
- "position": {"line": 78, "character": 2}}
+ "position": {"line": 78, "character": 4}}
 {"items":
  [{"sortText": "0",
    "label": "bar",
@@ -425,7 +425,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 2}},
+     "position": {"line": 78, "character": 4}},
     "cPos": 0}},
   {"sortText": "1",
    "label": "barfoo",
@@ -434,7 +434,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 2}},
+     "position": {"line": 78, "character": 4}},
     "cPos": 0}},
   {"sortText": "2",
    "label": "foo",
@@ -443,7 +443,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 2}},
+     "position": {"line": 78, "character": 4}},
     "cPos": 0}},
   {"sortText": "3",
    "label": "foobar",
@@ -452,7 +452,7 @@
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionStructureInstance.lean"},
-     "position": {"line": 78, "character": 2}},
+     "position": {"line": 78, "character": 4}},
     "cPos": 0}}],
  "isIncomplete": true}
 {"textDocument": {"uri": "file:///completionStructureInstance.lean"},

tests/lean/interactive/completionTactics.lean

@@ -113,3 +113,8 @@ example : True := by {
     -- All tactic completions expected
 --^ textDocument/completion
 }
+
+example : True := by
+  { skip -- All tactic completions expected
+     }
+  --^ textDocument/completion

tests/lean/interactive/completionTactics.lean.expected.out

@@ -1472,3 +1472,89 @@
      "position": {"line": 112, "character": 2}},
     "cPos": 0}}],
  "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 118, "character": 4}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.match",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.open",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.set_option",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}},
+  {"sortText": "7",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 118, "character": 4}},
+    "cPos": 0}}],
+ "isIncomplete": true}