max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: tactic name completion

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-03 15:45:44 -07:00
parent 20f569c033
commit 09ee8bddad
1 changed files with 18 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/Lean/Server/Completion.lean
View file

@ -7,6 +7,7 @@ import Lean.Environment
import Lean.Data.Lsp.LanguageFeatures
import Lean.Meta.Tactic.Apply
import Lean.Server.InfoUtils
import Lean.Parser.Extension
namespace Lean.Server.Completion
open Lsp
@ -86,7 +87,7 @@ private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax
if id.hasMacroScopes then return none
return none
private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option CompletionList) := do
private def optionCompletion (ctx : ContextInfo) : IO (Option CompletionList) := do
ctx.runMetaM {} do
let decls ← getOptionDecls
let opts ← getOptions
@ -94,12 +95,25 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option Com
items.push { label := name.toString, detail? := s!"({opts.get name decl.defValue}), {decl.descr}", documentation? := none }
return some { items := sortCompletionItems items, isIncomplete := true }
private def tacticCompletion (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 := table.fold (init := #[]) fun items tk parser =>
-- TODO pretty print tactic syntax
items.push { label := tk.toString, detail? := none, documentation? := none }
return some { items := sortCompletionItems items, isIncomplete := true }
partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTree) : IO (Option CompletionList) := do
let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with
| some (ctx, Info.ofCompletionInfo (CompletionInfo.dot info (expectedType? := expectedType?) ..)) => dotCompletion ctx info expectedType?
| some (ctx, Info.ofCompletionInfo (CompletionInfo.id stx lctx openDecls expectedType?)) => idCompletion ctx lctx stx openDecls expectedType?
| some (ctx, Info.ofCompletionInfo (CompletionInfo.option stx)) => optionCompletion ctx stx
| some (ctx, Info.ofCompletionInfo info) =>
match info with
| CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info expectedType?
| CompletionInfo.id stx lctx openDecls expectedType? => idCompletion ctx lctx stx openDecls expectedType?
| CompletionInfo.option .. => optionCompletion ctx
| CompletionInfo.tactic .. => tacticCompletion ctx
| _ => return none
| _ => return none
where
choose (fileMap : FileMap) (hoverLine : Nat) (ctx : ContextInfo) (info : Info) (best? : Option (ContextInfo × Info)) : Option (ContextInfo × Info) :=