From 73f219ddba597323391a5a9142da5e397b202062 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 3 Aug 2021 20:21:44 -0400 Subject: [PATCH] fix: no non-expr embeds in diagnostics --- src/Lean/Widget/InteractiveDiagnostics.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Widget/InteractiveDiagnostics.lean b/src/Lean/Widget/InteractiveDiagnostics.lean index 166faf60f2..f5a4d7fd1d 100644 --- a/src/Lean/Widget/InteractiveDiagnostics.lean +++ b/src/Lean/Widget/InteractiveDiagnostics.lean @@ -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