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

fix: no non-expr embeds in diagnostics

Browse source
This commit is contained in:
Wojciech Nawrocki 2021-08-03 20:21:44 -04:00 • committed by Leonardo de Moura
parent 73363bef1f
commit 73f219ddba
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Widget/InteractiveDiagnostics.lean
View file

@ -75,11 +75,12 @@ private def msgToInteractive (msgData : MessageData) : IO (TaggedText MsgEmbed)
and store the pretty-printed embed (which is itself a `TaggedText (WithRpcRef LazyExprWithCtx)`,
for example) in the tag. -/
tt.rewriteM fun n subTt =>
match embeds.get! n with
| EmbedFmt.ofExpr e =>
match embeds.get? n with
| some (EmbedFmt.ofExpr e) =>
TaggedText.tag
{ ef := subTt.map fun n => ⟨fun () => e.runMetaM (e.traverse n)⟩ }
(TaggedText.text "")
| none => TaggedText.text subTt.stripTags
private partial def stripEmbeds (tt : TaggedText MsgEmbed) : String :=
let tt : TaggedText MsgEmbed := tt.rewrite fun ⟨et⟩ _ => TaggedText.text et.stripTags