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

feat: use interactive goals in messages

Browse source
This commit is contained in:
Gabriel Ebner 2022-08-09 13:07:56 +02:00 • committed by Leonardo de Moura
parent 34b0b4b7e2
commit e4a7b82c8d
1 changed files with 27 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
src/Lean/Widget/InteractiveDiagnostic.lean
View file

@ -82,6 +82,17 @@ where
let t ← pushEmbed EmbedFmt.ignoreTags
return Format.tag t fmt
mkContextInfo (nCtx : NamingContext) (ctx : MessageDataContext) : Elab.ContextInfo := {
env := ctx.env
mctx := ctx.mctx
fileMap := default
options := ctx.opts
currNamespace := nCtx.currNamespace
openDecls := nCtx.openDecls
-- Hack: to make sure unique ids created at `ppExprWithInfos` do not collide with ones in `ctx.mctx`
ngen := { namePrefix := `_diag }
}
go : NamingContext → Option MessageDataContext → MessageData → MsgFmtM Format
| _, _, ofFormat fmt => withIgnoreTags (pure fmt)
| _, _, ofLevel u => return format u
@ -90,21 +101,13 @@ where
| _, none, ofSyntax s => withIgnoreTags (pure s.formatStx)
| _, none, ofExpr e => return format (toString e)
| nCtx, some ctx, ofExpr e => do
let ci : Elab.ContextInfo := {
env := ctx.env
mctx := ctx.mctx
fileMap := default
options := ctx.opts
currNamespace := nCtx.currNamespace
openDecls := nCtx.openDecls
-- Hack: to make sure unique ids created at `ppExprWithInfos` do not collide with ones in `ctx.mctx`
ngen := { namePrefix := `_diag }
}
let ci := mkContextInfo nCtx ctx
let (fmt, infos) ← ci.runMetaM ctx.lctx <| PrettyPrinter.ppExprWithInfos e
let t ← pushEmbed <| EmbedFmt.expr ci infos
return Format.tag t fmt
| _, none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId)
| nCtx, some ctx, ofGoal mvarId => withIgnoreTags <| ppGoal (mkPPContext nCtx ctx) mvarId
| nCtx, some ctx, ofGoal mvarId =>
return .tag (← pushEmbed (.goal (mkContextInfo nCtx ctx) ctx.lctx mvarId)) "\n"
| nCtx, _, withContext ctx d => go nCtx ctx d
| _, ctx, withNamingContext nCtx d => go nCtx ctx d
| nCtx, ctx, tagged _ d => go nCtx ctx d
@ -134,23 +137,23 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
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. -/
let rec fmtToTT (fmt : Format) (indent : Nat) : TaggedText MsgEmbed :=
(TaggedText.prettyTagged fmt indent).rewrite fun (n, col) tt =>
let rec fmtToTT (fmt : Format) (indent : Nat) : IO (TaggedText MsgEmbed) :=
(TaggedText.prettyTagged fmt indent).rewriteM fun (n, col) tt =>
match embeds[n]! with
| .expr ctx infos =>
.tag (.expr (tagExprInfos ctx infos tt)) default
| .goal _ _ _ =>
-- TODO(WN): use InteractiveGoal types here
unreachable!
| .trace cls msg collapsed children =>
return .tag (.expr (tagExprInfos ctx infos tt)) default
| .goal ctx lctx g =>
ctx.runMetaM lctx do
return .tag (.goal (← goalToInteractive g)) default
| .trace cls msg collapsed children => do
let col := col + tt.stripTags.length - 2
let children :=
let children ←
match children with
| .lazy children => .lazy ⟨{indent := col+2, children := children.map .mk}⟩
| .strict children => .strict (children.map (fmtToTT · (col+2)))
.tag (.trace indent cls (fmtToTT msg col) collapsed children) default
| .ignoreTags => .text tt.stripTags
return fmtToTT fmt indent
| .lazy children => pure <| .lazy ⟨{indent := col+2, children := children.map .mk}⟩
| .strict children => pure <| .strict (← children.mapM (fmtToTT · (col+2)))
return .tag (.trace indent cls (← fmtToTT msg col) collapsed children) default
| .ignoreTags => return .text tt.stripTags
fmtToTT fmt indent
/-- Transform a Lean Message concerning the given text into an LSP Diagnostic. -/
def msgToInteractiveDiagnostic (text : FileMap) (m : Message) (hasWidgets : Bool) : IO InteractiveDiagnostic := do