diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index ef8485ed0b..60d5eadccc 100644 --- a/src/Lean/Elab/App.lean +++ b/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" diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 12c3849a68..3ae3007df4 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index e5b24ac926..c22665265a 100644 --- a/src/Lean/Server/Completion.lean +++ b/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 diff --git a/tests/lean/interactive/completion3.lean b/tests/lean/interactive/completion3.lean index 6a8c35a779..fd381c4ff3 100644 --- a/tests/lean/interactive/completion3.lean +++ b/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 diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out index 36a7274219..6aeffd3c63 100644 --- a/tests/lean/interactive/completion3.lean.expected.out +++ b/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}