feat: more widget Info integration
This commit is contained in:
Wojciech Nawrocki
Leonardo de Moura
parent
fdc11104eb
commit
8207ca6493
2 changed files with 85 additions and 45 deletions
|
|
@ -127,51 +127,57 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : O
|
|||
return i.contains hoverPos
|
||||
return false
|
||||
|
||||
def Info.type? (i : Info) : MetaM (Option Expr) :=
|
||||
match i with
|
||||
| Info.ofTermInfo ti => Meta.inferType ti.expr
|
||||
| Info.ofFieldInfo fi => Meta.inferType fi.val
|
||||
| _ => return none
|
||||
|
||||
def Info.docString? (i : Info) : MetaM (Option String) := do
|
||||
if let Info.ofTermInfo ti := i then
|
||||
if let some n := ti.expr.constName? then
|
||||
return ← findDocString? n
|
||||
if let Info.ofFieldInfo fi := i then
|
||||
return ← findDocString? fi.projName
|
||||
if let some ei := i.toElabInfo? then
|
||||
return ← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind
|
||||
return none
|
||||
|
||||
/-- Construct a hover popup, if any, from an info node in a context.-/
|
||||
def Info.hoverMsg? (ci : ContextInfo) (i : Info) : IO (Option MessageData) := do
|
||||
def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
|
||||
ci.runMetaM i.lctx do
|
||||
let mut msgs := #[]
|
||||
let mut fmts := #[]
|
||||
try
|
||||
if let some m ← termMsg? then
|
||||
msgs := msgs.push m
|
||||
if let some f ← fmtTerm? then
|
||||
fmts := fmts.push f
|
||||
catch _ => pure ()
|
||||
if let some m ← docMsg? then
|
||||
msgs := msgs.push m
|
||||
if msgs.isEmpty then
|
||||
if let some m ← i.docString? then
|
||||
fmts := fmts.push m
|
||||
if fmts.isEmpty then
|
||||
none
|
||||
else
|
||||
MessageData.withContext { env := ci.env, mctx := ci.mctx, lctx := i.lctx, opts := ci.options }
|
||||
<| MessageData.withNamingContext { currNamespace := ci.currNamespace, openDecls := ci.openDecls }
|
||||
<| m!"\n***\n".joinSep msgs.toList
|
||||
f!"\n***\n".joinSep fmts.toList
|
||||
|
||||
where
|
||||
termMsg? : MetaM (Option MessageData) := do
|
||||
fmtTerm? : MetaM (Option Format) := do
|
||||
match i with
|
||||
| Info.ofTermInfo ti =>
|
||||
let tp ← Meta.inferType ti.expr
|
||||
-- try not to show too scary internals
|
||||
-- TODO(WN): this check is now quite costly; should we do it in `MessageData.format`?
|
||||
let eFmt ← Meta.ppExpr ti.expr
|
||||
let msg := if isAtomicFormat eFmt then m!"{ti.expr} : {tp}" else m!"{tp}"
|
||||
return m!"```lean
|
||||
{msg}
|
||||
let tpFmt ← Meta.ppExpr tp
|
||||
-- try not to show too scary internals
|
||||
let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}"
|
||||
return some f!"```lean
|
||||
{fmt}
|
||||
```"
|
||||
| Info.ofFieldInfo fi =>
|
||||
let tp ← Meta.inferType fi.val
|
||||
return m!"```lean
|
||||
{fi.fieldName} : {tp}
|
||||
let tpFmt ← Meta.ppExpr tp
|
||||
return some f!"```lean
|
||||
{fi.fieldName} : {tpFmt}
|
||||
```"
|
||||
| _ => return none
|
||||
|
||||
docMsg? : MetaM (Option MessageData) := do
|
||||
if let Info.ofTermInfo ti := i then
|
||||
if let some n := ti.expr.constName? then
|
||||
return (← findDocString? n).map toMessageData
|
||||
if let Info.ofFieldInfo fi := i then
|
||||
return (← findDocString? fi.projName).map toMessageData
|
||||
if let some ei := i.toElabInfo? then
|
||||
return (← findDocString? ei.elaborator <||> findDocString? ei.stx.getKind).map toMessageData
|
||||
return none
|
||||
|
||||
isAtomicFormat : Format → Bool
|
||||
| Std.Format.text _ => true
|
||||
| Std.Format.group f _ => isAtomicFormat f
|
||||
|
|
@ -179,11 +185,6 @@ where
|
|||
| Std.Format.tag _ f => isAtomicFormat f
|
||||
| _ => false
|
||||
|
||||
def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do
|
||||
match ← i.hoverMsg? ci with
|
||||
| none => return none
|
||||
| some m => m.format
|
||||
|
||||
structure GoalsAtResult where
|
||||
ctxInfo : ContextInfo
|
||||
tacticInfo : TacticInfo
|
||||
|
|
|
|||
|
|
@ -63,7 +63,8 @@ where
|
|||
fileMap := arbitrary
|
||||
options := ctx.opts
|
||||
currNamespace := nCtx.currNamespace
|
||||
openDecls := nCtx.openDecls }
|
||||
openDecls := nCtx.openDecls
|
||||
}
|
||||
let (fmt, infos) ← ci.runMetaM ctx.lctx (ExprWithCtx.formatInfos e)
|
||||
let t ← pushEmbed <| EmbedFmt.expr ci ctx.lctx infos
|
||||
return Format.tag t fmt
|
||||
|
|
@ -71,38 +72,75 @@ where
|
|||
| nCtx, some ctx, ofGoal mvarId => withIgnoreTags <| ppGoal (mkPPContext nCtx ctx) mvarId
|
||||
| nCtx, _, withContext ctx d => go nCtx ctx d
|
||||
| _, ctx, withNamingContext nCtx d => go nCtx ctx d
|
||||
| nCtx, ctx, tagged n d => do
|
||||
| nCtx, ctx, tagged t d => do
|
||||
-- tagged is *almost* perfect for detecting traces
|
||||
-- expect for the following two other occurrences:
|
||||
-- src/Lean/Elab/Term.lean:454
|
||||
-- src/Lean/Elab/Tactic/Basic.lean:33
|
||||
let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx n d
|
||||
Format.tag f <$> go nCtx ctx d
|
||||
if let Name.str cls "_traceCtx" _ := t then
|
||||
let f ← pushEmbed <| EmbedFmt.lazyTrace nCtx ctx cls d
|
||||
Format.tag f s!"[{cls}] (trace hidden)"
|
||||
else
|
||||
go nCtx ctx d
|
||||
| nCtx, ctx, nest n d => Format.nest n <$> go nCtx ctx d
|
||||
| nCtx, ctx, compose d₁ d₂ => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
|
||||
| nCtx, ctx, group d => Format.group <$> go nCtx ctx d
|
||||
| nCtx, ctx, node ds => Format.nest 2 <$> ds.foldlM (fun r d => do let d ← go nCtx ctx d; pure $ r ++ Format.line ++ d) Format.nil
|
||||
|
||||
private partial def msgToInteractive (msgData : MessageData) : IO (TaggedText MsgEmbed) := do
|
||||
partial def msgToInteractive (msgData : MessageData) (indent : Nat := 0) : IO (TaggedText MsgEmbed) := do
|
||||
let (fmt, embeds) ← msgToInteractiveAux msgData
|
||||
let tt := TaggedText.prettyTagged fmt
|
||||
let tt := TaggedText.prettyTagged fmt indent
|
||||
/- Here we rewrite a `TaggedText Nat` corresponding to a whole `MessageData` into one where
|
||||
the tags are `TaggedText MsgEmbed`s corresponding to embedded objects with their subtree
|
||||
empty (`text ""`). In other words, we terminate the `MsgEmbed`-tagged -tree at embedded objects
|
||||
and store the pretty-printed embed (which can itself be a `TaggedText`) in the tag. -/
|
||||
tt.rewriteM fun n subTt =>
|
||||
tt.rewriteM fun (n, col) subTt =>
|
||||
match embeds.get! n with
|
||||
| EmbedFmt.expr ctx lctx infos =>
|
||||
let subTt' := ExprWithCtx.tagExprInfos ctx lctx infos subTt
|
||||
TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text "")
|
||||
TaggedText.tag (MsgEmbed.expr subTt') (TaggedText.text subTt.stripTags)
|
||||
| EmbedFmt.goal ctx lctx g =>
|
||||
-- TODO(WN): use InteractiveGoal types here
|
||||
unreachable!
|
||||
| EmbedFmt.lazyTrace nCtx ctx? n m =>
|
||||
-- TODO(WN): TraceExplorer component
|
||||
TaggedText.tag (MsgEmbed.lazyTrace ⟨"1337"⟩) (TaggedText.text "")
|
||||
| EmbedFmt.lazyTrace nCtx ctx? cls m =>
|
||||
let msg :=
|
||||
match ctx? with
|
||||
| some ctx => MessageData.withNamingContext nCtx <| MessageData.withContext ctx m
|
||||
| none => MessageData.withNamingContext nCtx m
|
||||
TaggedText.tag (MsgEmbed.lazyTrace col cls ⟨msg⟩) (TaggedText.text subTt.stripTags)
|
||||
| EmbedFmt.ignoreTags => TaggedText.text subTt.stripTags
|
||||
|
||||
structure MsgToInteractive where
|
||||
msg : WithRpcRef MessageData
|
||||
indent : Nat
|
||||
deriving Inhabited, RpcEncoding
|
||||
|
||||
builtin_initialize
|
||||
registerRpcCallHandler `Lean.Widget.InteractiveDiagnostics.msgToInteractive MsgToInteractive (TaggedText MsgEmbed) fun ⟨⟨m⟩, i⟩ => RequestM.asTask do msgToInteractive m i
|
||||
|
||||
structure InfoPopup where
|
||||
type : Option CodeWithInfos
|
||||
exprExplicit : Option CodeWithInfos
|
||||
doc : Option String
|
||||
deriving Inhabited, RpcEncoding
|
||||
|
||||
builtin_initialize
|
||||
registerRpcCallHandler `Lean.Widget.InteractiveDiagnostics.infoToInteractive (WithRpcRef InfoWithCtx) InfoPopup
|
||||
fun ⟨i⟩ => RequestM.asTask do
|
||||
i.ctx.runMetaM i.lctx do
|
||||
let type? ← match (← i.info.type?) with
|
||||
| some type => some <$> ExprWithCtx.tagged type
|
||||
| none => none
|
||||
let exprExplicit? ← match i.info with
|
||||
| Elab.Info.ofTermInfo ti => some <$> ExprWithCtx.taggedExplicit ti.expr
|
||||
| Elab.Info.ofFieldInfo fi => some (TaggedText.text fi.fieldName.toString)
|
||||
| _ => none
|
||||
return {
|
||||
type := type?
|
||||
exprExplicit := exprExplicit?
|
||||
doc := ← i.info.docString? : InfoPopup
|
||||
}
|
||||
|
||||
/-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
|
||||
def msgToDiagnostic (text : FileMap) (m : Message) : ReaderT RpcSession IO Diagnostic := do
|
||||
let low : Lsp.Position := text.leanPosToLspPos m.pos
|
||||
|
|
@ -140,7 +178,8 @@ def publishMessages (m : DocumentMeta) (msgLog : MessageLog) (hOut : IO.FS.Strea
|
|||
let diagParams : PublishDiagnosticsParams :=
|
||||
{ uri := m.uri
|
||||
version? := some m.version
|
||||
diagnostics := diagnostics.toArray }
|
||||
diagnostics := diagnostics.toArray
|
||||
}
|
||||
hOut.writeLspNotification {
|
||||
method := "textDocument/publishDiagnostics"
|
||||
param := toJson diagParams
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue