feat: elaborate auxiliary completion node

src/Lean/Elab/App.lean

@@ -803,10 +803,6 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       f.getArgs.foldlM (fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc) acc
   else
     let elabFieldName (e field : Syntax) := do
-      if field.isMissing then
-        let e ← elabTerm e none
-        unless e.isSorry do
-          addDotCompletionInfo f e expectedType?
       let newLVals := field.getId.eraseMacroScopes.components.map fun n =>
         -- We use `none` here since `field` can't be part of a composite name
         LVal.fieldName field (toString n) none e
@@ -817,8 +813,8 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     match f with
     | `($(e).$idx:fieldIdx) => elabFieldIdx e idx
     | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx
-    | `($(e).$field) => elabFieldName e field
-    | `($e |>.$field) => elabFieldName e field
+    | `($(e).$field:ident) => elabFieldName e field
+    | `($e |>.$field:ident) => elabFieldName e field
     | `($e[%$bracket $idx]) => elabAppFn e (LVal.getOp bracket idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     | `($id:ident@$t:term) =>
       throwError "unexpected occurrence of named pattern"

src/Lean/Elab/Term.lean

@@ -1230,13 +1230,16 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
 @[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ =>
   return mkSort (mkLevelSucc (← elabOptLevel stx[1]))
 
-@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab := fun stx expectedType? => do
+@[builtinTermElab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
   let e ← elabTerm stx[0] none
   unless e.isSorry do
     -- dbg_trace "completion {stx} : {expectedType?}"
     addDotCompletionInfo stx e expectedType?
   throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
 
+@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab :=
+  elabCompletion
+
 @[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
   let mvar ← mkFreshExprMVar expectedType?
   registerMVarErrorHoleInfo mvar.mvarId! stx

src/Lean/Server/Completion.lean

@@ -196,6 +196,8 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? :
     | _ =>
       if info.stx.isIdent then
         idCompletionCore ctx info.stx expectedType?
+      else if info.stx.getKind == ``Lean.Parser.Term.completion then
+        idCompletionCore ctx info.stx[0] expectedType?
       else
         failure
 

tests/lean/interactive/completion3.lean

@@ -8,3 +8,15 @@ def f (s : S) : Nat :=
     if s. then 1 else 2
        --^ textDocument/completion
   foo s
+
+def g1 (s : S) : Nat × Nat :=
+  (s. )
+   --^ textDocument/completion
+
+def g2 (s : S) : Nat × Nat :=
+  (s.
+   --^ textDocument/completion
+
+def g3 (s : S) : Nat × Nat :=
+  (s. , 1, 2)
+   --^ textDocument/completion

tests/lean/interactive/completion3.lean.expected.out

@@ -6,3 +6,27 @@
   {"label": "x", "detail": "S → Nat"},
   {"label": "y", "detail": "S → String"}],
  "isIncomplete": true}
+{"textDocument": {"uri": "file://completion3.lean"},
+ "position": {"line": 12, "character": 5}}
+{"items":
+ [{"label": "b", "detail": "S → Bool"},
+  {"label": "mk", "detail": "Nat → String → Bool → S"},
+  {"label": "x", "detail": "S → Nat"},
+  {"label": "y", "detail": "S → String"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion3.lean"},
+ "position": {"line": 16, "character": 5}}
+{"items":
+ [{"label": "b", "detail": "S → Bool"},
+  {"label": "mk", "detail": "Nat → String → Bool → S"},
+  {"label": "x", "detail": "S → Nat"},
+  {"label": "y", "detail": "S → String"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion3.lean"},
+ "position": {"line": 20, "character": 5}}
+{"items":
+ [{"label": "x", "detail": "S → Nat"},
+  {"label": "b", "detail": "S → Bool"},
+  {"label": "mk", "detail": "Nat → String → Bool → S"},
+  {"label": "y", "detail": "S → String"}],
+ "isIncomplete": true}