chore: minor hover code cleanup
This commit is contained in:
Wojciech Nawrocki
Leonardo de Moura
parent
46e9d2533d
commit
d7c201a2d4
2 changed files with 49 additions and 46 deletions
|
|
@ -260,6 +260,9 @@ section RequestHandling
|
|||
-- TODO(WN): the type is too complicated
|
||||
abbrev RequestM α := ServerM $ Task $ Except IO.Error $ Except RequestError α
|
||||
|
||||
def mapTask (t : Task α) (f : α → ExceptT RequestError ServerM β) : RequestM β := fun st =>
|
||||
(IO.mapTask · t) fun a => f a st
|
||||
|
||||
/- Requests that need data from a certain command should traverse the snapshots
|
||||
by successively getting the next task, meaning that we might need to wait for elaboration.
|
||||
When that happens, the request should send a "content changed" error to the user
|
||||
|
|
@ -279,69 +282,56 @@ section RequestHandling
|
|||
value := s }
|
||||
range? := some { start := text.utf8PosToLspPos f
|
||||
«end» := text.utf8PosToLspPos t } }
|
||||
(IO.mapTask · findTask) fun
|
||||
mapTask findTask fun
|
||||
| Except.error ElabTaskError.aborted =>
|
||||
pure $ Except.error RequestError.fileChanged
|
||||
throwThe RequestError RequestError.fileChanged
|
||||
| Except.error (ElabTaskError.ioError e) =>
|
||||
throwThe IO.Error e
|
||||
| Except.error ElabTaskError.eof =>
|
||||
pure $ Except.ok none
|
||||
return none
|
||||
| Except.ok (some snap) => do
|
||||
for t in snap.toCmdState.infoState.trees do
|
||||
let ts := t.smallestNodes fun
|
||||
| Info.ofTermInfo i =>
|
||||
match i.pos?, i.endPos? with
|
||||
| some pos, some endPos =>
|
||||
/- TODO(WN): We search for the syntax in the original command because some macro expansions
|
||||
introduce phantom terms which actually contain position info but do not correspond
|
||||
to anything in the source. Example: `ForInStep.yield { .. }` in `for .. in .. do` -/
|
||||
if pos ≤ hoverPos ∧ hoverPos ≤ endPos ∧ (snap.stx.find? fun s => s == i.stx).isSome then
|
||||
if let Syntax.node `Lean.Parser.Term.app args := i.stx then
|
||||
let hd := args.get! 0
|
||||
match hd.getPos, hd.getTailPos with
|
||||
| some pos, some endPos => pos ≤ hoverPos ∧ hoverPos ≤ endPos
|
||||
| _, _ => false
|
||||
else
|
||||
/- TODO(WN): Currently only these kinds are displayed. This misses a lot of cases that we
|
||||
want to display but which will need to be tweaked to display correctly. -/
|
||||
#[`ident,
|
||||
`Lean.Parser.Term.proj
|
||||
].contains i.stx.getKind
|
||||
match i.pos?, i.tailPos? with
|
||||
| some pos, some tailPos =>
|
||||
/- TODO(WN): when we have a way to do so,
|
||||
check for synthetic syntax and allow arbitrary syntax kinds. -/
|
||||
if pos ≤ hoverPos ∧ hoverPos < tailPos then
|
||||
#[identKind,
|
||||
strLitKind,
|
||||
charLitKind,
|
||||
numLitKind,
|
||||
scientificLitKind,
|
||||
nameLitKind,
|
||||
fieldIdxKind,
|
||||
interpolatedStrLitKind,
|
||||
interpolatedStrKind
|
||||
].contains i.stx.getKind
|
||||
else false
|
||||
| _, _ => false
|
||||
| _ => false
|
||||
let mut nds : Array (Nat × ContextInfo × TermInfo) := #[]
|
||||
for t in ts do
|
||||
if let InfoTree.context ci (InfoTree.node (Info.ofTermInfo i) _) := t then
|
||||
let diff := i.endPos?.get! - i.pos?.get!
|
||||
let diff := i.tailPos?.get! - i.pos?.get!
|
||||
nds := nds.push (diff, ci, i)
|
||||
|
||||
if let some (_, ci, i) := nds.getMax? (fun a b => a.1 > b.1) then
|
||||
let (stx, expr, pos, endPos) : (Syntax × Expr × String.Pos × String.Pos) :=
|
||||
(if let Syntax.node `Lean.Parser.Term.app args := i.stx then
|
||||
let hd := args.get! 0
|
||||
let (pos, endPos) := (hd.getPos.get!, hd.getTailPos.get!)
|
||||
(hd, i.expr.getAppFn, pos, endPos)
|
||||
else
|
||||
(i.stx, i.expr, i.pos?.get!, i.endPos?.get!))
|
||||
|
||||
let tFmt ← ci.runMetaM i.lctx do
|
||||
return f!"{← Meta.ppExpr (← Meta.inferType expr)}"
|
||||
--return f!"{stx.getKind} --> {← Meta.ppExpr expr} <{pos}->{endPos}> : {← Meta.ppExpr (← Meta.inferType expr)}"
|
||||
let mut hoverStr := s!"```lean
|
||||
return f!"{← Meta.ppExpr i.expr} : {← Meta.ppExpr (← Meta.inferType i.expr)}"
|
||||
let mut hoverFmt := f!"```lean
|
||||
{tFmt}
|
||||
```"
|
||||
if let Expr.const n .. := expr then
|
||||
if let Expr.const n .. := i.expr then
|
||||
if let some doc ← ci.runMetaM i.lctx <| findDocString? n then
|
||||
hoverStr := s!"{hoverStr}\n***\n{doc}"
|
||||
hoverFmt := f!"{hoverFmt}\n***\n{doc}"
|
||||
|
||||
return (Except.ok $ some $ mkHover hoverStr pos endPos
|
||||
-- Type inference fails
|
||||
: Except RequestError _)
|
||||
return some <| mkHover (toString hoverFmt) i.pos?.get! i.tailPos?.get!
|
||||
pure ()
|
||||
|
||||
return Except.ok none
|
||||
| Except.ok none => return Except.ok none
|
||||
return none
|
||||
| Except.ok none => return none
|
||||
|
||||
def handleWaitForDiagnostics (id : RequestID) (p : WaitForDiagnosticsParam)
|
||||
: ServerM (Task (Except IO.Error (Except RequestError WaitForDiagnostics))) := do
|
||||
|
|
@ -512,3 +502,4 @@ def workerMain : IO UInt32 := do
|
|||
return 1
|
||||
|
||||
end Lean.Server.FileWorker
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,27 @@
|
|||
/-
|
||||
Copyright (c) 2021 Wojciech Nawrocki. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Authors: Wojciech Nawrocki
|
||||
-/
|
||||
import Lean.Elab
|
||||
|
||||
namespace Lean.Elab
|
||||
|
||||
/-- Finds the smallest node matching `p` in the first subtree which contains a matching node.
|
||||
Wraps the result in all outer `ContextInfo`s. -/
|
||||
/-- Find the deepest node matching `p` in the first subtree which contains a matching node.
|
||||
The result is wrapped in all outer `ContextInfo`s. -/
|
||||
partial def InfoTree.smallestNode? (p : Info → Bool) : InfoTree → Option InfoTree
|
||||
| context i t => context i <$> t.smallestNode? p
|
||||
| n@(node i cs) =>
|
||||
let cs := cs.map (fun c => c.smallestNode? p)
|
||||
let cs := cs.filter (fun c? => c?.isSome)
|
||||
let cs := cs.map (·.smallestNode? p)
|
||||
let cs := cs.filter (·.isSome)
|
||||
if !cs.isEmpty then cs.get! 0
|
||||
else if p i then some n
|
||||
else none
|
||||
| _ => none
|
||||
|
||||
/-- Finds the smallest node matching `p` in the first subtree which contains a matching node.
|
||||
Wraps the result in all outer `ContextInfo`s. -/
|
||||
/-- For every branch, find the deepest node in that branch matching `p`
|
||||
and return all of them. Each result is wrapper in all outer `ContextInfo`s. -/
|
||||
partial def InfoTree.smallestNodes (p : Info → Bool) : InfoTree → List InfoTree
|
||||
| context i t => t.smallestNodes p |>.map (context i)
|
||||
| n@(node i cs) =>
|
||||
|
|
@ -30,7 +36,13 @@ partial def InfoTree.smallestNodes (p : Info → Bool) : InfoTree → List InfoT
|
|||
def TermInfo.pos? (i : TermInfo) : Option String.Pos :=
|
||||
i.stx.getPos
|
||||
|
||||
def TermInfo.endPos? (i : TermInfo) : Option String.Pos :=
|
||||
def TermInfo.tailPos? (i : TermInfo) : Option String.Pos :=
|
||||
i.stx.getTailPos
|
||||
|
||||
def TacticInfo.pos? (i : TacticInfo) : Option String.Pos :=
|
||||
i.stx.getPos
|
||||
|
||||
def TacticInfo.tailPos? (i : TacticInfo) : Option String.Pos :=
|
||||
i.stx.getTailPos
|
||||
|
||||
end Lean.Elab
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue