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

feat: hover & go-to-definition for syntax (on first token)

Browse source
This commit is contained in:
Sebastian Ullrich 2021-06-09 19:18:19 +02:00 • committed by Leonardo de Moura
parent bae919355e
commit d44e2ea4bd
3 changed files with 120 additions and 97 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

118
src/Lean/Server/FileWorker/RequestHandling.lean
View file

@ -63,35 +63,45 @@ partial def handleDefinition (goToType? : Bool) (p : TextDocumentPositionParams)
let doc ← readDoc
let text := doc.meta.text
let hoverPos := text.lspPosToUtf8Pos p.position
let locationLinksFromDecl i n := do
let mod? ← findModuleOf? n
let modUri? ← match mod? with
| some modName =>
let modFname? ← rc.srcSearchPath.findWithExt "lean" modName
pure <| modFname?.map toFileUri
| none => pure <| some doc.meta.uri
let ranges? ← findDeclarationRanges? n
if let (some ranges, some modUri) := (ranges?, modUri?) then
let declRangeToLspRange (r : DeclarationRange) : Lsp.Range :=
{ start := ⟨r.pos.line - 1, r.charUtf16⟩
«end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ }
let ll : LocationLink := {
originSelectionRange? := (·.toLspRange text) <$> i.range?
targetUri := modUri
targetRange := declRangeToLspRange ranges.range
targetSelectionRange := declRangeToLspRange ranges.selectionRange
}
return #[ll]
return #[]
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure #[]) fun snap => do
for t in snap.cmdState.infoState.trees do
if let some (ci, Info.ofTermInfo i) := t.hoverableInfoAt? hoverPos then
let mut expr := i.expr
if goToType? then
expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType expr)
if let some n := expr.constName? then
let mod? ← ci.runMetaM i.lctx <| findModuleOf? n
let modUri? ← match mod? with
| some modName =>
let modFname? ← rc.srcSearchPath.findWithExt "lean" modName
pure <| modFname?.map toFileUri
| none => pure <| some doc.meta.uri
let ranges? ← ci.runMetaM i.lctx <| findDeclarationRanges? n
if let (some ranges, some modUri) := (ranges?, modUri?) then
let declRangeToLspRange (r : DeclarationRange) : Lsp.Range :=
{ start := ⟨r.pos.line - 1, r.charUtf16⟩
«end» := ⟨r.endPos.line - 1, r.endCharUtf16⟩ }
let ll : LocationLink := {
originSelectionRange? := some ⟨text.utf8PosToLspPos i.stx.getPos?.get!,
text.utf8PosToLspPos i.stx.getTailPos?.get!⟩
targetUri := modUri
targetRange := declRangeToLspRange ranges.range
targetSelectionRange := declRangeToLspRange ranges.selectionRange
}
return #[ll]
if let some (ci, i) := t.hoverableInfoAt? hoverPos then
if let Info.ofTermInfo ti := i then
let mut expr := ti.expr
if goToType? then
expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType expr)
if let some n := expr.constName? then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
if let some ei := i.toElabInfo? then
if ci.env.contains ei.elaborator then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
if ci.env.contains ei.stx.getKind then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
return #[]
open Elab in
@ -121,13 +131,6 @@ partial def handlePlainGoal (p : PlainGoalParams)
return none
def hasRange (stx : Syntax) : Bool :=
stx.getPos?.isSome && stx.getTailPos?.isSome
def rangeOfSyntax! (text : FileMap) (stx : Syntax) : Range :=
⟨text.utf8PosToLspPos <| stx.getPos?.get!,
text.utf8PosToLspPos <| stx.getTailPos?.get!⟩
open Elab in
partial def handlePlainTermGoal (p : PlainTermGoalParams)
: RequestM (RequestTask (Option PlainTermGoal)) := do
@ -137,11 +140,11 @@ partial def handlePlainTermGoal (p : PlainTermGoalParams)
withWaitFindSnap doc (fun s => s.endPos > hoverPos)
(notFoundX := pure none) fun snap => do
for t in snap.cmdState.infoState.trees do
if let some (ci, Info.ofTermInfo i) := t.termGoalAt? hoverPos then
if let some (ci, i@(Info.ofTermInfo ti)) := t.termGoalAt? hoverPos then
let goal ← ci.runMetaM i.lctx <| open Meta in do
let ty ← instantiateMVars <| i.expectedType?.getD (← inferType i.expr)
let ty ← instantiateMVars <| ti.expectedType?.getD (← inferType ti.expr)
withPPInaccessibleNames <| Meta.ppGoal (← mkFreshExprMVar ty).mvarId!
let range := if hasRange i.stx then rangeOfSyntax! text i.stx else ⟨p.position, p.position⟩
let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩
return some { goal := toString goal, range }
return none
@ -151,12 +154,12 @@ partial def handleDocumentHighlight (p : DocumentHighlightParams)
let text := doc.meta.text
let pos := text.lspPosToUtf8Pos p.position
let rec highlightReturn? (doRange? : Option Range) : Syntax → Option DocumentHighlight
| stx@`(doElem|return%$i $e) =>
if stx.getPos?.get! <= pos && pos < stx.getTailPos?.get! then
some { range := doRange?.getD (rangeOfSyntax! text i), kind? := DocumentHighlightKind.text }
else
highlightReturn? doRange? e
| `(do%$i $elems) => highlightReturn? (rangeOfSyntax! text i) elems
| stx@`(doElem|return%$i $e) => do
if let some range := i.getRange? then
if range.contains pos then
return some { range := doRange?.getD (range.toLspRange text), kind? := DocumentHighlightKind.text }
highlightReturn? doRange? e
| `(do%$i $elems) => highlightReturn? (i.getRange?.get!.toLspRange text) elems
| stx => stx.getArgs.findSome? (highlightReturn? doRange?)
withWaitFindSnap doc (fun s => s.endPos > pos)
@ -191,26 +194,25 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
| `(namespace $id) => sectionLikeToDocumentSymbols text stx stxs (id.getId.toString) SymbolKind.namespace id
| `(section $(id)?) => sectionLikeToDocumentSymbols text stx stxs ((·.getId.toString) <$> id |>.getD "<section>") SymbolKind.namespace (id.getD stx)
| `(end $(id)?) => ([], stx::stxs)
| _ =>
| _ => do
let (syms, stxs') := toDocumentSymbols text stxs
if stx.isOfKind ``Lean.Parser.Command.declaration && hasRange stx then
unless stx.isOfKind ``Lean.Parser.Command.declaration do
return (syms, stxs')
if let some stxRange := stx.getRange? then
let (name, selection) := match stx with
| `($dm:declModifiers $ak:attrKind instance $[$np:namedPrio]? $[$id:ident$[.{$ls,*}]?]? $sig:declSig $val) =>
((·.getId.toString) <$> id |>.getD s!"instance {sig.reprint.getD ""}", id.getD sig)
| _ => match stx[1][1] with
| `(declId|$id:ident$[.{$ls,*}]?) => (id.getId.toString, id)
| _ => (stx[1][0].isIdOrAtom?.getD "<unknown>", stx[1][0])
if hasRange selection then
(DocumentSymbol.mk {
if let some selRange := selection.getRange? then
return (DocumentSymbol.mk {
name := name
kind := SymbolKind.method
range := rangeOfSyntax! text stx
selectionRange := rangeOfSyntax! text selection
range := stxRange.toLspRange text
selectionRange := selRange.toLspRange text
} :: syms, stxs')
else
(syms, stxs')
else
(syms, stxs')
return (syms, stxs')
sectionLikeToDocumentSymbols (text : FileMap) (stx : Syntax) (stxs : List Syntax) (name : String) (kind : SymbolKind) (selection : Syntax) :=
let (syms, stxs') := toDocumentSymbols text stxs
-- discard `end`
@ -219,12 +221,12 @@ partial def handleDocumentSymbol (p : DocumentSymbolParams)
| endStx::_ => endStx
| [] => (stx::stxs').getLast!
-- we can assume that commands always have at least one position (see `parseCommand`)
let range := rangeOfSyntax! text (mkNullNode #[stx, endStx])
let range := (mkNullNode #[stx, endStx]).getRange?.get!.toLspRange text
(DocumentSymbol.mk {
name
kind
range
selectionRange := if hasRange selection then rangeOfSyntax! text selection else range
selectionRange := selection.getRange? |>.map (·.toLspRange text) |>.getD range
children? := syms.toArray
} :: syms', stxs'')
end
@ -276,16 +278,16 @@ where
else
stx.getArgs.forM go
highlightId (stx : Syntax) : ReaderT SemanticTokensContext (StateT SemanticTokensState RequestM) _ := do
if let (some pos, some tailPos) := (stx.getPos?, stx.getTailPos?) then
if let some range := stx.getRange? then
for t in (← read).infoState.trees do
for ti in t.deepestNodes (fun
| _, i@(Elab.Info.ofTermInfo ti), _ => match i.pos? with
| some ipos => if pos <= ipos && ipos < tailPos then some ti else none
| some ipos => if range.contains ipos then some ti else none
| _ => none
| _, _, _ => none) do
match ti.expr with
| Expr.fvar .. => addToken ti.stx SemanticTokenType.variable
| _ => if ti.stx.getPos?.get! > pos then addToken ti.stx SemanticTokenType.property
| _ => if ti.stx.getPos?.get! > range.start then addToken ti.stx SemanticTokenType.property
highlightKeyword stx := do
if let Syntax.atom info val := stx then
if val.bsize > 0 && val[0].isAlpha then
@ -347,4 +349,4 @@ builtin_initialize
registerLspRequestHandler "$/lean/plainGoal" PlainGoalParams (Option PlainGoal) handlePlainGoal
registerLspRequestHandler "$/lean/plainTermGoal" PlainTermGoalParams (Option PlainTermGoal) handlePlainTermGoal
end Lean.Server.FileWorker
end Lean.Server.FileWorker

95
src/Lean/Server/InfoUtils.lean
View file

@ -8,6 +8,19 @@ import Lean.DocString
import Lean.Elab.InfoTree
import Lean.Util.Sorry
protected structure String.Range where
start : String.Pos
stop : String.Pos
deriving Inhabited, Repr
def String.Range.contains (r : String.Range) (pos : String.Pos) : Bool :=
r.start <= pos && pos < r.stop
def Lean.Syntax.getRange? (stx : Syntax) (originalOnly := false) : Option String.Range :=
match stx.getPos? originalOnly, stx.getTailPos? originalOnly with
| some start, some stop => some { start, stop }
| _, _ => none
namespace Lean.Elab
/--
@ -61,12 +74,23 @@ def Info.stx : Info → Syntax
| ofFieldInfo i => i.stx
| ofCompletionInfo i => i.stx
def Info.lctx : Info → LocalContext
| Info.ofTermInfo i => i.lctx
| Info.ofFieldInfo i => i.lctx
| _ => LocalContext.empty
def Info.pos? (i : Info) : Option String.Pos :=
i.stx.getPos? (originalOnly := true)
def Info.tailPos? (i : Info) : Option String.Pos :=
i.stx.getTailPos? (originalOnly := true)
def Info.range? (i : Info) : Option String.Range :=
i.stx.getRange? (originalOnly := true)
def Info.contains (i : Info) (pos : String.Pos) : Bool :=
i.range?.any (·.contains pos)
def Info.size? (i : Info) : Option Nat := OptionM.run do
let pos ← i.pos?
let tailPos ← i.tailPos?
@ -95,57 +119,51 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
/-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) :=
t.smallestInfo? fun i =>
if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
if pos ≤ hoverPos ∧ hoverPos < tailPos then
match i with
| Info.ofTermInfo ti =>
!ti.expr.isSyntheticSorry &&
-- TODO: see if we can get rid of this
#[identKind,
strLitKind,
charLitKind,
numLitKind,
scientificLitKind,
nameLitKind,
fieldIdxKind,
interpolatedStrLitKind,
interpolatedStrKind
].contains i.stx.getKind
| Info.ofFieldInfo _ => true
| _ => false
else false
else false
t.smallestInfo? fun i => do
if i matches Info.ofFieldInfo _ || i.toElabInfo?.isSome then
-- show hover on first token (`i.stx` or immediate child of it) only
if i.stx.isIdent || i.stx.isAtom then
return i.contains hoverPos
if let some firstTk := i.stx.getArgs.find? (fun arg => arg.isAtom) then
return firstTk.getRange? (originalOnly := true) |>.any (·.contains hoverPos)
return false
/-- Construct a hover popup, if any, from an info node in a context.-/
def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
let lctx ← match i with
| Info.ofTermInfo i => i.lctx
| Info.ofFieldInfo i => i.lctx
| _ => return none
ci.runMetaM lctx do
ci.runMetaM i.lctx do
let mut fmts := #[]
if let some f ← fmtTerm? then
fmts := fmts.push f
if let some f ← fmtDoc? then
fmts := fmts.push f
if fmts.isEmpty then
none
else
f!"\n***\n".joinSep fmts.toList
where
fmtTerm? := do
match i with
| Info.ofTermInfo ti =>
let tp ← Meta.inferType ti.expr
let eFmt ← Meta.ppExpr ti.expr
let tpFmt ← Meta.ppExpr tp
let hoverFmt := f!"```lean
return some f!"```lean
{eFmt} : {tpFmt}
```"
if let some n := ti.expr.constName? then
if let some doc ← findDocString? n then
return f!"{hoverFmt}\n***\n{doc}"
return hoverFmt
| Info.ofFieldInfo fi =>
let tp ← Meta.inferType fi.val
let tpFmt ← Meta.ppExpr tp
return f!"```lean
return some f!"```lean
{fi.name} : {tpFmt}
```"
| _ => return none
fmtDoc? := do
if let Info.ofTermInfo ti := i then
if let some n := ti.expr.constName? then
return ← findDocString? n
if let some ei := i.toElabInfo? then
return ← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind
return none
structure GoalsAtResult where
ctxInfo : ContextInfo
@ -208,10 +226,9 @@ partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option
else
headFns
t.smallestInfo? fun i => do
if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
if pos ≤ hoverPos ∧ hoverPos < tailPos then
if let Info.ofTermInfo ti := i then
return !ti.stx.isIdent || !headFns.contains pos
if i.contains hoverPos then
if let Info.ofTermInfo ti := i then
return !ti.stx.isIdent || !headFns.contains i.pos?.get!
false
where
/- Returns the position of the head function symbol, if it is an identifier. -/

4
src/Lean/Server/Utils.lean
View file

@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki, Marc Huisinga
-/
import Lean.Data.Position
import Lean.Data.Lsp
import Lean.Server.InfoUtils
import Init.System.FilePath
namespace IO
@ -163,3 +164,6 @@ def takeWhile (p : α → Bool) : List α → List α
| hd :: tl => if p hd then hd :: takeWhile p tl else []
end List
def String.Range.toLspRange (text : Lean.FileMap) (r : String.Range) : Lean.Lsp.Range :=
⟨text.utf8PosToLspPos r.start, text.utf8PosToLspPos r.stop⟩