From 8488ef6655e05a6692e5341f8a72f560cee3d22e Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 16 Feb 2024 17:06:54 +0100 Subject: [PATCH 1/4] fix: auto-completion bugs and performance --- src/Lean/Data/Lsp/LanguageFeatures.lean | 6 +- src/Lean/Elab/BuiltinCommand.lean | 4 +- src/Lean/Elab/BuiltinTerm.lean | 5 +- src/Lean/Elab/InfoTree/Main.lean | 21 +- src/Lean/Meta/CompletionName.lean | 12 +- src/Lean/Modifiers.lean | 2 +- src/Lean/Server/Completion.lean | 503 +++++++++++++----- src/Lean/Server/CompletionItemData.lean | 28 + src/Lean/Server/FileWorker.lean | 2 + .../Server/FileWorker/RequestHandling.lean | 105 +++- src/Lean/Server/ImportCompletion.lean | 16 +- src/Lean/Server/Requests.lean | 17 +- src/Lean/Server/Watchdog.lean | 1 + tests/lean/interactive/1265.lean.expected.out | 182 +++++-- tests/lean/interactive/1659.lean.expected.out | 117 +++- tests/lean/interactive/533.lean.expected.out | 18 +- tests/lean/interactive/863.lean.expected.out | 36 +- .../interactive/compHeader.lean.expected.out | 18 +- .../compNamespace.lean.expected.out | 49 +- .../interactive/completion.lean.expected.out | 40 +- .../interactive/completion2.lean.expected.out | 135 ++++- .../interactive/completion3.lean.expected.out | 108 +++- .../interactive/completion4.lean.expected.out | 108 +++- .../interactive/completion5.lean.expected.out | 27 +- .../interactive/completion6.lean.expected.out | 99 +++- .../interactive/completion7.lean.expected.out | 37 +- .../completionAtPrint.lean.expected.out | 18 +- tests/lean/interactive/completionCheck.lean | 8 + .../completionCheck.lean.expected.out | 20 + .../completionDocString.lean.expected.out | 18 +- .../completionEOF.lean.expected.out | 10 +- .../completionFromExpectedType.lean | 5 + ...mpletionFromExpectedType.lean.expected.out | 12 + .../completionIStr.lean.expected.out | 27 +- .../interactive/completionOpenNamespaces.lean | 6 + ...completionOpenNamespaces.lean.expected.out | 13 + .../completionOption.lean.expected.out | 217 ++++++-- .../completionPrefixIssue.lean.expected.out | 18 +- .../interactive/completionPrivateTypes.lean | 5 + .../completionPrivateTypes.lean.expected.out | 12 + .../completionPrv.lean.expected.out | 64 ++- .../dotIdCompletion.lean.expected.out | 18 +- .../editCompletion.lean.expected.out | 10 +- .../inWordCompletion.lean.expected.out | 54 +- .../internalNamesIssue.lean.expected.out | 18 +- .../keywordCompletion.lean.expected.out | 64 ++- .../lean/interactive/match.lean.expected.out | 54 +- .../matchStxCompletion.lean.expected.out | 27 +- 48 files changed, 2016 insertions(+), 378 deletions(-) create mode 100644 src/Lean/Server/CompletionItemData.lean create mode 100644 tests/lean/interactive/completionCheck.lean create mode 100644 tests/lean/interactive/completionCheck.lean.expected.out create mode 100644 tests/lean/interactive/completionFromExpectedType.lean create mode 100644 tests/lean/interactive/completionFromExpectedType.lean.expected.out create mode 100644 tests/lean/interactive/completionOpenNamespaces.lean create mode 100644 tests/lean/interactive/completionOpenNamespaces.lean.expected.out create mode 100644 tests/lean/interactive/completionPrivateTypes.lean create mode 100644 tests/lean/interactive/completionPrivateTypes.lean.expected.out diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index ab1c6602ec17..95fbb07e3a66 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -47,19 +47,19 @@ structure CompletionItem where documentation? : Option MarkupContent := none kind? : Option CompletionItemKind := none textEdit? : Option InsertReplaceEdit := none + sortText? : Option String := none + data? : Option Json := none /- tags? : CompletionItemTag[] deprecated? : boolean preselect? : boolean - sortText? : string filterText? : string insertText? : string insertTextFormat? : InsertTextFormat insertTextMode? : InsertTextMode additionalTextEdits? : TextEdit[] commitCharacters? : string[] - command? : Command - data? : any -/ + command? : Command -/ deriving FromJson, ToJson, Inhabited structure CompletionList where diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 4c052b138d56..472d15a463d0 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -534,10 +534,10 @@ open Meta def elabCheckCore (ignoreStuckTC : Bool) : CommandElab | `(#check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do -- show signature for `#check id`/`#check @id` - if let `($_:ident) := term then + if let `($id:ident) := term then try for c in (← resolveGlobalConstWithInfos term) do - addCompletionInfo <| .id term c (danglingDot := false) {} none + addCompletionInfo <| .id term id.getId (danglingDot := false) {} none logInfoAt tk <| .ofPPFormat { pp := fun | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c | none => return f!"{c}" -- should never happen diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 64913174fda0..4600760c3b09 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -158,7 +158,10 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? => elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?) -@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun _ _ => +@[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun stx expectedType? => do + if let `(.) := stx then + -- Users may input bad cdots because they are trying to auto-complete them using the expected type + addCompletionInfo <| CompletionInfo.dotId stx .anonymous (← getLCtx) expectedType? throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)" @[builtin_term_elab str] def elabStrLit : TermElab := fun stx _ => do diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index ee05df339993..f0138fb71351 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -49,14 +49,21 @@ def PartialContextInfo.mergeIntoOuter? some { outer with parentDecl? := innerParentDecl } def CompletionInfo.stx : CompletionInfo → Syntax - | dot i .. => i.stx - | id stx .. => stx - | dotId stx .. => stx - | fieldId stx .. => stx - | namespaceId stx => stx - | option stx => stx + | dot i .. => i.stx + | id stx .. => stx + | dotId stx .. => stx + | fieldId stx .. => stx + | namespaceId stx => stx + | option stx => stx | endSection stx .. => stx - | tactic stx .. => stx + | tactic stx .. => stx + +def CompletionInfo.lctx : CompletionInfo → LocalContext + | dot i .. => i.lctx + | id _ _ _ lctx .. => lctx + | dotId _ _ lctx .. => lctx + | fieldId _ _ lctx .. => lctx + | _ => .empty def CustomInfo.format : CustomInfo → Format | i => f!"CustomInfo({i.value.typeName})" diff --git a/src/Lean/Meta/CompletionName.lean b/src/Lean/Meta/CompletionName.lean index c83e33f5b3e2..fcaf01e42669 100644 --- a/src/Lean/Meta/CompletionName.lean +++ b/src/Lean/Meta/CompletionName.lean @@ -29,11 +29,21 @@ builtin_initialize completionBlackListExt : TagDeclarationExtension ← mkTagDec def addToCompletionBlackList (env : Environment) (declName : Name) : Environment := completionBlackListExt.tag env declName +/-- +Checks whether a given name is internal due to something other than `_private`. +Correctly deals with names like `_private..0.._sizeOf_1` in a private type +`SomeType`, which `n.isInternal && !isPrivateName n` does not. +-/ +private def isNonPrivateInternalName : Name → Bool + | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isNonPrivateInternalName p + | .num p _ => isNonPrivateInternalName p + | _ => false + /-- Return true if name is blacklisted for completion purposes. -/ private def isBlacklisted (env : Environment) (declName : Name) : Bool := - declName.isInternal && !isPrivateName declName + isNonPrivateInternalName declName || isAuxRecursor env declName || isNoConfusion env declName || isRecCore env declName diff --git a/src/Lean/Modifiers.lean b/src/Lean/Modifiers.lean index 66674b4c619a..9c5440efdebc 100644 --- a/src/Lean/Modifiers.lean +++ b/src/Lean/Modifiers.lean @@ -47,7 +47,7 @@ def isPrivateNameExport (n : Name) : Bool := Return `true` if `n` is of the form `_private..0` See comment above. -/ -private def isPrivatePrefix (n : Name) : Bool := +def isPrivatePrefix (n : Name) : Bool := match n with | .num p 0 => go p | _ => false diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 926217b40802..c53aa20e7162 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -15,62 +15,141 @@ import Lean.Meta.Tactic.Apply import Lean.Meta.Match.MatcherInfo import Lean.Server.InfoUtils import Lean.Parser.Extension +import Lean.Server.FileSource +import Lean.Server.CompletionItemData -namespace Lean.Server.Completion -open Lsp -open Elab -open Meta -open FuzzyMatching - -private partial def consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do +private partial def Lean.Server.Completion.consumeImplicitPrefix (e : Expr) (k : Expr → MetaM α) : MetaM α := do match e with | Expr.forallE n d b c => -- We do not consume instance implicit arguments because the user probably wants be aware of this dependency if c == .implicit then - withLocalDecl n c d fun arg => + Meta.withLocalDecl n c d fun arg => consumeImplicitPrefix (b.instantiate1 arg) k else k e | _ => k e -private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM Bool := - try - match expectedType? with - | none => return true - | some expectedType => - let mut (numArgs, hasMVarHead) ← getExpectedNumArgsAux type - unless hasMVarHead do - let targetTypeNumArgs ← getExpectedNumArgs expectedType - numArgs := numArgs - targetTypeNumArgs - let (_, _, type) ← forallMetaTelescopeReducing type (some numArgs) - -- TODO take coercions into account - -- We use `withReducible` to make sure we don't spend too much time unfolding definitions - -- Alternative: use default and small number of heartbeats - withReducible <| withoutModifyingState <| isDefEq type expectedType - catch _ => - return false +namespace Lean.Lsp + +inductive CompletionIdentifier where + | const (declName : Name) + | fvar (id : FVarId) + +instance : ToJson CompletionIdentifier where + toJson + | .const declName => Json.mkObj [("const", toJson declName)] + | .fvar id => Json.mkObj [("fvar", toJson id)] + +instance : FromJson CompletionIdentifier where + fromJson? j := do + if let .ok declName := j.getObjValAs? Name "const" then + return .const declName + if let .ok id := j.getObjValAs? FVarId "fvar" then + return .fvar id + .error "invalid CompletionItemData" + +structure CompletionItemDataWithId where + params : CompletionParams + id? : Option CompletionIdentifier + deriving FromJson, ToJson + +def CompletionItem.resolve + (item : CompletionItem) + (id : CompletionIdentifier) + : MetaM CompletionItem := do + let env ← getEnv + let lctx ← getLCtx + let mut item := item -private def sortCompletionItems (items : Array (CompletionItem × Float)) : Array CompletionItem := - items.qsort (fun (i1, s1) (i2, s2) => if s1 == s2 then i1.label < i2.label else s1 > s2) |>.map (·.1) + if item.detail?.isNone then + let type? := match id with + | .const declName => + env.find? declName |>.map ConstantInfo.type + | .fvar id => + lctx.find? id |>.map LocalDecl.type + let detail? ← type?.mapM fun type => + Lean.Server.Completion.consumeImplicitPrefix type fun typeWithoutImplicits => + return toString (← Meta.ppExpr typeWithoutImplicits) + item := { item with detail? := detail? } -private def mkCompletionItem (label : Name) (type : Expr) (docString? : Option String) (kind : CompletionItemKind) : MetaM CompletionItem := do - let doc? := docString?.map fun docString => { value := docString, kind := MarkupKind.markdown : MarkupContent } - let detail ← consumeImplicitPrefix type fun type => return toString (← Meta.ppExpr type) - return { label := label.toString, detail? := detail, documentation? := doc?, kind? := kind } + return item -structure State where - itemsMain : Array (CompletionItem × Float) := #[] - itemsOther : Array (CompletionItem × Float) := #[] +end Lean.Lsp + +namespace Lean.Server.Completion +open Lsp +open Elab +open Meta +open FuzzyMatching -abbrev M := OptionT $ StateRefT State MetaM +builtin_initialize eligibleHeaderDeclsRef : IO.Ref (HashMap Name ConstantInfo) ← IO.mkRef {} -private def addCompletionItem (label : Name) (type : Expr) (expectedType? : Option Expr) (declName? : Option Name) (kind : CompletionItemKind) (score : Float) : M Unit := do - let docString? ← if let some declName := declName? then findDocString? (← getEnv) declName else pure none - let item ← mkCompletionItem label type docString? kind - if (← isTypeApplicable type expectedType?) then - modify fun s => { s with itemsMain := s.itemsMain.push (item, score) } - else - modify fun s => { s with itemsOther := s.itemsOther.push (item, score) } +def fillEligibleHeaderDecls (headerEnv : Environment) : IO Unit := do + eligibleHeaderDeclsRef.modify fun startEligibleHeaderDecls => + (·.2) <| StateT.run (m := Id) (s := startEligibleHeaderDecls) do + headerEnv.constants.forM fun declName c => do + modify fun eligibleHeaderDecls => + if allowCompletion headerEnv declName then + eligibleHeaderDecls.insert declName c + else + eligibleHeaderDecls + +private def forEligibleDeclsM [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] + (f : Name → ConstantInfo → m PUnit) : m PUnit := do + let env ← getEnv + (← eligibleHeaderDeclsRef.get).forM f + -- map₂ are exactly the local decls + env.constants.map₂.forM fun name c => do + if allowCompletion env name then + f name c + +private def allowCompletion [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] + (declName : Name) : m Bool := do + let env ← getEnv + if (← eligibleHeaderDeclsRef.get).contains declName then + return true + if env.constants.map₂.contains declName && Lean.Meta.allowCompletion env declName then + return true + return false + +private def sortCompletionItems (items : Array (CompletionItem × Float)) : Array CompletionItem := + let items := items.qsort fun (i1, s1) (i2, s2) => + if s1 != s2 then + s1 > s2 + else + i1.label.map (·.toLower) < i2.label.map (·.toLower) + items.map (·.1) + +structure State where + items : Array (CompletionItem × Float) := #[] + +abbrev M := OptionT $ ReaderT CompletionParams $ StateRefT State MetaM + +private def addItem + (item : CompletionItem) + (score : Float) + (id? : Option CompletionIdentifier := none) + : M Unit := do + let params ← read + let data := { params, id? : CompletionItemDataWithId } + let item := { item with data? := toJson data } + modify fun s => { s with items := s.items.push (item, score) } + +private def addUnresolvedCompletionItem + (label : Name) + (id : CompletionIdentifier) + (kind : CompletionItemKind) + (score : Float) + : M Unit := do + let doc? ← do + match id with + | .const declName => + let docString? ← findDocString? (← getEnv) declName + pure <| docString?.map fun docString => + { value := docString, kind := MarkupKind.markdown : MarkupContent } + | .fvar _ => pure none + let item := { label := label.toString, kind? := kind, documentation? := doc? } + addItem item score id private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do let env ← getEnv @@ -90,24 +169,25 @@ private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionIt else return CompletionItemKind.constant -private def addCompletionItemForDecl (label : Name) (declName : Name) (expectedType? : Option Expr) (score : Float) : M Unit := do +private def addUnresolvedCompletionItemForDecl (label : Name) (declName : Name) (score : Float) : M Unit := do if let some c := (← getEnv).find? declName then - addCompletionItem label c.type expectedType? (some declName) (← getCompletionKindForDecl c) score + addUnresolvedCompletionItem label (.const declName) (← getCompletionKindForDecl c) score -private def addKeywordCompletionItem (keyword : String) : M Unit := do +private def addKeywordCompletionItem (keyword : String) (score : Float) : M Unit := do let item := { label := keyword, detail? := "keyword", documentation? := none, kind? := CompletionItemKind.keyword } - modify fun s => { s with itemsMain := s.itemsMain.push (item, 1) } + addItem item score private def addNamespaceCompletionItem (ns : Name) (score : Float) : M Unit := do let item := { label := ns.toString, detail? := "namespace", documentation? := none, kind? := CompletionItemKind.module } - modify fun s => { s with itemsMain := s.itemsMain.push (item, score) } + addItem item score -private def runM (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) : IO (Option CompletionList) := +private def runM (params : CompletionParams) (ctx : ContextInfo) (lctx : LocalContext) (x : M Unit) + : IO (Option CompletionList) := ctx.runMetaM lctx do - match (← x.run |>.run {}) with + match (← x.run |>.run params |>.run {}) with | (none, _) => return none | (some _, s) => - return some { items := sortCompletionItems s.itemsMain ++ sortCompletionItems s.itemsOther, isIncomplete := true } + return some { items := sortCompletionItems s.items, isIncomplete := true } private def matchAtomic (id : Name) (declName : Name) : Option Float := match id, declName with @@ -217,7 +297,12 @@ def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M | _ => return () visitNamespaces ctx.currNamespace -private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) (expectedType? : Option Expr) : M Unit := do +private def idCompletionCore + (ctx : ContextInfo) + (id : Name) + (hoverInfo : HoverInfo) + (danglingDot : Bool) + : M Unit := do let mut id := id.eraseMacroScopes let mut danglingDot := danglingDot if let HoverInfo.inside delta := hoverInfo then @@ -228,35 +313,40 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI -- search for matches in the local context for localDecl in (← getLCtx) do if let some score := matchAtomic id localDecl.userName then - addCompletionItem localDecl.userName localDecl.type expectedType? none (kind := CompletionItemKind.variable) score + addUnresolvedCompletionItem localDecl.userName (.fvar localDecl.fvarId) (kind := CompletionItemKind.variable) score -- search for matches in the environment let env ← getEnv - env.constants.forM fun declName c => do - if allowCompletion env declName then - let matchUsingNamespace (ns : Name): M Bool := do - if let some (label, score) ← matchDecl? ns id danglingDot declName then - -- dbg_trace "matched with {id}, {declName}, {label}" - addCompletionItem label c.type expectedType? declName (← getCompletionKindForDecl c) score - return true - else - return false + forEligibleDeclsM fun declName c => do + let bestMatch? ← (·.2) <$> StateT.run (s := none) do + let matchUsingNamespace (ns : Name) : StateT (Option (Name × Float)) M Unit := do + let some (label, score) ← matchDecl? ns id danglingDot declName + | return + modify fun + | none => + some (label, score) + | some (bestLabel, bestScore) => + -- for open namespaces `A` and `A.B` and a decl `A.B.c`, pick the decl `c` over `B.c` + if label.isSuffixOf bestLabel then + some (label, score) + else + some (bestLabel, bestScore) + let rec visitNamespaces (ns : Name) : StateT (Option (Name × Float)) M Unit := do + let Name.str p .. := ns + | return () + matchUsingNamespace ns + visitNamespaces p -- use current namespace - let rec visitNamespaces (ns : Name) : M Bool := do - match ns with - | Name.str p .. => matchUsingNamespace ns <||> visitNamespaces p - | _ => return false - if (← visitNamespaces ctx.currNamespace) then - return () + visitNamespaces ctx.currNamespace -- use open decls for openDecl in ctx.openDecls do - match openDecl with - | OpenDecl.simple ns exs => - unless exs.contains declName do - if (← matchUsingNamespace ns) then - return () - | _ => pure () - if (← matchUsingNamespace Name.anonymous) then - return () + let OpenDecl.simple ns exs := openDecl + | pure () + if exs.contains declName then + continue + matchUsingNamespace ns + matchUsingNamespace Name.anonymous + if let some (bestLabel, bestScore) := bestMatch? then + addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) bestScore -- Recall that aliases may not be atomic and include the namespace where they were created. let matchAlias (ns : Name) (alias : Name) : Option Float := if ns.isPrefixOf alias then @@ -266,15 +356,15 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI -- Auxiliary function for `alias` let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do declNames.forM fun declName => do - if allowCompletion env declName then - addCompletionItemForDecl alias.getString! declName expectedType? score + if ← allowCompletion declName then + addUnresolvedCompletionItemForDecl alias.getString! declName score -- search explicitly open `ids` for openDecl in ctx.openDecls do match openDecl with | OpenDecl.explicit openedId resolvedId => - if allowCompletion env resolvedId then + if ← allowCompletion resolvedId then if let some score := matchAtomic id openedId then - addCompletionItemForDecl openedId.getString! resolvedId expectedType? score + addUnresolvedCompletionItemForDecl openedId.getString! resolvedId score | OpenDecl.simple ns _ => getAliasState env |>.forM fun alias declNames => do if let some score := matchAlias ns alias then @@ -294,20 +384,31 @@ private def idCompletionCore (ctx : ContextInfo) (id : Name) (hoverInfo : HoverI if let .str .anonymous s := id then let keywords := Parser.getTokenTable env for keyword in keywords.findPrefix s do - addKeywordCompletionItem keyword + if let some score := fuzzyMatchScoreWithThreshold? s keyword then + addKeywordCompletionItem keyword score -- Search namespaces completeNamespaces ctx id danglingDot -private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (id : Name) (hoverInfo : HoverInfo) (danglingDot : Bool) (expectedType? : Option Expr) : IO (Option CompletionList) := - runM ctx lctx do - idCompletionCore ctx id hoverInfo danglingDot expectedType? +private def idCompletion + (params : CompletionParams) + (ctx : ContextInfo) + (lctx : LocalContext) + (id : Name) + (hoverInfo : HoverInfo) + (danglingDot : Bool) + : IO (Option CompletionList) := + runM params ctx lctx do + idCompletionCore ctx id hoverInfo danglingDot private def unfoldeDefinitionGuarded? (e : Expr) : MetaM (Option Expr) := try unfoldDefinition? e catch _ => pure none /-- Return `true` if `e` is a `declName`-application, or can be unfolded (delta-reduced) to one. -/ private partial def isDefEqToAppOf (e : Expr) (declName : Name) : MetaM Bool := do - if e.getAppFn.isConstOf declName then + let isConstOf := match e.getAppFn with + | .const name .. => (privateToUserName? name).getD name == declName + | _ => false + if isConstOf then return true let some e ← unfoldeDefinitionGuarded? e | return false isDefEqToAppOf e declName @@ -321,14 +422,43 @@ private def isDotCompletionMethod (typeName : Name) (info : ConstantInfo) : Meta return true return false +private def isDotIdCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool := do + forallTelescopeReducing info.type fun _ type => + isDefEqToAppOf type.consumeMData typeName + +private def stripPrivatePrefix (n : Name) : Name := + match n with + | .num _ 0 => if isPrivatePrefix n then .anonymous else n + | _ => n + +partial def cmpModPrivate (n₁ n₂ : Name) : Ordering := + let n₁ := stripPrivatePrefix n₁ + let n₂ := stripPrivatePrefix n₂ + match n₁, n₂ with + | .anonymous, .anonymous => Ordering.eq + | .anonymous, _ => Ordering.lt + | _, .anonymous => Ordering.gt + | .num p₁ i₁, .num p₂ i₂ => + match compare i₁ i₂ with + | Ordering.eq => cmpModPrivate p₁ p₂ + | ord => ord + | .num _ _, .str _ _ => Ordering.lt + | .str _ _, .num _ _ => Ordering.gt + | .str p₁ n₁, .str p₂ n₂ => + match compare n₁ n₂ with + | Ordering.eq => cmpModPrivate p₁ p₂ + | ord => ord + +def NameSetModPrivate := RBTree Name cmpModPrivate + /-- Given a type, try to extract relevant type names for dot notation field completion. We extract the type name, parent struct names, and unfold the type. The process mimics the dot notation elaboration procedure at `App.lean` -/ -private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSet := - return (← visit type |>.run {}).2 +private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSetModPrivate := + return (← visit type |>.run RBTree.empty).2 where - visit (type : Expr) : StateRefT NameSet MetaM Unit := do + visit (type : Expr) : StateRefT NameSetModPrivate MetaM Unit := do let .const typeName _ := type.getAppFn | return () modify fun s => s.insert typeName if isStructure (← getEnv) typeName then @@ -337,49 +467,104 @@ where let some type ← unfoldeDefinitionGuarded? type | return () visit type -private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (hoverInfo : HoverInfo) (expectedType? : Option Expr) : IO (Option CompletionList) := - runM ctx info.lctx do +private def dotCompletion + (params : CompletionParams) + (ctx : ContextInfo) + (info : TermInfo) + (hoverInfo : HoverInfo) + : IO (Option CompletionList) := + runM params ctx info.lctx do let nameSet ← try getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr)) catch _ => - pure {} + pure RBTree.empty + if nameSet.isEmpty then - if info.stx.isIdent then - idCompletionCore ctx info.stx.getId hoverInfo (danglingDot := false) expectedType? - else if info.stx.getKind == ``Lean.Parser.Term.completion && info.stx[0].isIdent then + let stx := info.stx + if stx.isIdent then + idCompletionCore ctx stx.getId hoverInfo (danglingDot := false) + else if stx.getKind == ``Lean.Parser.Term.completion && stx[0].isIdent then -- TODO: truncation when there is a dangling dot - idCompletionCore ctx info.stx[0].getId HoverInfo.after (danglingDot := true) expectedType? + idCompletionCore ctx stx[0].getId HoverInfo.after (danglingDot := true) else failure - else - (← getEnv).constants.forM fun declName c => do - let some declName ← normPrivateName? declName - | return - let typeName := declName.getPrefix - if nameSet.contains typeName then - if allowCompletion (←getEnv) c.name && (← isDotCompletionMethod typeName c) then - addCompletionItem c.name.getString! c.type expectedType? c.name (kind := (← getCompletionKindForDecl c)) 1 - -private def dotIdCompletion (ctx : ContextInfo) (lctx : LocalContext) (id : Name) (expectedType? : Option Expr) : IO (Option CompletionList) := - runM ctx lctx do - let some expectedType := expectedType? | return () - let resultTypeFn := (← instantiateMVars expectedType).cleanupAnnotations.getAppFn - let .const typeName .. := resultTypeFn.cleanupAnnotations | return () - (← getEnv).constants.forM fun declName c => do - let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure () - addCompletionItem label c.type expectedType? declName (← getCompletionKindForDecl c) score + return + + forEligibleDeclsM fun declName c => do + let unnormedTypeName := declName.getPrefix + if ! nameSet.contains unnormedTypeName then + return + let some declName ← normPrivateName? declName + | return + let typeName := declName.getPrefix + if ! (← isDotCompletionMethod typeName c) then + return + let completionKind ← getCompletionKindForDecl c + addUnresolvedCompletionItem c.name.getString! (.const c.name) (kind := completionKind) 1 + +private def dotIdCompletion + (params : CompletionParams) + (ctx : ContextInfo) + (lctx : LocalContext) + (id : Name) + (expectedType? : Option Expr) + : IO (Option CompletionList) := + runM params ctx lctx do + let some expectedType := expectedType? + | return () + + let resultTypeFn := (← instantiateMVars expectedType).cleanupAnnotations.getAppFn.cleanupAnnotations + let .const .. := resultTypeFn + | return () + + let nameSet ← try + getDotCompletionTypeNames resultTypeFn + catch _ => + pure RBTree.empty -private def fieldIdCompletion (ctx : ContextInfo) (lctx : LocalContext) (id : Name) (structName : Name) : IO (Option CompletionList) := - runM ctx lctx do + forEligibleDeclsM fun declName c => do + let unnormedTypeName := declName.getPrefix + if ! nameSet.contains unnormedTypeName then + return + + let some declName ← normPrivateName? declName + | return + + let typeName := declName.getPrefix + if ! (← isDotIdCompletionMethod typeName c) then + return + + let completionKind ← getCompletionKindForDecl c + if id.isAnonymous then + -- We're completing a lone dot => offer all decls of the type + addUnresolvedCompletionItem c.name.getString! (.const c.name) completionKind 1 + return + + let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure () + addUnresolvedCompletionItem label (.const c.name) completionKind score + +private def fieldIdCompletion + (params : CompletionParams) + (ctx : ContextInfo) + (lctx : LocalContext) + (id : Name) + (structName : Name) + : IO (Option CompletionList) := + runM params ctx lctx do let idStr := id.toString let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false) for fieldName in fieldNames do let .str _ fieldName := fieldName | continue let some score := fuzzyMatchScoreWithThreshold? idStr fieldName | continue let item := { label := fieldName, detail? := "field", documentation? := none, kind? := CompletionItemKind.field } - modify fun s => { s with itemsMain := s.itemsMain.push (item, score) } - -private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCapabilities) : IO (Option CompletionList) := + addItem item score + +private def optionCompletion + (params : CompletionParams) + (ctx : ContextInfo) + (stx : Syntax) + (caps : ClientCapabilities) + : IO (Option CompletionList) := ctx.runMetaM {} do let (partialName, trailingDot) := -- `stx` is from `"set_option" >> ident` @@ -411,35 +596,44 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCa detail? := s!"({opts.get name decl.defValue}), {decl.descr}" documentation? := none, kind? := CompletionItemKind.property -- TODO: investigate whether this is the best kind for options. - textEdit? := textEdit }, score) + textEdit? := textEdit + data? := toJson { params, id? := none : CompletionItemDataWithId } }, score) return some { items := sortCompletionItems items, isIncomplete := true } -private def tacticCompletion (ctx : ContextInfo) : IO (Option CompletionList) := +private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : IO (Option CompletionList) := -- Just return the list of tactics for now. ctx.runMetaM {} do let table := Parser.getCategory (Parser.parserExtension.getState (← getEnv)).categories `tactic |>.get!.tables.leadingTable let items : Array (CompletionItem × Float) := table.fold (init := #[]) fun items tk _ => -- TODO pretty print tactic syntax - items.push ({ label := tk.toString, detail? := none, documentation? := none, kind? := CompletionItemKind.keyword }, 1) + items.push ({ + label := tk.toString + detail? := none + documentation? := none + kind? := CompletionItemKind.keyword + data? := toJson { params, id? := none : CompletionItemDataWithId } + }, 1) return some { items := sortCompletionItems items, isIncomplete := true } -partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) (caps : ClientCapabilities) : IO (Option CompletionList) := do +private def findCompletionInfoAt? + (fileMap : FileMap) + (hoverPos : String.Pos) + (infoTree : InfoTree) + : Option (HoverInfo × ContextInfo × CompletionInfo) := let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos - match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with + match infoTree.foldInfo (init := none) (choose hoverLine) with | some (hoverInfo, ctx, Info.ofCompletionInfo info) => - match info with - | .dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType? - | .id _ id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType? - | .dotId _ id lctx expectedType? => dotIdCompletion ctx lctx id expectedType? - | .fieldId _ id lctx structName => fieldIdCompletion ctx lctx id structName - | .option stx => optionCompletion ctx stx caps - | .tactic .. => tacticCompletion ctx - | _ => return none + some (hoverInfo, ctx, info) | _ => -- TODO try to extract id from `fileMap` and some `ContextInfo` from `InfoTree` - return none + none where - choose (fileMap : FileMap) (hoverLine : Nat) (ctx : ContextInfo) (info : Info) (best? : Option (HoverInfo × ContextInfo × Info)) : Option (HoverInfo × ContextInfo × Info) := + choose + (hoverLine : Nat) + (ctx : ContextInfo) + (info : Info) + (best? : Option (HoverInfo × ContextInfo × Info)) + : Option (HoverInfo × ContextInfo × Info) := if !info.isCompletion then best? else if info.occursInside? hoverPos |>.isSome then let headPos := info.pos?.get! @@ -473,4 +667,53 @@ where else best? +private def assignSortTexts (completions : CompletionList) : CompletionList := Id.run do + if completions.items.isEmpty then + return completions + let items := completions.items.mapIdx fun i item => + { item with sortText? := toString i.val } + let maxDigits := items[items.size - 1]!.sortText?.get!.length + let items := items.map fun item => + let sortText := item.sortText?.get! + let pad := List.replicate (maxDigits - sortText.length) '0' |>.asString + { item with sortText? := pad ++ sortText } + { completions with items := items } + +partial def find? + (params : CompletionParams) + (fileMap : FileMap) + (hoverPos : String.Pos) + (infoTree : InfoTree) + (caps : ClientCapabilities) + : IO (Option CompletionList) := do + let some (hoverInfo, ctx, info) := findCompletionInfoAt? fileMap hoverPos infoTree + | return none + let completionList? ← + match info with + | .dot info .. => + dotCompletion params ctx info hoverInfo + | .id _ id danglingDot lctx .. => + idCompletion params ctx lctx id hoverInfo danglingDot + | .dotId _ id lctx expectedType? => + dotIdCompletion params ctx lctx id expectedType? + | .fieldId _ id lctx structName => + fieldIdCompletion params ctx lctx id structName + | .option stx => + optionCompletion params ctx stx caps + | .tactic .. => + tacticCompletion params ctx + | _ => return none + return completionList?.map assignSortTexts + +def resolveCompletionItem? + (fileMap : FileMap) + (hoverPos : String.Pos) + (infoTree : InfoTree) + (item : CompletionItem) + (id : CompletionIdentifier) + : IO CompletionItem := do + let some (_, ctx, info) := findCompletionInfoAt? fileMap hoverPos infoTree + | return item + ctx.runMetaM info.lctx (item.resolve id) + end Lean.Server.Completion diff --git a/src/Lean/Server/CompletionItemData.lean b/src/Lean/Server/CompletionItemData.lean new file mode 100644 index 000000000000..160d6ebe4e23 --- /dev/null +++ b/src/Lean/Server/CompletionItemData.lean @@ -0,0 +1,28 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Marc Huisinga +-/ +import Lean.Server.FileSource + +namespace Lean.Lsp + +/-- Used in `CompletionItem.data?`. -/ +structure CompletionItemData where + params : CompletionParams + deriving FromJson, ToJson + +def CompletionItem.getFileSource! (item : CompletionItem) : DocumentUri := + let r : Except String DocumentUri := do + let some data := item.data? + | throw s!"no data param on completion item {item.label}" + let data : CompletionItemData ← fromJson? data + return data.params.textDocument.uri + match r with + | Except.ok uri => uri + | Except.error e => panic! e + +instance : FileSource CompletionItem where + fileSource := CompletionItem.getFileSource! + +end Lean.Lsp diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 206c512c555a..4aa9314f1fd5 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -231,6 +231,8 @@ section Initialization publishDiagnostics m #[progressDiagnostic] hOut let fileSetupResult := fileSetupResult.addGlobalOptions globalOptions let (headerEnv, envMsgLog) ← buildHeaderEnv m headerStx fileSetupResult + -- Prepare header-based caches that requests may use + runHeaderCachingHandlers headerEnv let headerMsgLog := parseMsgLog.append envMsgLog let cmdState := buildCommandState m headerStx headerEnv headerMsgLog fileSetupResult.fileOptions let headerSnap := { diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 8689c0b7f4c2..99d537882bbd 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -38,10 +38,25 @@ def handleCompletion (p : CompletionParams) (notFoundX := pure { items := #[], isIncomplete := true }) (abortedX := -- work around https://github.com/microsoft/vscode/issues/155738 - pure { items := #[{label := "-"}], isIncomplete := true }) fun snap => do - if let some r ← Completion.find? doc.meta.text pos snap.infoTree caps then + pure { items := #[{label := "-"}], isIncomplete := true }) + (x := fun snap => do + if let some r ← Completion.find? p doc.meta.text pos snap.infoTree caps then return r - return { items := #[ ], isIncomplete := true } + return { items := #[ ], isIncomplete := true }) + +def handleCompletionItemResolve (item : CompletionItem) + : RequestM (RequestTask CompletionItem) := do + let doc ← readDoc + let text := doc.meta.text + let some (data : CompletionItemDataWithId) := item.data?.bind fun data => (fromJson? data).toOption + | return .pure item + let some id := data.id? + | return .pure item + let pos := text.lspPosToUtf8Pos data.params.position + withWaitFindSnap doc (·.endPos + ' ' >= pos) + (notFoundX := pure item) + (abortedX := pure item) + (x := fun snap => Completion.resolveCompletionItem? text pos snap.infoTree item id) open Elab in def handleHover (p : HoverParams) @@ -609,18 +624,76 @@ partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams) return t₁.map fun _ => pure WaitForDiagnostics.mk builtin_initialize - registerLspRequestHandler "textDocument/waitForDiagnostics" WaitForDiagnosticsParams WaitForDiagnostics handleWaitForDiagnostics - registerLspRequestHandler "textDocument/completion" CompletionParams CompletionList handleCompletion - registerLspRequestHandler "textDocument/hover" HoverParams (Option Hover) handleHover - registerLspRequestHandler "textDocument/declaration" TextDocumentPositionParams (Array LocationLink) (handleDefinition GoToKind.declaration) - registerLspRequestHandler "textDocument/definition" TextDocumentPositionParams (Array LocationLink) (handleDefinition GoToKind.definition) - registerLspRequestHandler "textDocument/typeDefinition" TextDocumentPositionParams (Array LocationLink) (handleDefinition GoToKind.type) - registerLspRequestHandler "textDocument/documentHighlight" DocumentHighlightParams DocumentHighlightResult handleDocumentHighlight - registerLspRequestHandler "textDocument/documentSymbol" DocumentSymbolParams DocumentSymbolResult handleDocumentSymbol - registerLspRequestHandler "textDocument/semanticTokens/full" SemanticTokensParams SemanticTokens handleSemanticTokensFull - registerLspRequestHandler "textDocument/semanticTokens/range" SemanticTokensRangeParams SemanticTokens handleSemanticTokensRange - registerLspRequestHandler "textDocument/foldingRange" FoldingRangeParams (Array FoldingRange) handleFoldingRange - registerLspRequestHandler "$/lean/plainGoal" PlainGoalParams (Option PlainGoal) handlePlainGoal - registerLspRequestHandler "$/lean/plainTermGoal" PlainTermGoalParams (Option PlainTermGoal) handlePlainTermGoal + registerLspRequestHandler + "textDocument/waitForDiagnostics" + WaitForDiagnosticsParams + WaitForDiagnostics + handleWaitForDiagnostics + registerLspRequestHandler + "textDocument/completion" + CompletionParams + CompletionList + handleCompletion + Completion.fillEligibleHeaderDecls + registerLspRequestHandler + "completionItem/resolve" + CompletionItem + CompletionItem + handleCompletionItemResolve + registerLspRequestHandler + "textDocument/hover" + HoverParams + (Option Hover) + handleHover + registerLspRequestHandler + "textDocument/declaration" + TextDocumentPositionParams + (Array LocationLink) + (handleDefinition GoToKind.declaration) + registerLspRequestHandler + "textDocument/definition" + TextDocumentPositionParams + (Array LocationLink) + (handleDefinition GoToKind.definition) + registerLspRequestHandler + "textDocument/typeDefinition" + TextDocumentPositionParams + (Array LocationLink) + (handleDefinition GoToKind.type) + registerLspRequestHandler + "textDocument/documentHighlight" + DocumentHighlightParams + DocumentHighlightResult + handleDocumentHighlight + registerLspRequestHandler + "textDocument/documentSymbol" + DocumentSymbolParams + DocumentSymbolResult + handleDocumentSymbol + registerLspRequestHandler + "textDocument/semanticTokens/full" + SemanticTokensParams + SemanticTokens + handleSemanticTokensFull + registerLspRequestHandler + "textDocument/semanticTokens/range" + SemanticTokensRangeParams + SemanticTokens + handleSemanticTokensRange + registerLspRequestHandler + "textDocument/foldingRange" + FoldingRangeParams + (Array FoldingRange) + handleFoldingRange + registerLspRequestHandler + "$/lean/plainGoal" + PlainGoalParams + (Option PlainGoal) + handlePlainGoal + registerLspRequestHandler + "$/lean/plainTermGoal" + PlainTermGoalParams + (Option PlainTermGoal) + handlePlainTermGoal end Lean.Server.FileWorker diff --git a/src/Lean/Server/ImportCompletion.lean b/src/Lean/Server/ImportCompletion.lean index 08dfcb36d4cf..ca89b9da5210 100644 --- a/src/Lean/Server/ImportCompletion.lean +++ b/src/Lean/Server/ImportCompletion.lean @@ -10,6 +10,7 @@ import Lean.Data.Lsp.Utf16 import Lean.Data.Lsp.LanguageFeatures import Lean.Util.Paths import Lean.Util.LakePath +import Lean.Server.CompletionItemData namespace ImportCompletion @@ -120,23 +121,30 @@ def collectAvailableImports : IO AvailableImports := do ImportCompletion.collectAvailableImportsFromSrcSearchPath | some availableImports => pure availableImports +def addCompletionItemData (completionList : CompletionList) (params : CompletionParams) + : CompletionList := + let data := { params : Lean.Lsp.CompletionItemData } + { completionList with items := completionList.items.map fun item => + { item with data? := some <| toJson data } } + def find (text : FileMap) (headerStx : Syntax) (params : CompletionParams) (availableImports : AvailableImports) : CompletionList := let availableImports := availableImports.toImportTrie let completionPos := text.lspPosToUtf8Pos params.position if isImportNameCompletionRequest headerStx completionPos then let allAvailableImportNameCompletions := availableImports.toArray.map ({ label := toString · }) - { isIncomplete := false, items := allAvailableImportNameCompletions } + addCompletionItemData { isIncomplete := false, items := allAvailableImportNameCompletions } params else if isImportCmdCompletionRequest headerStx completionPos then let allAvailableFullImportCompletions := availableImports.toArray.map ({ label := s!"import {·}" }) - { isIncomplete := false, items := allAvailableFullImportCompletions } + addCompletionItemData { isIncomplete := false, items := allAvailableFullImportCompletions } params else let completionNames : Array Name := computePartialImportCompletions headerStx completionPos availableImports let completions : Array CompletionItem := completionNames.map ({ label := toString · }) - { isIncomplete := false, items := completions } + addCompletionItemData { isIncomplete := false, items := completions } params def computeCompletions (text : FileMap) (headerStx : Syntax) (params : CompletionParams) : IO CompletionList := do let availableImports ← collectAvailableImports - return find text headerStx params availableImports + let completionList := find text headerStx params availableImports + return addCompletionItemData completionList params end ImportCompletion diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 7ba32ea41817..de057cf8bca2 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -182,8 +182,9 @@ section HandlerTable open Lsp structure RequestHandler where - fileSource : Json → Except RequestError Lsp.DocumentUri - handle : Json → RequestM (RequestTask Json) + fileSource : Json → Except RequestError Lsp.DocumentUri + handle : Json → RequestM (RequestTask Json) + handleHeaderCaching : Environment → IO Unit builtin_initialize requestHandlers : IO.Ref (PersistentHashMap String RequestHandler) ← IO.mkRef {} @@ -203,7 +204,9 @@ as LSP error responses. -/ def registerLspRequestHandler (method : String) paramType [FromJson paramType] [FileSource paramType] respType [ToJson respType] - (handler : paramType → RequestM (RequestTask respType)) : IO Unit := do + (handler : paramType → RequestM (RequestTask respType)) + (headerCachingHandler : Environment → IO Unit := fun _ => pure ()) + : IO Unit := do if !(← Lean.initializing) then throw <| IO.userError s!"Failed to register LSP request handler for '{method}': only possible during initialization" if (← requestHandlers.get).contains method then @@ -214,8 +217,8 @@ def registerLspRequestHandler (method : String) let params ← liftExcept <| parseRequestParams paramType j let t ← handler params pure <| t.map <| Except.map ToJson.toJson - - requestHandlers.modify fun rhs => rhs.insert method { fileSource, handle } + let handleHeaderCaching := headerCachingHandler + requestHandlers.modify fun rhs => rhs.insert method { fileSource, handle, handleHeaderCaching } def lookupLspRequestHandler (method : String) : IO (Option RequestHandler) := return (← requestHandlers.get).find? method @@ -246,6 +249,10 @@ def chainLspRequestHandler (method : String) else throw <| IO.userError s!"Failed to chain LSP request handler for '{method}': no initial handler registered" +def runHeaderCachingHandlers (headerEnv : Environment) : IO Unit := do + (← requestHandlers.get).forM fun _ handler => + handler.handleHeaderCaching headerEnv + def routeLspRequest (method : String) (params : Json) : IO (Except RequestError DocumentUri) := do match (← lookupLspRequestHandler method) with | none => return Except.error <| RequestError.methodNotFound method diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 261e82be7fbe..d2d85ba266de 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -817,6 +817,7 @@ def mkLeanServerCapabilities : ServerCapabilities := { -- refine completionProvider? := some { triggerCharacters? := some #["."] + resolveProvider := true } hoverProvider := true declarationProvider := true diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out index 824aa82044e2..322acc7753d4 100644 --- a/tests/lean/interactive/1265.lean.expected.out +++ b/tests/lean/interactive/1265.lean.expected.out @@ -1,54 +1,172 @@ {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}} {"items": - [{"label": "getHygieneInfo", + [{"sortText": "0", + "label": "expandInterpolatedStr", "kind": 3, - "detail": "Lean.HygieneInfo → Lean.Name"}, - {"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"}, - {"label": "getName", "kind": 3, "detail": "Lean.NameLit → Lean.Name"}, - {"label": "expandInterpolatedStr", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.expandInterpolatedStr"}}}, + {"sortText": "1", + "label": "getChar", "kind": 3, - "detail": - "Lean.TSyntax Lean.interpolatedStrKind → Lean.Term → Lean.Term → Lean.MacroM Lean.Term"}, - {"label": "getChar", "kind": 3, "detail": "Lean.CharLit → Char"}, - {"label": "getDocString", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getChar"}}}, + {"sortText": "2", + "label": "getDocString", "kind": 3, - "detail": "Lean.TSyntax `Lean.Parser.Command.docComment → String"}, - {"label": "getNat", "kind": 3, "detail": "Lean.NumLit → Nat"}, - {"label": "getScientific", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getDocString"}}}, + {"sortText": "3", + "label": "getHygieneInfo", "kind": 3, - "detail": "Lean.ScientificLit → Nat × Bool × Nat"}, - {"label": "getString", "kind": 3, "detail": "Lean.StrLit → String"}, - {"label": "raw", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getHygieneInfo"}}}, + {"sortText": "4", + "label": "getId", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getId"}}}, + {"sortText": "5", + "label": "getName", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getName"}}}, + {"sortText": "6", + "label": "getNat", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getNat"}}}, + {"sortText": "7", + "label": "getScientific", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getScientific"}}}, + {"sortText": "8", + "label": "getString", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.getString"}}}, + {"sortText": "9", + "label": "raw", "kind": 5, "documentation": {"value": "The underlying `Syntax` value. ", "kind": "markdown"}, - "detail": "Lean.TSyntax ks → Lean.Syntax"}], + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 0, "character": 51}}, + "id": {"const": "Lean.TSyntax.raw"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}} {"items": - [{"label": "getHygieneInfo", + [{"sortText": "0", + "label": "expandInterpolatedStr", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.expandInterpolatedStr"}}}, + {"sortText": "1", + "label": "getChar", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getChar"}}}, + {"sortText": "2", + "label": "getDocString", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getDocString"}}}, + {"sortText": "3", + "label": "getHygieneInfo", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getHygieneInfo"}}}, + {"sortText": "4", + "label": "getId", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getId"}}}, + {"sortText": "5", + "label": "getName", "kind": 3, - "detail": "Lean.HygieneInfo → Lean.Name"}, - {"label": "getId", "kind": 3, "detail": "Lean.Ident → Lean.Name"}, - {"label": "getName", "kind": 3, "detail": "Lean.NameLit → Lean.Name"}, - {"label": "expandInterpolatedStr", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getName"}}}, + {"sortText": "6", + "label": "getNat", "kind": 3, - "detail": - "Lean.TSyntax Lean.interpolatedStrKind → Lean.Term → Lean.Term → Lean.MacroM Lean.Term"}, - {"label": "getChar", "kind": 3, "detail": "Lean.CharLit → Char"}, - {"label": "getDocString", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getNat"}}}, + {"sortText": "7", + "label": "getScientific", "kind": 3, - "detail": "Lean.TSyntax `Lean.Parser.Command.docComment → String"}, - {"label": "getNat", "kind": 3, "detail": "Lean.NumLit → Nat"}, - {"label": "getScientific", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getScientific"}}}, + {"sortText": "8", + "label": "getString", "kind": 3, - "detail": "Lean.ScientificLit → Nat × Bool × Nat"}, - {"label": "getString", "kind": 3, "detail": "Lean.StrLit → String"}, - {"label": "raw", + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.getString"}}}, + {"sortText": "9", + "label": "raw", "kind": 5, "documentation": {"value": "The underlying `Syntax` value. ", "kind": "markdown"}, - "detail": "Lean.TSyntax ks → Lean.Syntax"}], + "data": + {"params": + {"textDocument": {"uri": "file:///1265.lean"}, + "position": {"line": 2, "character": 53}}, + "id": {"const": "Lean.TSyntax.raw"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/1659.lean.expected.out b/tests/lean/interactive/1659.lean.expected.out index cb8d2d4bae23..ba7a5ef84b8f 100644 --- a/tests/lean/interactive/1659.lean.expected.out +++ b/tests/lean/interactive/1659.lean.expected.out @@ -1,47 +1,124 @@ {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 9, "character": 23}} {"items": - [{"label": "Lean.Elab.Tactic.elabTermEnsuringType", + [{"sortText": "0", + "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, - "detail": "Type"}, - {"label": "Lean.Elab.Term.elabTermEnsuringType", + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 9, "character": 23}}, + "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + {"sortText": "1", + "label": "Lean.Elab.Term.elabTermEnsuringType", "kind": 21, - "detail": "Type"}], + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 9, "character": 23}}, + "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 15, "character": 23}} {"items": - [{"label": "Tactic.elabTermEnsuringType", "kind": 21, "detail": "Type"}, - {"label": "Term.elabTermEnsuringType", "kind": 21, "detail": "Type"}], + [{"sortText": "0", + "label": "Tactic.elabTermEnsuringType", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 15, "character": 23}}, + "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + {"sortText": "1", + "label": "Term.elabTermEnsuringType", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 15, "character": 23}}, + "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 21, "character": 23}} {"items": - [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, - {"label": "Lean.Elab.Tactic.elabTermEnsuringType", + [{"sortText": "0", + "label": "elabTermEnsuringType", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 21, "character": 23}}, + "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}, + {"sortText": "1", + "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, - "detail": "Type"}], + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 21, "character": 23}}, + "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 27, "character": 23}} {"items": - [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, - {"label": "Lean.Elab.Tactic.elabTermEnsuringType", + [{"sortText": "0", + "label": "elabTermEnsuringType", "kind": 21, - "detail": "Type"}, - {"label": "Lean.Elab.Term.elabTermEnsuringType", + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 27, "character": 23}}, + "id": {"const": "elabTermEnsuringType"}}}, + {"sortText": "1", + "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, - "detail": "Type"}], + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 27, "character": 23}}, + "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + {"sortText": "2", + "label": "Lean.Elab.Term.elabTermEnsuringType", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 27, "character": 23}}, + "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}} {"items": - [{"label": "elabTermEnsuringType", "kind": 21, "detail": "Type"}, - {"label": "Lean.Elab.elabTermEnsuringType", "kind": 21, "detail": "Type"}, - {"label": "Lean.Elab.Tactic.elabTermEnsuringType", + [{"sortText": "0", + "label": "elabTermEnsuringType", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 33, "character": 23}}, + "id": {"const": "elabTermEnsuringType"}}}, + {"sortText": "1", + "label": "Lean.Elab.elabTermEnsuringType", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 33, "character": 23}}, + "id": {"const": "Lean.Elab.elabTermEnsuringType"}}}, + {"sortText": "2", + "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, - "detail": "Type"}, - {"label": "Lean.Elab.Term.elabTermEnsuringType", + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 33, "character": 23}}, + "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + {"sortText": "3", + "label": "Lean.Elab.Term.elabTermEnsuringType", "kind": 21, - "detail": "Type"}], + "data": + {"params": + {"textDocument": {"uri": "file:///1659.lean"}, + "position": {"line": 33, "character": 23}}, + "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index 155bb3aa7edb..d2940b5f5164 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -1,6 +1,20 @@ {"textDocument": {"uri": "file:///533.lean"}, "position": {"line": 4, "character": 10}} {"items": - [{"label": "F", "kind": 6, "detail": "Sort ?u"}, - {"label": "Foo", "kind": 6, "detail": "Sort ?u"}], + [{"sortText": "0", + "label": "F", + "kind": 6, + "data": + {"params": + {"textDocument": {"uri": "file:///533.lean"}, + "position": {"line": 4, "character": 10}}, + "id": {"fvar": "_uniq.6"}}}, + {"sortText": "1", + "label": "Foo", + "kind": 6, + "data": + {"params": + {"textDocument": {"uri": "file:///533.lean"}, + "position": {"line": 4, "character": 10}}, + "id": {"fvar": "_uniq.2"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out index faadde731fa1..249740d5d3e1 100644 --- a/tests/lean/interactive/863.lean.expected.out +++ b/tests/lean/interactive/863.lean.expected.out @@ -1,16 +1,40 @@ {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 9, "character": 12}} {"items": - [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}, - {"label": "MonadRef.getRef", + [{"sortText": "0", + "label": "getRef", "kind": 5, - "detail": "[self : MonadRef] → Type"}], + "data": + {"params": + {"textDocument": {"uri": "file:///863.lean"}, + "position": {"line": 9, "character": 12}}, + "id": {"const": "Lean.MonadRef.getRef"}}}, + {"sortText": "1", + "label": "MonadRef.getRef", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///863.lean"}, + "position": {"line": 9, "character": 12}}, + "id": {"const": "Lean.MonadRef.getRef"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 13, "character": 12}} {"items": - [{"label": "getRef", "kind": 5, "detail": "[self : MonadRef] → Type"}, - {"label": "MonadRef.getRef", + [{"sortText": "0", + "label": "getRef", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///863.lean"}, + "position": {"line": 13, "character": 12}}, + "id": {"const": "Lean.MonadRef.getRef"}}}, + {"sortText": "1", + "label": "MonadRef.getRef", "kind": 5, - "detail": "[self : MonadRef] → Type"}], + "data": + {"params": + {"textDocument": {"uri": "file:///863.lean"}, + "position": {"line": 13, "character": 12}}, + "id": {"const": "Lean.MonadRef.getRef"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/compHeader.lean.expected.out b/tests/lean/interactive/compHeader.lean.expected.out index e616d3c9ee52..e76b8e0786b1 100644 --- a/tests/lean/interactive/compHeader.lean.expected.out +++ b/tests/lean/interactive/compHeader.lean.expected.out @@ -1,6 +1,20 @@ {"textDocument": {"uri": "file:///compHeader.lean"}, "position": {"line": 2, "character": 22}} {"items": - [{"label": "veryLongNam", "kind": 6, "detail": "Sort u_1"}, - {"label": "veryLongNameForCompletion", "kind": 21, "detail": "Type"}], + [{"sortText": "0", + "label": "veryLongNam", + "kind": 6, + "data": + {"params": + {"textDocument": {"uri": "file:///compHeader.lean"}, + "position": {"line": 2, "character": 22}}, + "id": {"fvar": "_uniq.7"}}}, + {"sortText": "1", + "label": "veryLongNameForCompletion", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///compHeader.lean"}, + "position": {"line": 2, "character": 22}}, + "id": {"const": "veryLongNameForCompletion"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/compNamespace.lean.expected.out b/tests/lean/interactive/compNamespace.lean.expected.out index 68fd4113384b..ba2b53585e65 100644 --- a/tests/lean/interactive/compNamespace.lean.expected.out +++ b/tests/lean/interactive/compNamespace.lean.expected.out @@ -1,21 +1,60 @@ {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 5, "character": 12}} -{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], +{"items": + [{"sortText": "0", + "label": "LongNamespaceExample", + "kind": 9, + "detail": "namespace", + "data": + {"params": + {"textDocument": {"uri": "file:///compNamespace.lean"}, + "position": {"line": 5, "character": 12}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 9, "character": 12}} -{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], +{"items": + [{"sortText": "0", + "label": "LongNamespaceExample", + "kind": 9, + "detail": "namespace", + "data": + {"params": + {"textDocument": {"uri": "file:///compNamespace.lean"}, + "position": {"line": 9, "character": 12}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 13, "character": 11}} -{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], +{"items": + [{"sortText": "0", + "label": "LongNamespaceExample", + "kind": 9, + "detail": "namespace", + "data": + {"params": + {"textDocument": {"uri": "file:///compNamespace.lean"}, + "position": {"line": 13, "character": 11}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 16, "character": 16}} {"items": - [{"label": "Foo.LongNamespaceExample", "kind": 9, "detail": "namespace"}], + [{"sortText": "0", + "label": "Foo.LongNamespaceExample", + "kind": 9, + "detail": "namespace", + "data": + {"params": + {"textDocument": {"uri": "file:///compNamespace.lean"}, + "position": {"line": 16, "character": 16}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///compNamespace.lean"}, "position": {"line": 20, "character": 12}} -{"items": [{"label": "LongNamespaceExample", "kind": 9, "detail": "namespace"}], +{"items": + [{"sortText": "0", + "label": "LongNamespaceExample", + "kind": 9, + "detail": "namespace", + "data": + {"params": + {"textDocument": {"uri": "file:///compNamespace.lean"}, + "position": {"line": 20, "character": 12}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out index 8963177efab2..12bfafefa755 100644 --- a/tests/lean/interactive/completion.lean.expected.out +++ b/tests/lean/interactive/completion.lean.expected.out @@ -1,16 +1,48 @@ {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 3, "character": 22}} -{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], +{"items": + [{"sortText": "0", + "label": "foo", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion.lean"}, + "position": {"line": 3, "character": 22}}, + "id": {"const": "Foo.foo"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 5, "character": 23}} -{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], +{"items": + [{"sortText": "0", + "label": "foo", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion.lean"}, + "position": {"line": 5, "character": 23}}, + "id": {"const": "Foo.foo"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 7, "character": 28}} -{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], +{"items": + [{"sortText": "0", + "label": "foo", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion.lean"}, + "position": {"line": 7, "character": 28}}, + "id": {"const": "Foo.foo"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 9, "character": 29}} -{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], +{"items": + [{"sortText": "0", + "label": "foo", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion.lean"}, + "position": {"line": 9, "character": 29}}, + "id": {"const": "Foo.foo"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out index b2620931aa7c..a760a3958d6b 100644 --- a/tests/lean/interactive/completion2.lean.expected.out +++ b/tests/lean/interactive/completion2.lean.expected.out @@ -1,31 +1,136 @@ {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 19, "character": 10}} {"items": - [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, - {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"}, - {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"}, - {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], + [{"sortText": "0", + "label": "ax1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 19, "character": 10}}, + "id": {"const": "Foo.Bla.ax1"}}}, + {"sortText": "1", + "label": "ex1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 19, "character": 10}}, + "id": {"const": "Foo.Bla.ex1"}}}, + {"sortText": "2", + "label": "ex2", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 19, "character": 10}}, + "id": {"const": "Foo.Bla.ex2"}}}, + {"sortText": "3", + "label": "ex3", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 19, "character": 10}}, + "id": {"const": "Foo.Bla.ex3"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}} {"items": - [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, - {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"}, - {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"}, - {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], + [{"sortText": "0", + "label": "ax1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 25, "character": 6}}, + "id": {"const": "Foo.Bla.ax1"}}}, + {"sortText": "1", + "label": "ex1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 25, "character": 6}}, + "id": {"const": "Foo.Bla.ex1"}}}, + {"sortText": "2", + "label": "ex2", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 25, "character": 6}}, + "id": {"const": "Foo.Bla.ex2"}}}, + {"sortText": "3", + "label": "ex3", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 25, "character": 6}}, + "id": {"const": "Foo.Bla.ex3"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}} {"items": - [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, - {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"}, - {"label": "ax1", "kind": 3, "detail": "a ≤ b → a - a ≤ b - b"}, - {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], + [{"sortText": "0", + "label": "ax1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 30, "character": 21}}, + "id": {"const": "Foo.Bla.ax1"}}}, + {"sortText": "1", + "label": "ex1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 30, "character": 21}}, + "id": {"const": "Foo.Bla.ex1"}}}, + {"sortText": "2", + "label": "ex2", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 30, "character": 21}}, + "id": {"const": "Foo.Bla.ex2"}}}, + {"sortText": "3", + "label": "ex3", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 30, "character": 21}}, + "id": {"const": "Foo.Bla.ex3"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 37, "character": 22}} {"items": - [{"label": "ex2", "kind": 3, "detail": "a ≤ b → a + 2 ≤ b + 2"}, - {"label": "ex3", "kind": 3, "detail": "a ≤ b → c ≤ d → a + c ≤ b + d"}, - {"label": "ex1", "kind": 3, "detail": "a ≤ b → a + a ≤ b + b"}], + [{"sortText": "0", + "label": "ex1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 37, "character": 22}}, + "id": {"const": "Foo.Bla.ex1"}}}, + {"sortText": "1", + "label": "ex2", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 37, "character": 22}}, + "id": {"const": "Foo.Bla.ex2"}}}, + {"sortText": "2", + "label": "ex3", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion2.lean"}, + "position": {"line": 37, "character": 22}}, + "id": {"const": "Foo.Bla.ex3"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out index 615bb214c8a4..640cc68ef365 100644 --- a/tests/lean/interactive/completion3.lean.expected.out +++ b/tests/lean/interactive/completion3.lean.expected.out @@ -1,28 +1,112 @@ {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 7, "character": 9}} {"items": - [{"label": "b", "kind": 5, "detail": "S → Bool"}, - {"label": "x", "kind": 5, "detail": "S → Nat"}, - {"label": "y", "kind": 5, "detail": "S → String"}], + [{"sortText": "0", + "label": "b", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 7, "character": 9}}, + "id": {"const": "S.b"}}}, + {"sortText": "1", + "label": "x", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 7, "character": 9}}, + "id": {"const": "S.x"}}}, + {"sortText": "2", + "label": "y", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 7, "character": 9}}, + "id": {"const": "S.y"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 12, "character": 5}} {"items": - [{"label": "b", "kind": 5, "detail": "S → Bool"}, - {"label": "x", "kind": 5, "detail": "S → Nat"}, - {"label": "y", "kind": 5, "detail": "S → String"}], + [{"sortText": "0", + "label": "b", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 12, "character": 5}}, + "id": {"const": "S.b"}}}, + {"sortText": "1", + "label": "x", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 12, "character": 5}}, + "id": {"const": "S.x"}}}, + {"sortText": "2", + "label": "y", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 12, "character": 5}}, + "id": {"const": "S.y"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 16, "character": 5}} {"items": - [{"label": "b", "kind": 5, "detail": "S → Bool"}, - {"label": "x", "kind": 5, "detail": "S → Nat"}, - {"label": "y", "kind": 5, "detail": "S → String"}], + [{"sortText": "0", + "label": "b", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 16, "character": 5}}, + "id": {"const": "S.b"}}}, + {"sortText": "1", + "label": "x", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 16, "character": 5}}, + "id": {"const": "S.x"}}}, + {"sortText": "2", + "label": "y", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 16, "character": 5}}, + "id": {"const": "S.y"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 20, "character": 5}} {"items": - [{"label": "x", "kind": 5, "detail": "S → Nat"}, - {"label": "b", "kind": 5, "detail": "S → Bool"}, - {"label": "y", "kind": 5, "detail": "S → String"}], + [{"sortText": "0", + "label": "b", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 20, "character": 5}}, + "id": {"const": "S.b"}}}, + {"sortText": "1", + "label": "x", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 20, "character": 5}}, + "id": {"const": "S.x"}}}, + {"sortText": "2", + "label": "y", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion3.lean"}, + "position": {"line": 20, "character": 5}}, + "id": {"const": "S.y"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion4.lean.expected.out b/tests/lean/interactive/completion4.lean.expected.out index 67d9fc4fe530..b9ae0f03c03c 100644 --- a/tests/lean/interactive/completion4.lean.expected.out +++ b/tests/lean/interactive/completion4.lean.expected.out @@ -1,28 +1,112 @@ {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 7, "character": 4}} {"items": - [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, - {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, - {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], + [{"sortText": "0", + "label": "fn1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 7, "character": 4}}, + "id": {"const": "S.fn1"}}}, + {"sortText": "1", + "label": "fn2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 7, "character": 4}}, + "id": {"const": "S.fn2"}}}, + {"sortText": "2", + "label": "pred", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 7, "character": 4}}, + "id": {"const": "S.pred"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 11, "character": 10}} {"items": - [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, - {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, - {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], + [{"sortText": "0", + "label": "fn1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 11, "character": 10}}, + "id": {"const": "S.fn1"}}}, + {"sortText": "1", + "label": "fn2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 11, "character": 10}}, + "id": {"const": "S.fn2"}}}, + {"sortText": "2", + "label": "pred", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 11, "character": 10}}, + "id": {"const": "S.pred"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 16, "character": 11}} {"items": - [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, - {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, - {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], + [{"sortText": "0", + "label": "fn1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 16, "character": 11}}, + "id": {"const": "S.fn1"}}}, + {"sortText": "1", + "label": "fn2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 16, "character": 11}}, + "id": {"const": "S.fn2"}}}, + {"sortText": "2", + "label": "pred", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 16, "character": 11}}, + "id": {"const": "S.pred"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 20, "character": 21}} {"items": - [{"label": "fn1", "kind": 5, "detail": "S → Nat → IO Unit"}, - {"label": "fn2", "kind": 5, "detail": "S → Bool → IO Unit"}, - {"label": "pred", "kind": 5, "detail": "S → String → Bool"}], + [{"sortText": "0", + "label": "fn1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 20, "character": 21}}, + "id": {"const": "S.fn1"}}}, + {"sortText": "1", + "label": "fn2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 20, "character": 21}}, + "id": {"const": "S.fn2"}}}, + {"sortText": "2", + "label": "pred", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion4.lean"}, + "position": {"line": 20, "character": 21}}, + "id": {"const": "S.pred"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out index b88a5e9310d6..b84cf2c0edd5 100644 --- a/tests/lean/interactive/completion5.lean.expected.out +++ b/tests/lean/interactive/completion5.lean.expected.out @@ -1,7 +1,28 @@ {"textDocument": {"uri": "file:///completion5.lean"}, "position": {"line": 9, "character": 15}} {"items": - [{"label": "b1", "kind": 5, "detail": "C → String"}, - {"label": "f1", "kind": 5, "detail": "C → Nat"}, - {"label": "f2", "kind": 5, "detail": "C → Bool"}], + [{"sortText": "0", + "label": "b1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion5.lean"}, + "position": {"line": 9, "character": 15}}, + "id": {"const": "C.b1"}}}, + {"sortText": "1", + "label": "f1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion5.lean"}, + "position": {"line": 9, "character": 15}}, + "id": {"const": "C.f1"}}}, + {"sortText": "2", + "label": "f2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion5.lean"}, + "position": {"line": 9, "character": 15}}, + "id": {"const": "C.f2"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion6.lean.expected.out b/tests/lean/interactive/completion6.lean.expected.out index e5586b430b35..f297911e0d4f 100644 --- a/tests/lean/interactive/completion6.lean.expected.out +++ b/tests/lean/interactive/completion6.lean.expected.out @@ -1,19 +1,96 @@ {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}} {"items": - [{"label": "b1", "kind": 5, "detail": "C → String"}, - {"label": "f1", "kind": 5, "detail": "C → Nat"}, - {"label": "f2", "kind": 5, "detail": "C → Bool"}, - {"label": "f3", "kind": 5, "detail": "D → Bool"}, - {"label": "toC", "kind": 5, "detail": "D → C"}], + [{"sortText": "0", + "label": "b1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "C.b1"}}}, + {"sortText": "1", + "label": "f1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "C.f1"}}}, + {"sortText": "2", + "label": "f2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "C.f2"}}}, + {"sortText": "3", + "label": "f3", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "D.f3"}}}, + {"sortText": "4", + "label": "toC", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "D.toC"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}} {"items": - [{"label": "b1", "kind": 5, "detail": "C → String"}, - {"label": "doubleF1", "kind": 3, "detail": "E → Nat"}, - {"label": "f1", "kind": 5, "detail": "C → Nat"}, - {"label": "f2", "kind": 5, "detail": "C → Bool"}, - {"label": "f3", "kind": 5, "detail": "D → Bool"}, - {"label": "toC", "kind": 5, "detail": "D → C"}], + [{"sortText": "0", + "label": "b1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 21, "character": 4}}, + "id": {"const": "C.b1"}}}, + {"sortText": "1", + "label": "doubleF1", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 21, "character": 4}}, + "id": {"const": "E.doubleF1"}}}, + {"sortText": "2", + "label": "f1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 21, "character": 4}}, + "id": {"const": "C.f1"}}}, + {"sortText": "3", + "label": "f2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 21, "character": 4}}, + "id": {"const": "C.f2"}}}, + {"sortText": "4", + "label": "f3", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 21, "character": 4}}, + "id": {"const": "D.f3"}}}, + {"sortText": "5", + "label": "toC", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion6.lean"}, + "position": {"line": 21, "character": 4}}, + "id": {"const": "D.toC"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index 04dd60a4ea12..c1e2efa5a698 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -1,11 +1,40 @@ {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 6, "character": 10}} -{"items": [{"label": "And", "kind": 22, "detail": "Type 1"}], +{"items": + [{"sortText": "0", + "label": "And", + "kind": 22, + "data": + {"params": + {"textDocument": {"uri": "file:///completion7.lean"}, + "position": {"line": 6, "character": 10}}, + "id": {"const": "And"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 8, "character": 11}} {"items": - [{"label": "left", "kind": 5, "detail": "And → Type"}, - {"label": "mk", "kind": 4, "detail": "Type → Type → And"}, - {"label": "right", "kind": 5, "detail": "And → Type"}], + [{"sortText": "0", + "label": "left", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion7.lean"}, + "position": {"line": 8, "character": 11}}, + "id": {"const": "And.left"}}}, + {"sortText": "1", + "label": "mk", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completion7.lean"}, + "position": {"line": 8, "character": 11}}, + "id": {"const": "And.mk"}}}, + {"sortText": "2", + "label": "right", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completion7.lean"}, + "position": {"line": 8, "character": 11}}, + "id": {"const": "And.right"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionAtPrint.lean.expected.out b/tests/lean/interactive/completionAtPrint.lean.expected.out index 6a27b6c940d1..4ac1f7722e74 100644 --- a/tests/lean/interactive/completionAtPrint.lean.expected.out +++ b/tests/lean/interactive/completionAtPrint.lean.expected.out @@ -1,14 +1,24 @@ {"textDocument": {"uri": "file:///completionAtPrint.lean"}, "position": {"line": 2, "character": 25}} {"items": - [{"label": "find?", + [{"sortText": "0", + "label": "find?", "kind": 3, - "detail": "Lean.Environment → Lean.Name → Option Lean.ConstantInfo"}, - {"label": "freeRegions", + "data": + {"params": + {"textDocument": {"uri": "file:///completionAtPrint.lean"}, + "position": {"line": 2, "character": 25}}, + "id": {"const": "Lean.Environment.find?"}}}, + {"sortText": "1", + "label": "freeRegions", "kind": 3, "documentation": {"value": "Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in\nparticular, `env` should be the last reference to any `Environment` derived from these imports. ", "kind": "markdown"}, - "detail": "Lean.Environment → IO Unit"}], + "data": + {"params": + {"textDocument": {"uri": "file:///completionAtPrint.lean"}, + "position": {"line": 2, "character": 25}}, + "id": {"const": "Lean.Environment.freeRegions"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionCheck.lean b/tests/lean/interactive/completionCheck.lean new file mode 100644 index 000000000000..67a105de2163 --- /dev/null +++ b/tests/lean/interactive/completionCheck.lean @@ -0,0 +1,8 @@ +structure AVerySpecificStructureName where + x : Nat + +structure AVerySpecificStructureName2 where + x : Nat + +#check AVerySpecificStructureName + --^ textDocument/completion diff --git a/tests/lean/interactive/completionCheck.lean.expected.out b/tests/lean/interactive/completionCheck.lean.expected.out new file mode 100644 index 000000000000..0c1647a11e95 --- /dev/null +++ b/tests/lean/interactive/completionCheck.lean.expected.out @@ -0,0 +1,20 @@ +{"textDocument": {"uri": "file:///completionCheck.lean"}, + "position": {"line": 6, "character": 33}} +{"items": + [{"sortText": "0", + "label": "AVerySpecificStructureName", + "kind": 22, + "data": + {"params": + {"textDocument": {"uri": "file:///completionCheck.lean"}, + "position": {"line": 6, "character": 33}}, + "id": {"const": "AVerySpecificStructureName"}}}, + {"sortText": "1", + "label": "AVerySpecificStructureName2", + "kind": 22, + "data": + {"params": + {"textDocument": {"uri": "file:///completionCheck.lean"}, + "position": {"line": 6, "character": 33}}, + "id": {"const": "AVerySpecificStructureName2"}}}], + "isIncomplete": true} diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out index 4521ca09a1c6..2d4a8aef4b6a 100644 --- a/tests/lean/interactive/completionDocString.lean.expected.out +++ b/tests/lean/interactive/completionDocString.lean.expected.out @@ -1,16 +1,26 @@ {"textDocument": {"uri": "file:///completionDocString.lean"}, "position": {"line": 0, "character": 20}} {"items": - [{"label": "insertAt", + [{"sortText": "0", + "label": "insertAt", "kind": 3, "documentation": {"value": "Insert element `a` at position `i`. ", "kind": "markdown"}, - "detail": "(as : Array α) → Fin (Array.size as + 1) → α → Array α"}, - {"label": "insertAt!", + "data": + {"params": + {"textDocument": {"uri": "file:///completionDocString.lean"}, + "position": {"line": 0, "character": 20}}, + "id": {"const": "Array.insertAt"}}}, + {"sortText": "1", + "label": "insertAt!", "kind": 3, "documentation": {"value": "Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. ", "kind": "markdown"}, - "detail": "Array α → Nat → α → Array α"}], + "data": + {"params": + {"textDocument": {"uri": "file:///completionDocString.lean"}, + "position": {"line": 0, "character": 20}}, + "id": {"const": "Array.insertAt!"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionEOF.lean.expected.out b/tests/lean/interactive/completionEOF.lean.expected.out index db831fc9d4fd..370fd1ca3540 100644 --- a/tests/lean/interactive/completionEOF.lean.expected.out +++ b/tests/lean/interactive/completionEOF.lean.expected.out @@ -1,4 +1,12 @@ {"textDocument": {"uri": "file:///completionEOF.lean"}, "position": {"line": 8, "character": 9}} -{"items": [{"label": "And", "kind": 21, "detail": "Type"}], +{"items": + [{"sortText": "0", + "label": "And", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///completionEOF.lean"}, + "position": {"line": 8, "character": 9}}, + "id": {"const": "And"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionFromExpectedType.lean b/tests/lean/interactive/completionFromExpectedType.lean new file mode 100644 index 000000000000..53cf24bf9d35 --- /dev/null +++ b/tests/lean/interactive/completionFromExpectedType.lean @@ -0,0 +1,5 @@ +structure Foo where + x : Nat + +def foo : Foo := . + --^ textDocument/completion diff --git a/tests/lean/interactive/completionFromExpectedType.lean.expected.out b/tests/lean/interactive/completionFromExpectedType.lean.expected.out new file mode 100644 index 000000000000..d94d7fab2fdc --- /dev/null +++ b/tests/lean/interactive/completionFromExpectedType.lean.expected.out @@ -0,0 +1,12 @@ +{"textDocument": {"uri": "file:///completionFromExpectedType.lean"}, + "position": {"line": 3, "character": 18}} +{"items": + [{"sortText": "0", + "label": "mk", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///completionFromExpectedType.lean"}, + "position": {"line": 3, "character": 18}}, + "id": {"const": "Foo.mk"}}}], + "isIncomplete": true} diff --git a/tests/lean/interactive/completionIStr.lean.expected.out b/tests/lean/interactive/completionIStr.lean.expected.out index 47ea662abba0..6e8056aeef2a 100644 --- a/tests/lean/interactive/completionIStr.lean.expected.out +++ b/tests/lean/interactive/completionIStr.lean.expected.out @@ -1,7 +1,28 @@ {"textDocument": {"uri": "file:///completionIStr.lean"}, "position": {"line": 5, "character": 34}} {"items": - [{"label": "b1", "kind": 5, "detail": "C → String"}, - {"label": "f1", "kind": 5, "detail": "C → Nat"}, - {"label": "f2", "kind": 5, "detail": "C → Bool"}], + [{"sortText": "0", + "label": "b1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionIStr.lean"}, + "position": {"line": 5, "character": 34}}, + "id": {"const": "C.b1"}}}, + {"sortText": "1", + "label": "f1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionIStr.lean"}, + "position": {"line": 5, "character": 34}}, + "id": {"const": "C.f1"}}}, + {"sortText": "2", + "label": "f2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionIStr.lean"}, + "position": {"line": 5, "character": 34}}, + "id": {"const": "C.f2"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionOpenNamespaces.lean b/tests/lean/interactive/completionOpenNamespaces.lean new file mode 100644 index 000000000000..ffbdd4dc994b --- /dev/null +++ b/tests/lean/interactive/completionOpenNamespaces.lean @@ -0,0 +1,6 @@ +def A.B1.verySpecificDefinitionNameOfCompletionOpenNamespaces := 1 +open A B1 + +namespace A +def c2 : Nat := verySpecificDefinitionNameOfCompletionOpenNamespaces + --^ textDocument/completion diff --git a/tests/lean/interactive/completionOpenNamespaces.lean.expected.out b/tests/lean/interactive/completionOpenNamespaces.lean.expected.out new file mode 100644 index 000000000000..5b3087dd01c7 --- /dev/null +++ b/tests/lean/interactive/completionOpenNamespaces.lean.expected.out @@ -0,0 +1,13 @@ +{"textDocument": {"uri": "file:///completionOpenNamespaces.lean"}, + "position": {"line": 4, "character": 68}} +{"items": + [{"sortText": "0", + "label": "verySpecificDefinitionNameOfCompletionOpenNamespaces", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///completionOpenNamespaces.lean"}, + "position": {"line": 4, "character": 68}}, + "id": + {"const": "A.B1.verySpecificDefinitionNameOfCompletionOpenNamespaces"}}}], + "isIncomplete": true} diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out index 8b3036f5ffb4..31d9a27f4b03 100644 --- a/tests/lean/interactive/completionOption.lean.expected.out +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -9,10 +9,15 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "0", "label": "trace.PrettyPrinter.format", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -21,9 +26,14 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "1", "label": "format.indent", "kind": 10, - "detail": "(2), indentation"}, + "detail": "(2), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -32,9 +42,14 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "2", "label": "format.inputWidth", "kind": 10, - "detail": "(100), ideal input width"}, + "detail": "(100), ideal input width", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -43,9 +58,14 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "3", "label": "format.unicode", "kind": 10, - "detail": "(true), unicode characters"}, + "detail": "(true), unicode characters", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -54,9 +74,14 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "4", "label": "format.width", "kind": 10, - "detail": "(120), indentation"}, + "detail": "(120), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -65,10 +90,15 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "5", "label": "trace.PrettyPrinter.format.backtrack", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 1, "character": 11}, @@ -77,10 +107,15 @@ "insert": {"start": {"line": 1, "character": 11}, "end": {"line": 1, "character": 17}}}, + "sortText": "6", "label": "trace.PrettyPrinter.format.input", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}], + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 1, "character": 17}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 4, "character": 20}} @@ -93,9 +128,14 @@ "insert": {"start": {"line": 4, "character": 11}, "end": {"line": 4, "character": 20}}}, + "sortText": "0", "label": "format.indent", "kind": 10, - "detail": "(2), indentation"}, + "detail": "(2), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 4, "character": 20}}}}, {"textEdit": {"replace": {"start": {"line": 4, "character": 11}, @@ -104,9 +144,14 @@ "insert": {"start": {"line": 4, "character": 11}, "end": {"line": 4, "character": 20}}}, + "sortText": "1", "label": "format.inputWidth", "kind": 10, - "detail": "(100), ideal input width"}, + "detail": "(100), ideal input width", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 4, "character": 20}}}}, {"textEdit": {"replace": {"start": {"line": 4, "character": 11}, @@ -115,10 +160,15 @@ "insert": {"start": {"line": 4, "character": 11}, "end": {"line": 4, "character": 20}}}, + "sortText": "2", "label": "trace.PrettyPrinter.format.input", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}], + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 4, "character": 20}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 7, "character": 23}} @@ -131,10 +181,15 @@ "insert": {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}}, + "sortText": "0", "label": "trace.pp.analyze", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 7, "character": 23}}}}, {"textEdit": {"replace": {"start": {"line": 7, "character": 11}, @@ -143,10 +198,15 @@ "insert": {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}}, + "sortText": "1", "label": "trace.pp.analyze.annotate", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 7, "character": 23}}}}, {"textEdit": {"replace": {"start": {"line": 7, "character": 11}, @@ -155,10 +215,15 @@ "insert": {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}}, + "sortText": "2", "label": "trace.pp.analyze.error", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 7, "character": 23}}}}, {"textEdit": {"replace": {"start": {"line": 7, "character": 11}, @@ -167,10 +232,15 @@ "insert": {"start": {"line": 7, "character": 11}, "end": {"line": 7, "character": 23}}}, + "sortText": "3", "label": "trace.pp.analyze.tryUnify", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}], + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 7, "character": 23}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 10, "character": 27}} @@ -183,10 +253,15 @@ "insert": {"start": {"line": 10, "character": 11}, "end": {"line": 10, "character": 27}}}, + "sortText": "0", "label": "trace.pp.analyze", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 10, "character": 27}}}}, {"textEdit": {"replace": {"start": {"line": 10, "character": 11}, @@ -195,10 +270,15 @@ "insert": {"start": {"line": 10, "character": 11}, "end": {"line": 10, "character": 27}}}, + "sortText": "1", "label": "trace.pp.analyze.annotate", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 10, "character": 27}}}}, {"textEdit": {"replace": {"start": {"line": 10, "character": 11}, @@ -207,10 +287,15 @@ "insert": {"start": {"line": 10, "character": 11}, "end": {"line": 10, "character": 27}}}, + "sortText": "2", "label": "trace.pp.analyze.error", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 10, "character": 27}}}}, {"textEdit": {"replace": {"start": {"line": 10, "character": 11}, @@ -219,10 +304,15 @@ "insert": {"start": {"line": 10, "character": 11}, "end": {"line": 10, "character": 27}}}, + "sortText": "3", "label": "trace.pp.analyze.tryUnify", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}], + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 10, "character": 27}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 13, "character": 17}} @@ -235,10 +325,15 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "0", "label": "trace.PrettyPrinter.format", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -247,9 +342,14 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "1", "label": "format.indent", "kind": 10, - "detail": "(2), indentation"}, + "detail": "(2), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -258,9 +358,14 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "2", "label": "format.inputWidth", "kind": 10, - "detail": "(100), ideal input width"}, + "detail": "(100), ideal input width", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -269,9 +374,14 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "3", "label": "format.unicode", "kind": 10, - "detail": "(true), unicode characters"}, + "detail": "(true), unicode characters", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -280,9 +390,14 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "4", "label": "format.width", "kind": 10, - "detail": "(120), indentation"}, + "detail": "(120), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -291,10 +406,15 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "5", "label": "trace.PrettyPrinter.format.backtrack", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}, {"textEdit": {"replace": {"start": {"line": 13, "character": 11}, @@ -303,10 +423,15 @@ "insert": {"start": {"line": 13, "character": 11}, "end": {"line": 13, "character": 17}}}, + "sortText": "6", "label": "trace.PrettyPrinter.format.input", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}], + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 13, "character": 17}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionOption.lean"}, "position": {"line": 16, "character": 18}} @@ -319,9 +444,14 @@ "insert": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 18}}}, + "sortText": "0", "label": "format.indent", "kind": 10, - "detail": "(2), indentation"}, + "detail": "(2), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 16, "character": 18}}}}, {"textEdit": {"replace": {"start": {"line": 16, "character": 11}, @@ -330,9 +460,14 @@ "insert": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 18}}}, + "sortText": "1", "label": "format.inputWidth", "kind": 10, - "detail": "(100), ideal input width"}, + "detail": "(100), ideal input width", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 16, "character": 18}}}}, {"textEdit": {"replace": {"start": {"line": 16, "character": 11}, @@ -341,9 +476,14 @@ "insert": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 18}}}, + "sortText": "2", "label": "format.unicode", "kind": 10, - "detail": "(true), unicode characters"}, + "detail": "(true), unicode characters", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 16, "character": 18}}}}, {"textEdit": {"replace": {"start": {"line": 16, "character": 11}, @@ -352,9 +492,14 @@ "insert": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 18}}}, + "sortText": "3", "label": "format.width", "kind": 10, - "detail": "(120), indentation"}, + "detail": "(120), indentation", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 16, "character": 18}}}}, {"textEdit": {"replace": {"start": {"line": 16, "character": 11}, @@ -363,10 +508,15 @@ "insert": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 18}}}, + "sortText": "4", "label": "trace.PrettyPrinter.format.backtrack", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}, + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 16, "character": 18}}}}, {"textEdit": {"replace": {"start": {"line": 16, "character": 11}, @@ -375,8 +525,13 @@ "insert": {"start": {"line": 16, "character": 11}, "end": {"line": 16, "character": 18}}}, + "sortText": "5", "label": "trace.PrettyPrinter.format.input", "kind": 10, "detail": - "(false), enable/disable tracing for the given module and submodules"}], + "(false), enable/disable tracing for the given module and submodules", + "data": + {"params": + {"textDocument": {"uri": "file:///completionOption.lean"}, + "position": {"line": 16, "character": 18}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrefixIssue.lean.expected.out b/tests/lean/interactive/completionPrefixIssue.lean.expected.out index 903119b94fa4..04b1fda66fd9 100644 --- a/tests/lean/interactive/completionPrefixIssue.lean.expected.out +++ b/tests/lean/interactive/completionPrefixIssue.lean.expected.out @@ -1,8 +1,20 @@ {"textDocument": {"uri": "file:///completionPrefixIssue.lean"}, "position": {"line": 1, "character": 64}} {"items": - [{"label": "veryLongDefinitionName", "kind": 6, "detail": "Nat"}, - {"label": "veryLongDefinitionNameVeryLongDefinitionName", + [{"sortText": "0", + "label": "veryLongDefinitionName", + "kind": 6, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrefixIssue.lean"}, + "position": {"line": 1, "character": 64}}, + "id": {"fvar": "_uniq.29"}}}, + {"sortText": "1", + "label": "veryLongDefinitionNameVeryLongDefinitionName", "kind": 21, - "detail": "Nat"}], + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrefixIssue.lean"}, + "position": {"line": 1, "character": 64}}, + "id": {"const": "veryLongDefinitionNameVeryLongDefinitionName"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrivateTypes.lean b/tests/lean/interactive/completionPrivateTypes.lean new file mode 100644 index 000000000000..087005c9a54f --- /dev/null +++ b/tests/lean/interactive/completionPrivateTypes.lean @@ -0,0 +1,5 @@ +private structure Foo where + x : Nat + +def foobar (f : Foo) := f. + --^ textDocument/completion diff --git a/tests/lean/interactive/completionPrivateTypes.lean.expected.out b/tests/lean/interactive/completionPrivateTypes.lean.expected.out new file mode 100644 index 000000000000..b59b710c7a27 --- /dev/null +++ b/tests/lean/interactive/completionPrivateTypes.lean.expected.out @@ -0,0 +1,12 @@ +{"textDocument": {"uri": "file:///completionPrivateTypes.lean"}, + "position": {"line": 3, "character": 26}} +{"items": + [{"sortText": "0", + "label": "x", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrivateTypes.lean"}, + "position": {"line": 3, "character": 26}}, + "id": {"const": "_private.0.Foo.x"}}}], + "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index 87db18785039..33264eb9a71c 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/tests/lean/interactive/completionPrv.lean.expected.out @@ -1,22 +1,72 @@ {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 2, "character": 11}} -{"items": [{"label": "blaBlaBoo", "kind": 21, "detail": "Nat"}], +{"items": + [{"sortText": "0", + "label": "blaBlaBoo", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 2, "character": 11}}, + "id": {"const": "_private.0.blaBlaBoo"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 9, "character": 11}} {"items": - [{"label": "booBoo", "kind": 21, "detail": "Nat"}, - {"label": "instToBoolBool", "kind": 21, "detail": "ToBool Bool"}], + [{"sortText": "0", + "label": "booBoo", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 9, "character": 11}}, + "id": {"const": "_private.0.Foo.booBoo"}}}, + {"sortText": "1", + "label": "instToBoolBool", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 9, "character": 11}}, + "id": {"const": "instToBoolBool"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 21, "character": 5}} {"items": - [{"label": "field1", "kind": 5, "detail": "S → Nat"}, - {"label": "getInc", "kind": 3, "detail": "S → Nat"}], + [{"sortText": "0", + "label": "field1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 21, "character": 5}}, + "id": {"const": "S.field1"}}}, + {"sortText": "1", + "label": "getInc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 21, "character": 5}}, + "id": {"const": "_private.0.S.getInc"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 25, "character": 4}} {"items": - [{"label": "field1", "kind": 5, "detail": "S → Nat"}, - {"label": "getInc", "kind": 3, "detail": "S → Nat"}], + [{"sortText": "0", + "label": "field1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 25, "character": 4}}, + "id": {"const": "S.field1"}}}, + {"sortText": "1", + "label": "getInc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///completionPrv.lean"}, + "position": {"line": 25, "character": 4}}, + "id": {"const": "_private.0.S.getInc"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/dotIdCompletion.lean.expected.out b/tests/lean/interactive/dotIdCompletion.lean.expected.out index cec637cc5f0b..bca1c47286cf 100644 --- a/tests/lean/interactive/dotIdCompletion.lean.expected.out +++ b/tests/lean/interactive/dotIdCompletion.lean.expected.out @@ -1,6 +1,20 @@ {"textDocument": {"uri": "file:///dotIdCompletion.lean"}, "position": {"line": 4, "character": 5}} {"items": - [{"label": "true", "kind": 4, "detail": "Boo"}, - {"label": "truth", "kind": 4, "detail": "Boo"}], + [{"sortText": "0", + "label": "true", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///dotIdCompletion.lean"}, + "position": {"line": 4, "character": 5}}, + "id": {"const": "Boo.true"}}}, + {"sortText": "1", + "label": "truth", + "kind": 4, + "data": + {"params": + {"textDocument": {"uri": "file:///dotIdCompletion.lean"}, + "position": {"line": 4, "character": 5}}, + "id": {"const": "Boo.truth"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/editCompletion.lean.expected.out b/tests/lean/interactive/editCompletion.lean.expected.out index 7625ab84e90e..b28a99504cba 100644 --- a/tests/lean/interactive/editCompletion.lean.expected.out +++ b/tests/lean/interactive/editCompletion.lean.expected.out @@ -6,5 +6,13 @@ "end": {"line": 3, "character": 22}}}]} {"textDocument": {"uri": "file:///editCompletion.lean"}, "position": {"line": 3, "character": 22}} -{"items": [{"label": "foo", "kind": 5, "detail": "Foo → Nat"}], +{"items": + [{"sortText": "0", + "label": "foo", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///editCompletion.lean"}, + "position": {"line": 3, "character": 22}}, + "id": {"const": "Foo.foo"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/inWordCompletion.lean.expected.out b/tests/lean/interactive/inWordCompletion.lean.expected.out index f55b50f1a5f6..fcb5cd52e577 100644 --- a/tests/lean/interactive/inWordCompletion.lean.expected.out +++ b/tests/lean/interactive/inWordCompletion.lean.expected.out @@ -1,14 +1,56 @@ {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 4, "character": 11}} {"items": - [{"label": "gfxabc", "kind": 3, "detail": "Nat → Nat"}, - {"label": "gfxacc", "kind": 3, "detail": "Nat → Nat"}, - {"label": "gfxadc", "kind": 3, "detail": "Nat → Nat"}], + [{"sortText": "0", + "label": "gfxabc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///inWordCompletion.lean"}, + "position": {"line": 4, "character": 11}}, + "id": {"const": "gfxabc"}}}, + {"sortText": "1", + "label": "gfxacc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///inWordCompletion.lean"}, + "position": {"line": 4, "character": 11}}, + "id": {"const": "gfxacc"}}}, + {"sortText": "2", + "label": "gfxadc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///inWordCompletion.lean"}, + "position": {"line": 4, "character": 11}}, + "id": {"const": "gfxadc"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 12, "character": 15}} {"items": - [{"label": "gfxabc", "kind": 3, "detail": "Nat → Nat"}, - {"label": "gfxacc", "kind": 3, "detail": "Nat → Nat"}, - {"label": "gfxadc", "kind": 3, "detail": "Nat → Nat"}], + [{"sortText": "0", + "label": "gfxabc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///inWordCompletion.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "Boo.gfxabc"}}}, + {"sortText": "1", + "label": "gfxacc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///inWordCompletion.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "Boo.gfxacc"}}}, + {"sortText": "2", + "label": "gfxadc", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///inWordCompletion.lean"}, + "position": {"line": 12, "character": 15}}, + "id": {"const": "Boo.gfxadc"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/internalNamesIssue.lean.expected.out b/tests/lean/interactive/internalNamesIssue.lean.expected.out index f71d1926f9c2..89f19119993e 100644 --- a/tests/lean/interactive/internalNamesIssue.lean.expected.out +++ b/tests/lean/interactive/internalNamesIssue.lean.expected.out @@ -1,6 +1,20 @@ {"textDocument": {"uri": "file:///internalNamesIssue.lean"}, "position": {"line": 9, "character": 11}} {"items": - [{"label": "bla", "kind": 3, "detail": "Nat → Nat"}, - {"label": "foo", "kind": 3, "detail": "Nat → Nat"}], + [{"sortText": "0", + "label": "bla", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///internalNamesIssue.lean"}, + "position": {"line": 9, "character": 11}}, + "id": {"const": "Foo.bla"}}}, + {"sortText": "1", + "label": "foo", + "kind": 3, + "data": + {"params": + {"textDocument": {"uri": "file:///internalNamesIssue.lean"}, + "position": {"line": 9, "character": 11}}, + "id": {"const": "Foo.foo"}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out index ac4cd1ef7e3b..81864a085616 100644 --- a/tests/lean/interactive/keywordCompletion.lean.expected.out +++ b/tests/lean/interactive/keywordCompletion.lean.expected.out @@ -1,14 +1,64 @@ {"textDocument": {"uri": "file:///keywordCompletion.lean"}, "position": {"line": 4, "character": 10}} {"items": - [{"label": "bin", "kind": 21, "detail": "Type 1"}, - {"label": "binder_predicate", "kind": 14, "detail": "keyword"}, - {"label": "binop%", "kind": 14, "detail": "keyword"}, - {"label": "binop_lazy%", "kind": 14, "detail": "keyword"}, - {"label": "binrel%", "kind": 14, "detail": "keyword"}, - {"label": "binrel_no_prop%", "kind": 14, "detail": "keyword"}], + [{"sortText": "0", + "label": "bin", + "kind": 21, + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 10}}, + "id": {"const": "bin"}}}, + {"sortText": "1", + "label": "binder_predicate", + "kind": 14, + "detail": "keyword", + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 10}}}}, + {"sortText": "2", + "label": "binop%", + "kind": 14, + "detail": "keyword", + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 10}}}}, + {"sortText": "3", + "label": "binop_lazy%", + "kind": 14, + "detail": "keyword", + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 10}}}}, + {"sortText": "4", + "label": "binrel%", + "kind": 14, + "detail": "keyword", + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 10}}}}, + {"sortText": "5", + "label": "binrel_no_prop%", + "kind": 14, + "detail": "keyword", + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 10}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///keywordCompletion.lean"}, "position": {"line": 4, "character": 13}} -{"items": [{"label": "binop_lazy%", "kind": 14, "detail": "keyword"}], +{"items": + [{"sortText": "0", + "label": "binop_lazy%", + "kind": 14, + "detail": "keyword", + "data": + {"params": + {"textDocument": {"uri": "file:///keywordCompletion.lean"}, + "position": {"line": 4, "character": 13}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/match.lean.expected.out b/tests/lean/interactive/match.lean.expected.out index 55e628339f95..fd6471bbe1d5 100644 --- a/tests/lean/interactive/match.lean.expected.out +++ b/tests/lean/interactive/match.lean.expected.out @@ -1,16 +1,58 @@ {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 6, "character": 11}} {"items": - [{"label": "fn1", "kind": 5, "detail": "S → Nat"}, - {"label": "name", "kind": 5, "detail": "S → String"}, - {"label": "value", "kind": 5, "detail": "S → Bool"}], + [{"sortText": "0", + "label": "fn1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///match.lean"}, + "position": {"line": 6, "character": 11}}, + "id": {"const": "S.fn1"}}}, + {"sortText": "1", + "label": "name", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///match.lean"}, + "position": {"line": 6, "character": 11}}, + "id": {"const": "S.name"}}}, + {"sortText": "2", + "label": "value", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///match.lean"}, + "position": {"line": 6, "character": 11}}, + "id": {"const": "S.value"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 10, "character": 10}} {"items": - [{"label": "fn1", "kind": 5, "detail": "S → Nat"}, - {"label": "name", "kind": 5, "detail": "S → String"}, - {"label": "value", "kind": 5, "detail": "S → Bool"}], + [{"sortText": "0", + "label": "fn1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///match.lean"}, + "position": {"line": 10, "character": 10}}, + "id": {"const": "S.fn1"}}}, + {"sortText": "1", + "label": "name", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///match.lean"}, + "position": {"line": 10, "character": 10}}, + "id": {"const": "S.name"}}}, + {"sortText": "2", + "label": "value", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///match.lean"}, + "position": {"line": 10, "character": 10}}, + "id": {"const": "S.value"}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 14, "character": 2}} diff --git a/tests/lean/interactive/matchStxCompletion.lean.expected.out b/tests/lean/interactive/matchStxCompletion.lean.expected.out index 427e2a554ec0..31598dd7531d 100644 --- a/tests/lean/interactive/matchStxCompletion.lean.expected.out +++ b/tests/lean/interactive/matchStxCompletion.lean.expected.out @@ -1,7 +1,28 @@ {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, "position": {"line": 8, "character": 9}} {"items": - [{"label": "b1", "kind": 5, "detail": "C → String"}, - {"label": "f1", "kind": 5, "detail": "C → Nat"}, - {"label": "f2", "kind": 5, "detail": "C → Bool"}], + [{"sortText": "0", + "label": "b1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, + "position": {"line": 8, "character": 9}}, + "id": {"const": "C.b1"}}}, + {"sortText": "1", + "label": "f1", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, + "position": {"line": 8, "character": 9}}, + "id": {"const": "C.f1"}}}, + {"sortText": "2", + "label": "f2", + "kind": 5, + "data": + {"params": + {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, + "position": {"line": 8, "character": 9}}, + "id": {"const": "C.f2"}}}], "isIncomplete": true} From 634bebc09d853187d91b96aaa8bb3c5900b1f3ff Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 23 Feb 2024 09:38:22 +0100 Subject: [PATCH 2/4] chore: missing prelude --- src/Lean/Server/CompletionItemData.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Server/CompletionItemData.lean b/src/Lean/Server/CompletionItemData.lean index 160d6ebe4e23..74024b02c5ba 100644 --- a/src/Lean/Server/CompletionItemData.lean +++ b/src/Lean/Server/CompletionItemData.lean @@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Marc Huisinga -/ +prelude import Lean.Server.FileSource namespace Lean.Lsp From baaedf053b10011ebacb86c361db4b9dbc94a1a4 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 23 Feb 2024 15:09:24 +0100 Subject: [PATCH 3/4] doc: missing doc comments --- src/Lean/Elab/InfoTree/Main.lean | 4 ++ src/Lean/Server/Completion.lean | 62 ++++++++++++++++++- src/Lean/Server/CompletionItemData.lean | 10 +++ .../Server/FileWorker/RequestHandling.lean | 7 +++ src/Lean/Server/ImportCompletion.lean | 5 ++ src/Lean/Server/Requests.lean | 8 +++ 6 files changed, 93 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index f0138fb71351..71ef2e6f594f 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -58,6 +58,10 @@ def CompletionInfo.stx : CompletionInfo → Syntax | endSection stx .. => stx | tactic stx .. => stx +/-- +Obtains the `LocalContext` from this `CompletionInfo` if available and yields an empty context +otherwise. +-/ def CompletionInfo.lctx : CompletionInfo → LocalContext | dot i .. => i.lctx | id _ _ _ lctx .. => lctx diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index c53aa20e7162..bf4394c2f17d 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -31,9 +31,14 @@ private partial def Lean.Server.Completion.consumeImplicitPrefix (e : Expr) (k : namespace Lean.Lsp +/-- +Identifier that is sent from the server to the client as part of the `CompletionItem.data?` field. +Needed to resolve the `CompletionItem` when the client sends a `completionItem/resolve` request +for that item, again containing the `data?` field provided by the server. +-/ inductive CompletionIdentifier where | const (declName : Name) - | fvar (id : FVarId) + | fvar (id : FVarId) instance : ToJson CompletionIdentifier where toJson @@ -48,11 +53,17 @@ instance : FromJson CompletionIdentifier where return .fvar id .error "invalid CompletionItemData" -structure CompletionItemDataWithId where - params : CompletionParams +/-- +`CompletionItemData` that also contains a `CompletionIdentifier`. +See the documentation of`CompletionItemData` and `CompletionIdentifier`. +-/ +structure CompletionItemDataWithId extends CompletionItemData where id? : Option CompletionIdentifier deriving FromJson, ToJson +/-- +Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id`. +-/ def CompletionItem.resolve (item : CompletionItem) (id : CompletionIdentifier) @@ -82,8 +93,10 @@ open Elab open Meta open FuzzyMatching +/-- Cached header declarations for which `allowCompletion headerEnv decl` is true. -/ builtin_initialize eligibleHeaderDeclsRef : IO.Ref (HashMap Name ConstantInfo) ← IO.mkRef {} +/-- Caches the declarations in the header for which `allowCompletion headerEnv decl` is true. -/ def fillEligibleHeaderDecls (headerEnv : Environment) : IO Unit := do eligibleHeaderDeclsRef.modify fun startEligibleHeaderDecls => (·.2) <| StateT.run (m := Id) (s := startEligibleHeaderDecls) do @@ -94,6 +107,7 @@ def fillEligibleHeaderDecls (headerEnv : Environment) : IO Unit := do else eligibleHeaderDecls +/-- Iterate over all declarations that are allowed in completion results. -/ private def forEligibleDeclsM [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (f : Name → ConstantInfo → m PUnit) : m PUnit := do let env ← getEnv @@ -103,6 +117,7 @@ private def forEligibleDeclsM [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorl if allowCompletion env name then f name c +/-- Checks whether this declaration can appear in completion results. -/ private def allowCompletion [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) m] (declName : Name) : m Bool := do let env ← getEnv @@ -112,6 +127,10 @@ private def allowCompletion [Monad m] [MonadEnv m] [MonadLiftT (ST IO.RealWorld) return true return false +/-- +Sorts `items` descendingly according to their score and ascendingly according to their label +for equal scores. +-/ private def sortCompletionItems (items : Array (CompletionItem × Float)) : Array CompletionItem := let items := items.qsort fun (i1, s1) (i2, s2) => if s1 != s2 then @@ -120,11 +139,18 @@ private def sortCompletionItems (items : Array (CompletionItem × Float)) : Arra i1.label.map (·.toLower) < i2.label.map (·.toLower) items.map (·.1) +/-- Intermediate state while completions are being computed. -/ structure State where + /-- All completion items and their fuzzy match scores so far. -/ items : Array (CompletionItem × Float) := #[] +/-- +Monad used for completion computation that allows modifying a completion `State` and reading +`CompletionParams`. +-/ abbrev M := OptionT $ ReaderT CompletionParams $ StateRefT State MetaM +/-- Adds a new completion item to the state in `M`. -/ private def addItem (item : CompletionItem) (score : Float) @@ -135,6 +161,10 @@ private def addItem let item := { item with data? := toJson data } modify fun s => { s with items := s.items.push (item, score) } +/-- +Adds a new completion item with the given `label`, `id`, `kind` and `score` to the state in `M`. +Computes the doc string from the environment if available. +-/ private def addUnresolvedCompletionItem (label : Name) (id : CompletionIdentifier) @@ -422,15 +452,26 @@ private def isDotCompletionMethod (typeName : Name) (info : ConstantInfo) : Meta return true return false +/-- +Checks whether the expected type of `info.type` can be reduced to an application of `typeName`. +-/ private def isDotIdCompletionMethod (typeName : Name) (info : ConstantInfo) : MetaM Bool := do forallTelescopeReducing info.type fun _ type => isDefEqToAppOf type.consumeMData typeName +/-- +Converts `n` to `Name.anonymous` if `n` is a private prefix (see `Lean.isPrivatePrefix`). +-/ private def stripPrivatePrefix (n : Name) : Name := match n with | .num _ 0 => if isPrivatePrefix n then .anonymous else n | _ => n +/-- +Compares `n₁` and `n₂` modulo private prefixes. Similar to `Name.cmp` but ignores all +private prefixes in both names. +Necessary because the namespaces of private names do not contain private prefixes. +-/ partial def cmpModPrivate (n₁ n₂ : Name) : Ordering := let n₁ := stripPrivatePrefix n₁ let n₂ := stripPrivatePrefix n₂ @@ -449,6 +490,12 @@ partial def cmpModPrivate (n₁ n₂ : Name) : Ordering := | Ordering.eq => cmpModPrivate p₁ p₂ | ord => ord +/-- +`NameSet` where names are compared according to `cmpModPrivate`. +Helps speed up dot completion because it allows us to look up names without first having to +strip the private prefix from deep in the name, letting us reject most names without +having to scan the full name first. +-/ def NameSetModPrivate := RBTree Name cmpModPrivate /-- @@ -667,6 +714,11 @@ where else best? +/-- +Assigns the `CompletionItem.sortText?` for all items in `completions` according to their order +in `completions`. This is necessary because clients will use their own sort order if the server +does not set it. +-/ private def assignSortTexts (completions : CompletionList) : CompletionList := Id.run do if completions.items.isEmpty then return completions @@ -705,6 +757,10 @@ partial def find? | _ => return none return completionList?.map assignSortTexts +/-- +Fills the `CompletionItem.detail?` field of `item` using the pretty-printed type identified by `id` +in the context found at `hoverPos` in `infoTree`. +-/ def resolveCompletionItem? (fileMap : FileMap) (hoverPos : String.Pos) diff --git a/src/Lean/Server/CompletionItemData.lean b/src/Lean/Server/CompletionItemData.lean index 74024b02c5ba..313c9600513e 100644 --- a/src/Lean/Server/CompletionItemData.lean +++ b/src/Lean/Server/CompletionItemData.lean @@ -13,6 +13,16 @@ structure CompletionItemData where params : CompletionParams deriving FromJson, ToJson +/-- +Yields the file source of `item` by attempting to parse `item.data?` to `CompletionItemData` and +obtaining the original file source from its `params` fields. Panics if `item.data?` is not present +or cannot be parsed to `CompletionItemData`. +Used when `completionItem/resolve` requests pass the watchdog to decide which file worker to forward +the request to. +Since this function can panic and clients typically send `completionItem/resolve` requests for every +selected completion item, all completion items returned by the server in `textDocument/completion` +requests must have a `data?` field that can be parsed to `CompletionItemData`. +-/ def CompletionItem.getFileSource! (item : CompletionItem) : DocumentUri := let r : Except String DocumentUri := do let some data := item.data? diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 99d537882bbd..2f1ee1b78b9c 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -44,6 +44,13 @@ def handleCompletion (p : CompletionParams) return r return { items := #[ ], isIncomplete := true }) +/-- +Handles `completionItem/resolve` requests that are sent by the client after the user selects +a completion item that was provided by `textDocument/completion`. Resolving the item fills the +`detail?` field of the item with the pretty-printed type. +This control flow is necessary because pretty-printing the type for every single completion item +(even those never selected by the user) is inefficient. +-/ def handleCompletionItemResolve (item : CompletionItem) : RequestM (RequestTask CompletionItem) := do let doc ← readDoc diff --git a/src/Lean/Server/ImportCompletion.lean b/src/Lean/Server/ImportCompletion.lean index ca89b9da5210..9c6a540e7861 100644 --- a/src/Lean/Server/ImportCompletion.lean +++ b/src/Lean/Server/ImportCompletion.lean @@ -121,6 +121,11 @@ def collectAvailableImports : IO AvailableImports := do ImportCompletion.collectAvailableImportsFromSrcSearchPath | some availableImports => pure availableImports +/-- +Sets the `data?` field of every `CompletionItem` in `completionList` using `params`. Ensures that +`completionItem/resolve` requests can be routed to the correct file worker even for +`CompletionItem`s produced by the import completion. +-/ def addCompletionItemData (completionList : CompletionList) (params : CompletionParams) : CompletionList := let data := { params : Lean.Lsp.CompletionItemData } diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index de057cf8bca2..57e5ab5612bd 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -184,6 +184,10 @@ open Lsp structure RequestHandler where fileSource : Json → Except RequestError Lsp.DocumentUri handle : Json → RequestM (RequestTask Json) + /-- + Handler that is called by the file worker after processing the header with the header environment. + Enables request handlers to cache data related to imports. + -/ handleHeaderCaching : Environment → IO Unit builtin_initialize requestHandlers : IO.Ref (PersistentHashMap String RequestHandler) ← @@ -249,6 +253,10 @@ def chainLspRequestHandler (method : String) else throw <| IO.userError s!"Failed to chain LSP request handler for '{method}': no initial handler registered" +/-- +Runs the header caching handler for every single registered request handler using the given +`headerEnv`. +-/ def runHeaderCachingHandlers (headerEnv : Environment) : IO Unit := do (← requestHandlers.get).forM fun _ handler => handler.handleHeaderCaching headerEnv From 5c2ef8a8d575944d218cba3d6413c8b446f0cbe6 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 23 Feb 2024 15:42:39 +0100 Subject: [PATCH 4/4] chore: review comments --- src/Lean/Elab/BuiltinTerm.lean | 2 +- src/Lean/Meta/CompletionName.lean | 8 ++-- src/Lean/Server/Completion.lean | 14 +------ tests/lean/interactive/1265.lean.expected.out | 40 +++++++++---------- tests/lean/interactive/1659.lean.expected.out | 26 ++++++------ tests/lean/interactive/533.lean.expected.out | 4 +- tests/lean/interactive/863.lean.expected.out | 8 ++-- .../interactive/compHeader.lean.expected.out | 4 +- .../interactive/completion.lean.expected.out | 8 ++-- .../interactive/completion2.lean.expected.out | 30 +++++++------- .../interactive/completion3.lean.expected.out | 24 +++++------ .../interactive/completion4.lean.expected.out | 24 +++++------ .../interactive/completion5.lean.expected.out | 6 +-- .../interactive/completion6.lean.expected.out | 22 +++++----- .../interactive/completion7.lean.expected.out | 8 ++-- .../completionAtPrint.lean.expected.out | 4 +- .../completionCheck.lean.expected.out | 4 +- .../completionDocString.lean.expected.out | 4 +- .../completionEOF.lean.expected.out | 2 +- ...mpletionFromExpectedType.lean.expected.out | 2 +- .../completionIStr.lean.expected.out | 6 +-- ...completionOpenNamespaces.lean.expected.out | 4 +- .../completionPrefixIssue.lean.expected.out | 5 ++- .../completionPrivateTypes.lean.expected.out | 2 +- .../completionPrv.lean.expected.out | 14 +++---- .../dotIdCompletion.lean.expected.out | 4 +- .../editCompletion.lean.expected.out | 2 +- .../inWordCompletion.lean.expected.out | 12 +++--- .../internalNamesIssue.lean.expected.out | 4 +- .../keywordCompletion.lean.expected.out | 2 +- .../lean/interactive/match.lean.expected.out | 12 +++--- .../matchStxCompletion.lean.expected.out | 6 +-- 32 files changed, 154 insertions(+), 163 deletions(-) diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 4600760c3b09..e8ac2da4e9c0 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -159,7 +159,7 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?) @[builtin_term_elab Lean.Parser.Term.cdot] def elabBadCDot : TermElab := fun stx expectedType? => do - if let `(.) := stx then + if stx[0].getAtomVal == "." then -- Users may input bad cdots because they are trying to auto-complete them using the expected type addCompletionInfo <| CompletionInfo.dotId stx .anonymous (← getLCtx) expectedType? throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)" diff --git a/src/Lean/Meta/CompletionName.lean b/src/Lean/Meta/CompletionName.lean index fcaf01e42669..4465447a3a4c 100644 --- a/src/Lean/Meta/CompletionName.lean +++ b/src/Lean/Meta/CompletionName.lean @@ -34,16 +34,16 @@ Checks whether a given name is internal due to something other than `_private`. Correctly deals with names like `_private..0.._sizeOf_1` in a private type `SomeType`, which `n.isInternal && !isPrivateName n` does not. -/ -private def isNonPrivateInternalName : Name → Bool - | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isNonPrivateInternalName p - | .num p _ => isNonPrivateInternalName p +private def isInternalNameModuloPrivate : Name → Bool + | n@(.str p s) => s.get 0 == '_' && n != privateHeader || isInternalNameModuloPrivate p + | .num p _ => isInternalNameModuloPrivate p | _ => false /-- Return true if name is blacklisted for completion purposes. -/ private def isBlacklisted (env : Environment) (declName : Name) : Bool := - isNonPrivateInternalName declName + isInternalNameModuloPrivate declName || isAuxRecursor env declName || isNoConfusion env declName || isRecCore env declName diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index bf4394c2f17d..6c981c7a2593 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -39,19 +39,7 @@ for that item, again containing the `data?` field provided by the server. inductive CompletionIdentifier where | const (declName : Name) | fvar (id : FVarId) - -instance : ToJson CompletionIdentifier where - toJson - | .const declName => Json.mkObj [("const", toJson declName)] - | .fvar id => Json.mkObj [("fvar", toJson id)] - -instance : FromJson CompletionIdentifier where - fromJson? j := do - if let .ok declName := j.getObjValAs? Name "const" then - return .const declName - if let .ok id := j.getObjValAs? FVarId "fvar" then - return .fvar id - .error "invalid CompletionItemData" + deriving FromJson, ToJson /-- `CompletionItemData` that also contains a `CompletionIdentifier`. diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out index 322acc7753d4..abe2bf402d4e 100644 --- a/tests/lean/interactive/1265.lean.expected.out +++ b/tests/lean/interactive/1265.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.expandInterpolatedStr"}}}, + "id": {"const": {"declName": "Lean.TSyntax.expandInterpolatedStr"}}}}, {"sortText": "1", "label": "getChar", "kind": 3, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getChar"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getChar"}}}}, {"sortText": "2", "label": "getDocString", "kind": 3, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getDocString"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getDocString"}}}}, {"sortText": "3", "label": "getHygieneInfo", "kind": 3, @@ -32,7 +32,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getHygieneInfo"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getHygieneInfo"}}}}, {"sortText": "4", "label": "getId", "kind": 3, @@ -40,7 +40,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getId"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getId"}}}}, {"sortText": "5", "label": "getName", "kind": 3, @@ -48,7 +48,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getName"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getName"}}}}, {"sortText": "6", "label": "getNat", "kind": 3, @@ -56,7 +56,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getNat"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getNat"}}}}, {"sortText": "7", "label": "getScientific", "kind": 3, @@ -64,7 +64,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getScientific"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getScientific"}}}}, {"sortText": "8", "label": "getString", "kind": 3, @@ -72,7 +72,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.getString"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getString"}}}}, {"sortText": "9", "label": "raw", "kind": 5, @@ -82,7 +82,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 0, "character": 51}}, - "id": {"const": "Lean.TSyntax.raw"}}}], + "id": {"const": {"declName": "Lean.TSyntax.raw"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}} @@ -94,7 +94,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.expandInterpolatedStr"}}}, + "id": {"const": {"declName": "Lean.TSyntax.expandInterpolatedStr"}}}}, {"sortText": "1", "label": "getChar", "kind": 3, @@ -102,7 +102,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getChar"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getChar"}}}}, {"sortText": "2", "label": "getDocString", "kind": 3, @@ -110,7 +110,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getDocString"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getDocString"}}}}, {"sortText": "3", "label": "getHygieneInfo", "kind": 3, @@ -118,7 +118,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getHygieneInfo"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getHygieneInfo"}}}}, {"sortText": "4", "label": "getId", "kind": 3, @@ -126,7 +126,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getId"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getId"}}}}, {"sortText": "5", "label": "getName", "kind": 3, @@ -134,7 +134,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getName"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getName"}}}}, {"sortText": "6", "label": "getNat", "kind": 3, @@ -142,7 +142,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getNat"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getNat"}}}}, {"sortText": "7", "label": "getScientific", "kind": 3, @@ -150,7 +150,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getScientific"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getScientific"}}}}, {"sortText": "8", "label": "getString", "kind": 3, @@ -158,7 +158,7 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.getString"}}}, + "id": {"const": {"declName": "Lean.TSyntax.getString"}}}}, {"sortText": "9", "label": "raw", "kind": 5, @@ -168,5 +168,5 @@ {"params": {"textDocument": {"uri": "file:///1265.lean"}, "position": {"line": 2, "character": 53}}, - "id": {"const": "Lean.TSyntax.raw"}}}], + "id": {"const": {"declName": "Lean.TSyntax.raw"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/1659.lean.expected.out b/tests/lean/interactive/1659.lean.expected.out index ba7a5ef84b8f..dc26f41f1c31 100644 --- a/tests/lean/interactive/1659.lean.expected.out +++ b/tests/lean/interactive/1659.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 9, "character": 23}}, - "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + "id": {"const": {"declName": "Lean.Elab.Tactic.elabTermEnsuringType"}}}}, {"sortText": "1", "label": "Lean.Elab.Term.elabTermEnsuringType", "kind": 21, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 9, "character": 23}}, - "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], + "id": {"const": {"declName": "Lean.Elab.Term.elabTermEnsuringType"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 15, "character": 23}} @@ -28,7 +28,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 15, "character": 23}}, - "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + "id": {"const": {"declName": "Lean.Elab.Tactic.elabTermEnsuringType"}}}}, {"sortText": "1", "label": "Term.elabTermEnsuringType", "kind": 21, @@ -36,7 +36,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 15, "character": 23}}, - "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], + "id": {"const": {"declName": "Lean.Elab.Term.elabTermEnsuringType"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 21, "character": 23}} @@ -48,7 +48,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 21, "character": 23}}, - "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}, + "id": {"const": {"declName": "Lean.Elab.Term.elabTermEnsuringType"}}}}, {"sortText": "1", "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, @@ -56,7 +56,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 21, "character": 23}}, - "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}], + "id": {"const": {"declName": "Lean.Elab.Tactic.elabTermEnsuringType"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 27, "character": 23}} @@ -68,7 +68,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 27, "character": 23}}, - "id": {"const": "elabTermEnsuringType"}}}, + "id": {"const": {"declName": "elabTermEnsuringType"}}}}, {"sortText": "1", "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, @@ -76,7 +76,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 27, "character": 23}}, - "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + "id": {"const": {"declName": "Lean.Elab.Tactic.elabTermEnsuringType"}}}}, {"sortText": "2", "label": "Lean.Elab.Term.elabTermEnsuringType", "kind": 21, @@ -84,7 +84,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 27, "character": 23}}, - "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], + "id": {"const": {"declName": "Lean.Elab.Term.elabTermEnsuringType"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}} @@ -96,7 +96,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}}, - "id": {"const": "elabTermEnsuringType"}}}, + "id": {"const": {"declName": "elabTermEnsuringType"}}}}, {"sortText": "1", "label": "Lean.Elab.elabTermEnsuringType", "kind": 21, @@ -104,7 +104,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}}, - "id": {"const": "Lean.Elab.elabTermEnsuringType"}}}, + "id": {"const": {"declName": "Lean.Elab.elabTermEnsuringType"}}}}, {"sortText": "2", "label": "Lean.Elab.Tactic.elabTermEnsuringType", "kind": 21, @@ -112,7 +112,7 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}}, - "id": {"const": "Lean.Elab.Tactic.elabTermEnsuringType"}}}, + "id": {"const": {"declName": "Lean.Elab.Tactic.elabTermEnsuringType"}}}}, {"sortText": "3", "label": "Lean.Elab.Term.elabTermEnsuringType", "kind": 21, @@ -120,5 +120,5 @@ {"params": {"textDocument": {"uri": "file:///1659.lean"}, "position": {"line": 33, "character": 23}}, - "id": {"const": "Lean.Elab.Term.elabTermEnsuringType"}}}], + "id": {"const": {"declName": "Lean.Elab.Term.elabTermEnsuringType"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index d2940b5f5164..72e7be4fb911 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///533.lean"}, "position": {"line": 4, "character": 10}}, - "id": {"fvar": "_uniq.6"}}}, + "id": {"fvar": {"id": "_uniq.6"}}}}, {"sortText": "1", "label": "Foo", "kind": 6, @@ -16,5 +16,5 @@ {"params": {"textDocument": {"uri": "file:///533.lean"}, "position": {"line": 4, "character": 10}}, - "id": {"fvar": "_uniq.2"}}}], + "id": {"fvar": {"id": "_uniq.2"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/863.lean.expected.out b/tests/lean/interactive/863.lean.expected.out index 249740d5d3e1..6843b01e86c4 100644 --- a/tests/lean/interactive/863.lean.expected.out +++ b/tests/lean/interactive/863.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 9, "character": 12}}, - "id": {"const": "Lean.MonadRef.getRef"}}}, + "id": {"const": {"declName": "Lean.MonadRef.getRef"}}}}, {"sortText": "1", "label": "MonadRef.getRef", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 9, "character": 12}}, - "id": {"const": "Lean.MonadRef.getRef"}}}], + "id": {"const": {"declName": "Lean.MonadRef.getRef"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 13, "character": 12}} @@ -28,7 +28,7 @@ {"params": {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 13, "character": 12}}, - "id": {"const": "Lean.MonadRef.getRef"}}}, + "id": {"const": {"declName": "Lean.MonadRef.getRef"}}}}, {"sortText": "1", "label": "MonadRef.getRef", "kind": 5, @@ -36,5 +36,5 @@ {"params": {"textDocument": {"uri": "file:///863.lean"}, "position": {"line": 13, "character": 12}}, - "id": {"const": "Lean.MonadRef.getRef"}}}], + "id": {"const": {"declName": "Lean.MonadRef.getRef"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/compHeader.lean.expected.out b/tests/lean/interactive/compHeader.lean.expected.out index e76b8e0786b1..d4ca54fdbfdd 100644 --- a/tests/lean/interactive/compHeader.lean.expected.out +++ b/tests/lean/interactive/compHeader.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///compHeader.lean"}, "position": {"line": 2, "character": 22}}, - "id": {"fvar": "_uniq.7"}}}, + "id": {"fvar": {"id": "_uniq.7"}}}}, {"sortText": "1", "label": "veryLongNameForCompletion", "kind": 21, @@ -16,5 +16,5 @@ {"params": {"textDocument": {"uri": "file:///compHeader.lean"}, "position": {"line": 2, "character": 22}}, - "id": {"const": "veryLongNameForCompletion"}}}], + "id": {"const": {"declName": "veryLongNameForCompletion"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out index 12bfafefa755..09db65135461 100644 --- a/tests/lean/interactive/completion.lean.expected.out +++ b/tests/lean/interactive/completion.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 3, "character": 22}}, - "id": {"const": "Foo.foo"}}}], + "id": {"const": {"declName": "Foo.foo"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 5, "character": 23}} @@ -20,7 +20,7 @@ {"params": {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 5, "character": 23}}, - "id": {"const": "Foo.foo"}}}], + "id": {"const": {"declName": "Foo.foo"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 7, "character": 28}} @@ -32,7 +32,7 @@ {"params": {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 7, "character": 28}}, - "id": {"const": "Foo.foo"}}}], + "id": {"const": {"declName": "Foo.foo"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 9, "character": 29}} @@ -44,5 +44,5 @@ {"params": {"textDocument": {"uri": "file:///completion.lean"}, "position": {"line": 9, "character": 29}}, - "id": {"const": "Foo.foo"}}}], + "id": {"const": {"declName": "Foo.foo"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion2.lean.expected.out b/tests/lean/interactive/completion2.lean.expected.out index a760a3958d6b..6e34e1033472 100644 --- a/tests/lean/interactive/completion2.lean.expected.out +++ b/tests/lean/interactive/completion2.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 19, "character": 10}}, - "id": {"const": "Foo.Bla.ax1"}}}, + "id": {"const": {"declName": "Foo.Bla.ax1"}}}}, {"sortText": "1", "label": "ex1", "kind": 3, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 19, "character": 10}}, - "id": {"const": "Foo.Bla.ex1"}}}, + "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "2", "label": "ex2", "kind": 3, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 19, "character": 10}}, - "id": {"const": "Foo.Bla.ex2"}}}, + "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "3", "label": "ex3", "kind": 3, @@ -32,7 +32,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 19, "character": 10}}, - "id": {"const": "Foo.Bla.ex3"}}}], + "id": {"const": {"declName": "Foo.Bla.ex3"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}} @@ -44,7 +44,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}}, - "id": {"const": "Foo.Bla.ax1"}}}, + "id": {"const": {"declName": "Foo.Bla.ax1"}}}}, {"sortText": "1", "label": "ex1", "kind": 3, @@ -52,7 +52,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}}, - "id": {"const": "Foo.Bla.ex1"}}}, + "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "2", "label": "ex2", "kind": 3, @@ -60,7 +60,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}}, - "id": {"const": "Foo.Bla.ex2"}}}, + "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "3", "label": "ex3", "kind": 3, @@ -68,7 +68,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 25, "character": 6}}, - "id": {"const": "Foo.Bla.ex3"}}}], + "id": {"const": {"declName": "Foo.Bla.ex3"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}} @@ -80,7 +80,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}}, - "id": {"const": "Foo.Bla.ax1"}}}, + "id": {"const": {"declName": "Foo.Bla.ax1"}}}}, {"sortText": "1", "label": "ex1", "kind": 3, @@ -88,7 +88,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}}, - "id": {"const": "Foo.Bla.ex1"}}}, + "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "2", "label": "ex2", "kind": 3, @@ -96,7 +96,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}}, - "id": {"const": "Foo.Bla.ex2"}}}, + "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "3", "label": "ex3", "kind": 3, @@ -104,7 +104,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 30, "character": 21}}, - "id": {"const": "Foo.Bla.ex3"}}}], + "id": {"const": {"declName": "Foo.Bla.ex3"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 37, "character": 22}} @@ -116,7 +116,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 37, "character": 22}}, - "id": {"const": "Foo.Bla.ex1"}}}, + "id": {"const": {"declName": "Foo.Bla.ex1"}}}}, {"sortText": "1", "label": "ex2", "kind": 3, @@ -124,7 +124,7 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 37, "character": 22}}, - "id": {"const": "Foo.Bla.ex2"}}}, + "id": {"const": {"declName": "Foo.Bla.ex2"}}}}, {"sortText": "2", "label": "ex3", "kind": 3, @@ -132,5 +132,5 @@ {"params": {"textDocument": {"uri": "file:///completion2.lean"}, "position": {"line": 37, "character": 22}}, - "id": {"const": "Foo.Bla.ex3"}}}], + "id": {"const": {"declName": "Foo.Bla.ex3"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion3.lean.expected.out b/tests/lean/interactive/completion3.lean.expected.out index 640cc68ef365..e3f61c586b8e 100644 --- a/tests/lean/interactive/completion3.lean.expected.out +++ b/tests/lean/interactive/completion3.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 7, "character": 9}}, - "id": {"const": "S.b"}}}, + "id": {"const": {"declName": "S.b"}}}}, {"sortText": "1", "label": "x", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 7, "character": 9}}, - "id": {"const": "S.x"}}}, + "id": {"const": {"declName": "S.x"}}}}, {"sortText": "2", "label": "y", "kind": 5, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 7, "character": 9}}, - "id": {"const": "S.y"}}}], + "id": {"const": {"declName": "S.y"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 12, "character": 5}} @@ -36,7 +36,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 12, "character": 5}}, - "id": {"const": "S.b"}}}, + "id": {"const": {"declName": "S.b"}}}}, {"sortText": "1", "label": "x", "kind": 5, @@ -44,7 +44,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 12, "character": 5}}, - "id": {"const": "S.x"}}}, + "id": {"const": {"declName": "S.x"}}}}, {"sortText": "2", "label": "y", "kind": 5, @@ -52,7 +52,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 12, "character": 5}}, - "id": {"const": "S.y"}}}], + "id": {"const": {"declName": "S.y"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 16, "character": 5}} @@ -64,7 +64,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 16, "character": 5}}, - "id": {"const": "S.b"}}}, + "id": {"const": {"declName": "S.b"}}}}, {"sortText": "1", "label": "x", "kind": 5, @@ -72,7 +72,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 16, "character": 5}}, - "id": {"const": "S.x"}}}, + "id": {"const": {"declName": "S.x"}}}}, {"sortText": "2", "label": "y", "kind": 5, @@ -80,7 +80,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 16, "character": 5}}, - "id": {"const": "S.y"}}}], + "id": {"const": {"declName": "S.y"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 20, "character": 5}} @@ -92,7 +92,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 20, "character": 5}}, - "id": {"const": "S.b"}}}, + "id": {"const": {"declName": "S.b"}}}}, {"sortText": "1", "label": "x", "kind": 5, @@ -100,7 +100,7 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 20, "character": 5}}, - "id": {"const": "S.x"}}}, + "id": {"const": {"declName": "S.x"}}}}, {"sortText": "2", "label": "y", "kind": 5, @@ -108,5 +108,5 @@ {"params": {"textDocument": {"uri": "file:///completion3.lean"}, "position": {"line": 20, "character": 5}}, - "id": {"const": "S.y"}}}], + "id": {"const": {"declName": "S.y"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion4.lean.expected.out b/tests/lean/interactive/completion4.lean.expected.out index b9ae0f03c03c..f13560912614 100644 --- a/tests/lean/interactive/completion4.lean.expected.out +++ b/tests/lean/interactive/completion4.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 7, "character": 4}}, - "id": {"const": "S.fn1"}}}, + "id": {"const": {"declName": "S.fn1"}}}}, {"sortText": "1", "label": "fn2", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 7, "character": 4}}, - "id": {"const": "S.fn2"}}}, + "id": {"const": {"declName": "S.fn2"}}}}, {"sortText": "2", "label": "pred", "kind": 5, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 7, "character": 4}}, - "id": {"const": "S.pred"}}}], + "id": {"const": {"declName": "S.pred"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 11, "character": 10}} @@ -36,7 +36,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 11, "character": 10}}, - "id": {"const": "S.fn1"}}}, + "id": {"const": {"declName": "S.fn1"}}}}, {"sortText": "1", "label": "fn2", "kind": 5, @@ -44,7 +44,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 11, "character": 10}}, - "id": {"const": "S.fn2"}}}, + "id": {"const": {"declName": "S.fn2"}}}}, {"sortText": "2", "label": "pred", "kind": 5, @@ -52,7 +52,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 11, "character": 10}}, - "id": {"const": "S.pred"}}}], + "id": {"const": {"declName": "S.pred"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 16, "character": 11}} @@ -64,7 +64,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 16, "character": 11}}, - "id": {"const": "S.fn1"}}}, + "id": {"const": {"declName": "S.fn1"}}}}, {"sortText": "1", "label": "fn2", "kind": 5, @@ -72,7 +72,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 16, "character": 11}}, - "id": {"const": "S.fn2"}}}, + "id": {"const": {"declName": "S.fn2"}}}}, {"sortText": "2", "label": "pred", "kind": 5, @@ -80,7 +80,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 16, "character": 11}}, - "id": {"const": "S.pred"}}}], + "id": {"const": {"declName": "S.pred"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 20, "character": 21}} @@ -92,7 +92,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 20, "character": 21}}, - "id": {"const": "S.fn1"}}}, + "id": {"const": {"declName": "S.fn1"}}}}, {"sortText": "1", "label": "fn2", "kind": 5, @@ -100,7 +100,7 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 20, "character": 21}}, - "id": {"const": "S.fn2"}}}, + "id": {"const": {"declName": "S.fn2"}}}}, {"sortText": "2", "label": "pred", "kind": 5, @@ -108,5 +108,5 @@ {"params": {"textDocument": {"uri": "file:///completion4.lean"}, "position": {"line": 20, "character": 21}}, - "id": {"const": "S.pred"}}}], + "id": {"const": {"declName": "S.pred"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion5.lean.expected.out b/tests/lean/interactive/completion5.lean.expected.out index b84cf2c0edd5..152236a17a6b 100644 --- a/tests/lean/interactive/completion5.lean.expected.out +++ b/tests/lean/interactive/completion5.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion5.lean"}, "position": {"line": 9, "character": 15}}, - "id": {"const": "C.b1"}}}, + "id": {"const": {"declName": "C.b1"}}}}, {"sortText": "1", "label": "f1", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///completion5.lean"}, "position": {"line": 9, "character": 15}}, - "id": {"const": "C.f1"}}}, + "id": {"const": {"declName": "C.f1"}}}}, {"sortText": "2", "label": "f2", "kind": 5, @@ -24,5 +24,5 @@ {"params": {"textDocument": {"uri": "file:///completion5.lean"}, "position": {"line": 9, "character": 15}}, - "id": {"const": "C.f2"}}}], + "id": {"const": {"declName": "C.f2"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion6.lean.expected.out b/tests/lean/interactive/completion6.lean.expected.out index f297911e0d4f..f6cb7e7c4fb8 100644 --- a/tests/lean/interactive/completion6.lean.expected.out +++ b/tests/lean/interactive/completion6.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "C.b1"}}}, + "id": {"const": {"declName": "C.b1"}}}}, {"sortText": "1", "label": "f1", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "C.f1"}}}, + "id": {"const": {"declName": "C.f1"}}}}, {"sortText": "2", "label": "f2", "kind": 5, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "C.f2"}}}, + "id": {"const": {"declName": "C.f2"}}}}, {"sortText": "3", "label": "f3", "kind": 5, @@ -32,7 +32,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "D.f3"}}}, + "id": {"const": {"declName": "D.f3"}}}}, {"sortText": "4", "label": "toC", "kind": 5, @@ -40,7 +40,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "D.toC"}}}], + "id": {"const": {"declName": "D.toC"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}} @@ -52,7 +52,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}}, - "id": {"const": "C.b1"}}}, + "id": {"const": {"declName": "C.b1"}}}}, {"sortText": "1", "label": "doubleF1", "kind": 3, @@ -60,7 +60,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}}, - "id": {"const": "E.doubleF1"}}}, + "id": {"const": {"declName": "E.doubleF1"}}}}, {"sortText": "2", "label": "f1", "kind": 5, @@ -68,7 +68,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}}, - "id": {"const": "C.f1"}}}, + "id": {"const": {"declName": "C.f1"}}}}, {"sortText": "3", "label": "f2", "kind": 5, @@ -76,7 +76,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}}, - "id": {"const": "C.f2"}}}, + "id": {"const": {"declName": "C.f2"}}}}, {"sortText": "4", "label": "f3", "kind": 5, @@ -84,7 +84,7 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}}, - "id": {"const": "D.f3"}}}, + "id": {"const": {"declName": "D.f3"}}}}, {"sortText": "5", "label": "toC", "kind": 5, @@ -92,5 +92,5 @@ {"params": {"textDocument": {"uri": "file:///completion6.lean"}, "position": {"line": 21, "character": 4}}, - "id": {"const": "D.toC"}}}], + "id": {"const": {"declName": "D.toC"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completion7.lean.expected.out b/tests/lean/interactive/completion7.lean.expected.out index c1e2efa5a698..8b6d13ec7fef 100644 --- a/tests/lean/interactive/completion7.lean.expected.out +++ b/tests/lean/interactive/completion7.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 6, "character": 10}}, - "id": {"const": "And"}}}], + "id": {"const": {"declName": "And"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 8, "character": 11}} @@ -20,7 +20,7 @@ {"params": {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 8, "character": 11}}, - "id": {"const": "And.left"}}}, + "id": {"const": {"declName": "And.left"}}}}, {"sortText": "1", "label": "mk", "kind": 4, @@ -28,7 +28,7 @@ {"params": {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 8, "character": 11}}, - "id": {"const": "And.mk"}}}, + "id": {"const": {"declName": "And.mk"}}}}, {"sortText": "2", "label": "right", "kind": 5, @@ -36,5 +36,5 @@ {"params": {"textDocument": {"uri": "file:///completion7.lean"}, "position": {"line": 8, "character": 11}}, - "id": {"const": "And.right"}}}], + "id": {"const": {"declName": "And.right"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionAtPrint.lean.expected.out b/tests/lean/interactive/completionAtPrint.lean.expected.out index 4ac1f7722e74..bb2fc2b59efb 100644 --- a/tests/lean/interactive/completionAtPrint.lean.expected.out +++ b/tests/lean/interactive/completionAtPrint.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completionAtPrint.lean"}, "position": {"line": 2, "character": 25}}, - "id": {"const": "Lean.Environment.find?"}}}, + "id": {"const": {"declName": "Lean.Environment.find?"}}}}, {"sortText": "1", "label": "freeRegions", "kind": 3, @@ -20,5 +20,5 @@ {"params": {"textDocument": {"uri": "file:///completionAtPrint.lean"}, "position": {"line": 2, "character": 25}}, - "id": {"const": "Lean.Environment.freeRegions"}}}], + "id": {"const": {"declName": "Lean.Environment.freeRegions"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionCheck.lean.expected.out b/tests/lean/interactive/completionCheck.lean.expected.out index 0c1647a11e95..af03d40b5fb9 100644 --- a/tests/lean/interactive/completionCheck.lean.expected.out +++ b/tests/lean/interactive/completionCheck.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completionCheck.lean"}, "position": {"line": 6, "character": 33}}, - "id": {"const": "AVerySpecificStructureName"}}}, + "id": {"const": {"declName": "AVerySpecificStructureName"}}}}, {"sortText": "1", "label": "AVerySpecificStructureName2", "kind": 22, @@ -16,5 +16,5 @@ {"params": {"textDocument": {"uri": "file:///completionCheck.lean"}, "position": {"line": 6, "character": 33}}, - "id": {"const": "AVerySpecificStructureName2"}}}], + "id": {"const": {"declName": "AVerySpecificStructureName2"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out index 2d4a8aef4b6a..87577cd094a1 100644 --- a/tests/lean/interactive/completionDocString.lean.expected.out +++ b/tests/lean/interactive/completionDocString.lean.expected.out @@ -10,7 +10,7 @@ {"params": {"textDocument": {"uri": "file:///completionDocString.lean"}, "position": {"line": 0, "character": 20}}, - "id": {"const": "Array.insertAt"}}}, + "id": {"const": {"declName": "Array.insertAt"}}}}, {"sortText": "1", "label": "insertAt!", "kind": 3, @@ -22,5 +22,5 @@ {"params": {"textDocument": {"uri": "file:///completionDocString.lean"}, "position": {"line": 0, "character": 20}}, - "id": {"const": "Array.insertAt!"}}}], + "id": {"const": {"declName": "Array.insertAt!"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionEOF.lean.expected.out b/tests/lean/interactive/completionEOF.lean.expected.out index 370fd1ca3540..bffabbbf7909 100644 --- a/tests/lean/interactive/completionEOF.lean.expected.out +++ b/tests/lean/interactive/completionEOF.lean.expected.out @@ -8,5 +8,5 @@ {"params": {"textDocument": {"uri": "file:///completionEOF.lean"}, "position": {"line": 8, "character": 9}}, - "id": {"const": "And"}}}], + "id": {"const": {"declName": "And"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionFromExpectedType.lean.expected.out b/tests/lean/interactive/completionFromExpectedType.lean.expected.out index d94d7fab2fdc..938821b1d38c 100644 --- a/tests/lean/interactive/completionFromExpectedType.lean.expected.out +++ b/tests/lean/interactive/completionFromExpectedType.lean.expected.out @@ -8,5 +8,5 @@ {"params": {"textDocument": {"uri": "file:///completionFromExpectedType.lean"}, "position": {"line": 3, "character": 18}}, - "id": {"const": "Foo.mk"}}}], + "id": {"const": {"declName": "Foo.mk"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionIStr.lean.expected.out b/tests/lean/interactive/completionIStr.lean.expected.out index 6e8056aeef2a..2da7e5d5b6be 100644 --- a/tests/lean/interactive/completionIStr.lean.expected.out +++ b/tests/lean/interactive/completionIStr.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completionIStr.lean"}, "position": {"line": 5, "character": 34}}, - "id": {"const": "C.b1"}}}, + "id": {"const": {"declName": "C.b1"}}}}, {"sortText": "1", "label": "f1", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///completionIStr.lean"}, "position": {"line": 5, "character": 34}}, - "id": {"const": "C.f1"}}}, + "id": {"const": {"declName": "C.f1"}}}}, {"sortText": "2", "label": "f2", "kind": 5, @@ -24,5 +24,5 @@ {"params": {"textDocument": {"uri": "file:///completionIStr.lean"}, "position": {"line": 5, "character": 34}}, - "id": {"const": "C.f2"}}}], + "id": {"const": {"declName": "C.f2"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionOpenNamespaces.lean.expected.out b/tests/lean/interactive/completionOpenNamespaces.lean.expected.out index 5b3087dd01c7..468aaf3ced85 100644 --- a/tests/lean/interactive/completionOpenNamespaces.lean.expected.out +++ b/tests/lean/interactive/completionOpenNamespaces.lean.expected.out @@ -9,5 +9,7 @@ {"textDocument": {"uri": "file:///completionOpenNamespaces.lean"}, "position": {"line": 4, "character": 68}}, "id": - {"const": "A.B1.verySpecificDefinitionNameOfCompletionOpenNamespaces"}}}], + {"const": + {"declName": + "A.B1.verySpecificDefinitionNameOfCompletionOpenNamespaces"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrefixIssue.lean.expected.out b/tests/lean/interactive/completionPrefixIssue.lean.expected.out index 04b1fda66fd9..b56a773a16a6 100644 --- a/tests/lean/interactive/completionPrefixIssue.lean.expected.out +++ b/tests/lean/interactive/completionPrefixIssue.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrefixIssue.lean"}, "position": {"line": 1, "character": 64}}, - "id": {"fvar": "_uniq.29"}}}, + "id": {"fvar": {"id": "_uniq.29"}}}}, {"sortText": "1", "label": "veryLongDefinitionNameVeryLongDefinitionName", "kind": 21, @@ -16,5 +16,6 @@ {"params": {"textDocument": {"uri": "file:///completionPrefixIssue.lean"}, "position": {"line": 1, "character": 64}}, - "id": {"const": "veryLongDefinitionNameVeryLongDefinitionName"}}}], + "id": + {"const": {"declName": "veryLongDefinitionNameVeryLongDefinitionName"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrivateTypes.lean.expected.out b/tests/lean/interactive/completionPrivateTypes.lean.expected.out index b59b710c7a27..15004871556b 100644 --- a/tests/lean/interactive/completionPrivateTypes.lean.expected.out +++ b/tests/lean/interactive/completionPrivateTypes.lean.expected.out @@ -8,5 +8,5 @@ {"params": {"textDocument": {"uri": "file:///completionPrivateTypes.lean"}, "position": {"line": 3, "character": 26}}, - "id": {"const": "_private.0.Foo.x"}}}], + "id": {"const": {"declName": "_private.0.Foo.x"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out index 33264eb9a71c..a12f228c7444 100644 --- a/tests/lean/interactive/completionPrv.lean.expected.out +++ b/tests/lean/interactive/completionPrv.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 2, "character": 11}}, - "id": {"const": "_private.0.blaBlaBoo"}}}], + "id": {"const": {"declName": "_private.0.blaBlaBoo"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 9, "character": 11}} @@ -20,7 +20,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 9, "character": 11}}, - "id": {"const": "_private.0.Foo.booBoo"}}}, + "id": {"const": {"declName": "_private.0.Foo.booBoo"}}}}, {"sortText": "1", "label": "instToBoolBool", "kind": 21, @@ -28,7 +28,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 9, "character": 11}}, - "id": {"const": "instToBoolBool"}}}], + "id": {"const": {"declName": "instToBoolBool"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 21, "character": 5}} @@ -40,7 +40,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 21, "character": 5}}, - "id": {"const": "S.field1"}}}, + "id": {"const": {"declName": "S.field1"}}}}, {"sortText": "1", "label": "getInc", "kind": 3, @@ -48,7 +48,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 21, "character": 5}}, - "id": {"const": "_private.0.S.getInc"}}}], + "id": {"const": {"declName": "_private.0.S.getInc"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 25, "character": 4}} @@ -60,7 +60,7 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 25, "character": 4}}, - "id": {"const": "S.field1"}}}, + "id": {"const": {"declName": "S.field1"}}}}, {"sortText": "1", "label": "getInc", "kind": 3, @@ -68,5 +68,5 @@ {"params": {"textDocument": {"uri": "file:///completionPrv.lean"}, "position": {"line": 25, "character": 4}}, - "id": {"const": "_private.0.S.getInc"}}}], + "id": {"const": {"declName": "_private.0.S.getInc"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/dotIdCompletion.lean.expected.out b/tests/lean/interactive/dotIdCompletion.lean.expected.out index bca1c47286cf..1cca64cc656f 100644 --- a/tests/lean/interactive/dotIdCompletion.lean.expected.out +++ b/tests/lean/interactive/dotIdCompletion.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///dotIdCompletion.lean"}, "position": {"line": 4, "character": 5}}, - "id": {"const": "Boo.true"}}}, + "id": {"const": {"declName": "Boo.true"}}}}, {"sortText": "1", "label": "truth", "kind": 4, @@ -16,5 +16,5 @@ {"params": {"textDocument": {"uri": "file:///dotIdCompletion.lean"}, "position": {"line": 4, "character": 5}}, - "id": {"const": "Boo.truth"}}}], + "id": {"const": {"declName": "Boo.truth"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/editCompletion.lean.expected.out b/tests/lean/interactive/editCompletion.lean.expected.out index b28a99504cba..dc9667a3460e 100644 --- a/tests/lean/interactive/editCompletion.lean.expected.out +++ b/tests/lean/interactive/editCompletion.lean.expected.out @@ -14,5 +14,5 @@ {"params": {"textDocument": {"uri": "file:///editCompletion.lean"}, "position": {"line": 3, "character": 22}}, - "id": {"const": "Foo.foo"}}}], + "id": {"const": {"declName": "Foo.foo"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/inWordCompletion.lean.expected.out b/tests/lean/interactive/inWordCompletion.lean.expected.out index fcb5cd52e577..0c61f227a910 100644 --- a/tests/lean/interactive/inWordCompletion.lean.expected.out +++ b/tests/lean/interactive/inWordCompletion.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 4, "character": 11}}, - "id": {"const": "gfxabc"}}}, + "id": {"const": {"declName": "gfxabc"}}}}, {"sortText": "1", "label": "gfxacc", "kind": 3, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 4, "character": 11}}, - "id": {"const": "gfxacc"}}}, + "id": {"const": {"declName": "gfxacc"}}}}, {"sortText": "2", "label": "gfxadc", "kind": 3, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 4, "character": 11}}, - "id": {"const": "gfxadc"}}}], + "id": {"const": {"declName": "gfxadc"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 12, "character": 15}} @@ -36,7 +36,7 @@ {"params": {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "Boo.gfxabc"}}}, + "id": {"const": {"declName": "Boo.gfxabc"}}}}, {"sortText": "1", "label": "gfxacc", "kind": 3, @@ -44,7 +44,7 @@ {"params": {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "Boo.gfxacc"}}}, + "id": {"const": {"declName": "Boo.gfxacc"}}}}, {"sortText": "2", "label": "gfxadc", "kind": 3, @@ -52,5 +52,5 @@ {"params": {"textDocument": {"uri": "file:///inWordCompletion.lean"}, "position": {"line": 12, "character": 15}}, - "id": {"const": "Boo.gfxadc"}}}], + "id": {"const": {"declName": "Boo.gfxadc"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/internalNamesIssue.lean.expected.out b/tests/lean/interactive/internalNamesIssue.lean.expected.out index 89f19119993e..d2e2dd36fd53 100644 --- a/tests/lean/interactive/internalNamesIssue.lean.expected.out +++ b/tests/lean/interactive/internalNamesIssue.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///internalNamesIssue.lean"}, "position": {"line": 9, "character": 11}}, - "id": {"const": "Foo.bla"}}}, + "id": {"const": {"declName": "Foo.bla"}}}}, {"sortText": "1", "label": "foo", "kind": 3, @@ -16,5 +16,5 @@ {"params": {"textDocument": {"uri": "file:///internalNamesIssue.lean"}, "position": {"line": 9, "character": 11}}, - "id": {"const": "Foo.foo"}}}], + "id": {"const": {"declName": "Foo.foo"}}}}], "isIncomplete": true} diff --git a/tests/lean/interactive/keywordCompletion.lean.expected.out b/tests/lean/interactive/keywordCompletion.lean.expected.out index 81864a085616..19498180d631 100644 --- a/tests/lean/interactive/keywordCompletion.lean.expected.out +++ b/tests/lean/interactive/keywordCompletion.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///keywordCompletion.lean"}, "position": {"line": 4, "character": 10}}, - "id": {"const": "bin"}}}, + "id": {"const": {"declName": "bin"}}}}, {"sortText": "1", "label": "binder_predicate", "kind": 14, diff --git a/tests/lean/interactive/match.lean.expected.out b/tests/lean/interactive/match.lean.expected.out index fd6471bbe1d5..4965eee71f15 100644 --- a/tests/lean/interactive/match.lean.expected.out +++ b/tests/lean/interactive/match.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 6, "character": 11}}, - "id": {"const": "S.fn1"}}}, + "id": {"const": {"declName": "S.fn1"}}}}, {"sortText": "1", "label": "name", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 6, "character": 11}}, - "id": {"const": "S.name"}}}, + "id": {"const": {"declName": "S.name"}}}}, {"sortText": "2", "label": "value", "kind": 5, @@ -24,7 +24,7 @@ {"params": {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 6, "character": 11}}, - "id": {"const": "S.value"}}}], + "id": {"const": {"declName": "S.value"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 10, "character": 10}} @@ -36,7 +36,7 @@ {"params": {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 10, "character": 10}}, - "id": {"const": "S.fn1"}}}, + "id": {"const": {"declName": "S.fn1"}}}}, {"sortText": "1", "label": "name", "kind": 5, @@ -44,7 +44,7 @@ {"params": {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 10, "character": 10}}, - "id": {"const": "S.name"}}}, + "id": {"const": {"declName": "S.name"}}}}, {"sortText": "2", "label": "value", "kind": 5, @@ -52,7 +52,7 @@ {"params": {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 10, "character": 10}}, - "id": {"const": "S.value"}}}], + "id": {"const": {"declName": "S.value"}}}}], "isIncomplete": true} {"textDocument": {"uri": "file:///match.lean"}, "position": {"line": 14, "character": 2}} diff --git a/tests/lean/interactive/matchStxCompletion.lean.expected.out b/tests/lean/interactive/matchStxCompletion.lean.expected.out index 31598dd7531d..6e9e15b0974c 100644 --- a/tests/lean/interactive/matchStxCompletion.lean.expected.out +++ b/tests/lean/interactive/matchStxCompletion.lean.expected.out @@ -8,7 +8,7 @@ {"params": {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, "position": {"line": 8, "character": 9}}, - "id": {"const": "C.b1"}}}, + "id": {"const": {"declName": "C.b1"}}}}, {"sortText": "1", "label": "f1", "kind": 5, @@ -16,7 +16,7 @@ {"params": {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, "position": {"line": 8, "character": 9}}, - "id": {"const": "C.f1"}}}, + "id": {"const": {"declName": "C.f1"}}}}, {"sortText": "2", "label": "f2", "kind": 5, @@ -24,5 +24,5 @@ {"params": {"textDocument": {"uri": "file:///matchStxCompletion.lean"}, "position": {"line": 8, "character": 9}}, - "id": {"const": "C.f2"}}}], + "id": {"const": {"declName": "C.f2"}}}}], "isIncomplete": true}