From d594563693d948c97daf94dff747af4b447bc514 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 1 Aug 2025 06:41:18 +0200 Subject: [PATCH] feat: configurable trace expansion Lean output that contains traces can now expand certain trace classes by default. --- examples/anchor-examples/lake-manifest.json | 2 +- .../documented-package/lake-manifest.json | 2 +- examples/website-examples/lake-manifest.json | 2 +- examples/website-literate/lake-manifest.json | 2 +- lake-manifest.json | 2 +- src/verso-blog/VersoBlog.lean | 18 +++++----- src/verso-blog/VersoBlog/Basic.lean | 4 +-- src/verso-blog/VersoBlog/Template.lean | 8 ++--- .../VersoManual/ExternalLean.lean | 22 ++++++------ src/verso-manual/VersoManual/Glossary.lean | 1 + src/verso-manual/VersoManual/InlineLean.lean | 35 +++++++++++-------- src/verso/Verso/Code/External.lean | 25 ++++++++----- src/verso/Verso/Code/Highlighted.lean | 21 +++++------ 13 files changed, 79 insertions(+), 65 deletions(-) diff --git a/examples/anchor-examples/lake-manifest.json b/examples/anchor-examples/lake-manifest.json index 4135355f7..e99aa5ca2 100644 --- a/examples/anchor-examples/lake-manifest.json +++ b/examples/anchor-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7", + "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/documented-package/lake-manifest.json b/examples/documented-package/lake-manifest.json index 85fda858f..a9044b784 100644 --- a/examples/documented-package/lake-manifest.json +++ b/examples/documented-package/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7", + "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/website-examples/lake-manifest.json b/examples/website-examples/lake-manifest.json index 4135355f7..e99aa5ca2 100644 --- a/examples/website-examples/lake-manifest.json +++ b/examples/website-examples/lake-manifest.json @@ -6,7 +6,7 @@ "url": "https://github.com/leanprover/subverso", "type": "git", "subDir": null, - "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7", + "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/examples/website-literate/lake-manifest.json b/examples/website-literate/lake-manifest.json index 453a0e282..203f90062 100644 --- a/examples/website-literate/lake-manifest.json +++ b/examples/website-literate/lake-manifest.json @@ -7,7 +7,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7", + "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lake-manifest.json b/lake-manifest.json index 141519c42..e8729e886 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "bdc74c95376f9a5c23dba1b3159b03c5c1c8aad7", + "rev": "9909b0d7a1f32cd92bb9a6662599f1e08d087c74", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean index 9df4701cf..94b518b51 100644 --- a/src/verso-blog/VersoBlog.lean +++ b/src/verso-blog/VersoBlog.lean @@ -690,15 +690,15 @@ where } open SubVerso.Highlighting in -private def leanOutputBlock [bg : BlogGenre genre] (message : Highlighted.Message) (summarize := false) : Block genre := - Block.other (bg.block_eq ▸ BlockExt.message summarize message) #[Block.code message.toString] +private def leanOutputBlock [bg : BlogGenre genre] (message : Highlighted.Message) (summarize := false) (expandTraces : List Name := []) : Block genre := + Block.other (bg.block_eq ▸ BlockExt.message summarize message expandTraces) #[Block.code message.toString] open SubVerso.Highlighting in -private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Message) (plain : Bool) : Inline genre := +private def leanOutputInline [bg : BlogGenre genre] (message : Highlighted.Message) (plain : Bool) (expandTraces : List Name := []) : Inline genre := if plain then Inline.code message.toString else - Inline.other (bg.inline_eq ▸ InlineExt.message message) #[Inline.code message.toString] + Inline.other (bg.inline_eq ▸ InlineExt.message message expandTraces) #[Inline.code message.toString] @[code_block_expander leanOutput] def leanOutput : Doc.Elab.CodeBlockExpander @@ -728,7 +728,7 @@ def leanOutput : Doc.Elab.CodeBlockExpander withOptions (·.set `pp.tagAppFns true) do SubVerso.Highlighting.highlightMessage m finally setEnv myEnv - ``(Block.other (Blog.BlockExt.message false $(quote m')) #[Block.code $(quote str.getString)]) + ``(Block.other (Blog.BlockExt.message false $(quote m') ([] : List Lean.Name)) #[Block.code $(quote str.getString)]) return #[content] pure messages | .inr msgs => @@ -855,7 +855,7 @@ instance [bg : BlogGenre genre] : ExternalCode genre where Inline.other (bg.inline_eq ▸ InlineExt.highlightedCode { cfg with contextName := `verso } hl) #[] leanBlock hl cfg := Block.other (bg.block_eq ▸ BlockExt.highlightedCode { cfg with contextName := `verso } hl) #[] - leanOutputInline message plain := - leanOutputInline message plain - leanOutputBlock message (summarize := false) := - leanOutputBlock message (summarize := summarize) + leanOutputInline message plain (expandTraces := []) := + leanOutputInline message plain (expandTraces := expandTraces) + leanOutputBlock message (summarize := false) (expandTraces : List Name := []) := + leanOutputBlock message (summarize := summarize) (expandTraces := expandTraces) diff --git a/src/verso-blog/VersoBlog/Basic.lean b/src/verso-blog/VersoBlog/Basic.lean index afa1c1a8e..2f57e3720 100644 --- a/src/verso-blog/VersoBlog/Basic.lean +++ b/src/verso-blog/VersoBlog/Basic.lean @@ -36,7 +36,7 @@ deriving Repr inductive BlockExt where | highlightedCode (opts : CodeOpts) (highlighted : Highlighted) - | message (summarize : Bool) (msg : Highlighted.Message) + | message (summarize : Bool) (msg : Highlighted.Message) (expandTraces : List Lean.Name) | lexedText (content : LexedText) | htmlDiv (classes : String) | htmlWrapper (tag : String) (attributes : Array (String × String)) @@ -46,7 +46,7 @@ inductive BlockExt where inductive InlineExt where | highlightedCode (opts : CodeOpts) (highlighted : Highlighted) - | message (msg : Highlighted.Message) + | message (msg : Highlighted.Message) (expandTraces : List Lean.Name) | lexedText (content : LexedText) | customHighlight (highlighted : Highlighted) | label (name : Lean.Name) diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean index 52ab98657..d14dbcc08 100644 --- a/src/verso-blog/VersoBlog/Template.lean +++ b/src/verso-blog/VersoBlog/Template.lean @@ -149,8 +149,8 @@ def blockHtml (g : Genre) | .highlightedCode { contextName, showProofStates } hls, _contents => withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <| hls.blockHtml (toString contextName) (g := g) - | .message summarize msg, _contents => do - return {{
{{← msg.toHtml (g := g)}}
}} + | .message summarize msg expandTraces, _contents => do + return {{
{{← msg.toHtml (expandTraces := expandTraces) (g := g)}}
}} | .htmlDetails classes summary, contents => do pure {{
{{summary}} {{← contents.mapM goB}}
}} | .htmlWrapper name attrs, contents => do @@ -180,8 +180,8 @@ def inlineHtml (g : Genre) [bg : BlogGenre g] | .highlightedCode { contextName, showProofStates } hls, _contents => withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <| hls.inlineHtml (some <| toString contextName) (g := g) - | .message msg, _contents => do - return {{{{← msg.toHtml (g := g)}}}} + | .message msg expandTraces, _contents => do + return {{{{← msg.toHtml expandTraces (g := g)}}}} | .lexedText content, _contents => do pure {{ {{ content.toHtml }} }} | .customHighlight hls, _contents => do diff --git a/src/verso-manual/VersoManual/ExternalLean.lean b/src/verso-manual/VersoManual/ExternalLean.lean index d274fb9f7..c037e11b1 100644 --- a/src/verso-manual/VersoManual/ExternalLean.lean +++ b/src/verso-manual/VersoManual/ExternalLean.lean @@ -123,8 +123,8 @@ inline_extension Inline.lean (hls : Highlighted) (cfg : CodeConfig) where codeOptions.inlineProofStates := cfg.showProofStates, codeOptions.definitionsAsTargets := cfg.defSite.getD false }) <| hl.inlineHtml (g := Manual) "examples" -block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bool := false) where - data := ToJson.toJson (message, summarize) +block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bool := false) (expandTraces : List Name := []) where + data := ToJson.toJson (message, summarize, expandTraces) traverse _ _ _ := do pure none toTeX := @@ -142,12 +142,12 @@ block_extension Block.leanOutput (message : Highlighted.Message) (summarize : Bo | .error err => HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err pure .empty - | .ok ((msg, summarize) : Highlighted.Message × Bool) => - msg.blockHtml summarize (g := Manual) + | .ok ((msg, summarize, expandTraces) : Highlighted.Message × Bool × List Name) => + msg.blockHtml summarize expandTraces (g := Manual) -inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool) where - data := ToJson.toJson (message, plain) +inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool) (expandTraces : List Name) where + data := ToJson.toJson (message, plain, expandTraces) traverse _ _ _ := do pure none toTeX := @@ -165,16 +165,16 @@ inline_extension Inline.leanOutput (message : Highlighted.Message) (plain : Bool | .error err => HtmlT.logError <| "Couldn't deserialize Lean code while rendering HTML: " ++ err pure .empty - | .ok ((txt, plain) : Highlighted.Message × Bool) => + | .ok ((txt, plain, expandTraces) : Highlighted.Message × Bool × List Name) => let plainHtml := {{{{txt.toString}}}} if plain then pure plainHtml - else txt.toHtml (g := Manual) + else txt.toHtml expandTraces (g := Manual) open Verso.Code.External instance : ExternalCode Manual where leanInline hl cfg := Inline.other (Inline.lean hl cfg) #[] leanBlock hl cfg := Block.other (Block.lean hl cfg) #[] - leanOutputInline message plain := Inline.other (Inline.leanOutput message plain) #[] - leanOutputBlock message (summarize : Bool := false) := - Block.other (Block.leanOutput message (summarize := summarize)) #[] + leanOutputInline message plain (expandTraces : List Name := []) := Inline.other (Inline.leanOutput message plain (expandTraces := expandTraces)) #[] + leanOutputBlock message (summarize : Bool := false) (expandTraces : List Name := []) := + Block.other (Block.leanOutput message (summarize := summarize) (expandTraces := expandTraces)) #[] diff --git a/src/verso-manual/VersoManual/Glossary.lean b/src/verso-manual/VersoManual/Glossary.lean index 7a28d0151..6651c6593 100644 --- a/src/verso-manual/VersoManual/Glossary.lean +++ b/src/verso-manual/VersoManual/Glossary.lean @@ -44,6 +44,7 @@ private partial def normString (term : String) : String := Id.run do let mut str := term.toLower if str.endsWith "ies" then str := str.dropRight 3 ++ "y" if str.endsWith "s" then str := str.dropRight 1 + str := str.replace "‑" "-" String.intercalate " " (str.split (fun c => c.isWhitespace || c == '-') |>.filter (!·.isEmpty)) diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean index 8e5e2249f..80d0a5a0c 100644 --- a/src/verso-manual/VersoManual/InlineLean.lean +++ b/src/verso-manual/VersoManual/InlineLean.lean @@ -597,8 +597,8 @@ block_extension Block.leanOutput where | .error err => HtmlT.logError <| "Couldn't deserialize Lean output while rendering HTML: " ++ err ++ "\n" ++ toString data pure .empty - | .ok ((msg, summarize) : Highlighted.Message × Bool) => - msg.blockHtml summarize (g := Manual) + | .ok ((msg, summarize, expandTraces) : Highlighted.Message × Bool × List Name) => + msg.blockHtml summarize (expandTraces := expandTraces) (g := Manual) structure LeanOutputConfig where @@ -609,11 +609,15 @@ structure LeanOutputConfig where whitespace : WhitespaceMode normalizeMetas : Bool allowDiff : Nat + expandTraces : List Name := [] section variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] -def LeanOutputConfig.parser : ArgParse m LeanOutputConfig := +partial def many (p : ArgParse m α) : ArgParse m (List α) := + ((· :: ·) <$> p <*> many p) <|> pure [] + +def LeanOutputConfig.parser : ArgParse m LeanOutputConfig := LeanOutputConfig.mk <$> .positional `name output <*> ((·.getD true) <$> .named `show .bool true) <*> @@ -621,7 +625,8 @@ def LeanOutputConfig.parser : ArgParse m LeanOutputConfig := ((·.getD false) <$> .named `summarize .bool true) <*> ((·.getD .exact) <$> .named `whitespace .whitespaceMode true) <*> .namedD `normalizeMetas .bool true <*> - .namedD `allowDiff .nat 0 + .namedD `allowDiff .nat 0 <*> + many (.named `expandTrace .name false) where output : ValDesc m Ident := { description := "output name", @@ -643,8 +648,6 @@ def leanOutput : CodeBlockExpander | args, str => do let config ← LeanOutputConfig.parser.run args - let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character) - PointOfInterest.save (← getRef) (config.name.getId.toString) (kind := Lsp.SymbolKind.file) (selectionRange := config.name) @@ -657,9 +660,12 @@ def leanOutput : CodeBlockExpander normalizeMetavars str.getString else str.getString + let mut texts : Array (Highlighted.Span.Kind × String) := #[] + if config.allowDiff == 0 then for msg in msgs do - let txt := msg.toString + let txt := msg.toString (expandTraces := config.expandTraces) + texts := texts.push (msg.severity, txt) let actual := if config.normalizeMetas then normalizeMetavars txt @@ -669,7 +675,7 @@ def leanOutput : CodeBlockExpander if s != msg.severity.toSeverity then throwErrorAt str s!"Expected severity {sevStr s}, but got {sevStr msg.severity.toSeverity}" if config.show then - let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize))} #[Block.code $(quote str.getString)]) + let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize), ($(quote config.expandTraces) : List Name))} #[Block.code $(quote str.getString)]) return #[content] else return #[] else @@ -693,22 +699,21 @@ def leanOutput : CodeBlockExpander Log.logSilentInfo m!"Diff is {d} lines:\n{d'}" if config.show then - let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize))} #[Block.code $(quote str.getString)]) + let content ← `(Block.other {Block.leanOutput with data := ToJson.toJson ($(quote msg), $(quote config.summarize), ($(quote config.expandTraces) : List Name))} #[Block.code $(quote str.getString)]) return #[content] else return #[] - let suggs : Array (Nat × Meta.Hint.Suggestion) := msgs.toArray.map fun msg => - let strMsg := msg.toString - ((diffSize config.whitespace strMsg str.getString).1, { - suggestion := withNl msg.toString, - preInfo? := some s!"{sevStr msg.severity.toSeverity}: " + let suggs : Array (Nat × Meta.Hint.Suggestion) := texts.map fun (sev, msg) => + ((diffSize config.whitespace msg str.getString).1, { + suggestion := withNl msg, + preInfo? := some s!"{sevStr sev.toSeverity}: " }) let suggs : Array Meta.Hint.Suggestion := suggs.qsort (fun x y => x.1 < y.1) |>.map (·.2) let hintMsg := if suggs.size > 1 then m!"Replace with one of the actual messages:" else m!"Replace with the actual message:" let hint ← hintAt str hintMsg suggs - throwErrorAt str (m!"Didn't match - got: {indentD (toMessageData <| msgs.map (Std.Format.text ·.toString))}\nbut expected:{indentD (toMessageData str.getString)}" ++ hint) + throwErrorAt str (m!"Didn't match - got: {indentD (toMessageData <| texts.map (Std.Format.text ·.2))}\nbut expected:{indentD (toMessageData str.getString)}" ++ hint) where sevStr : MessageSeverity → String | .error => "error" diff --git a/src/verso/Verso/Code/External.lean b/src/verso/Verso/Code/External.lean index dc0816ea9..2986c0466 100644 --- a/src/verso/Verso/Code/External.lean +++ b/src/verso/Verso/Code/External.lean @@ -58,9 +58,9 @@ class ExternalCode (genre : Genre) where An inline element for rendering Lean messages. `plain` should suppress the annotation of the output with its message severity. -/ - leanOutputInline (message : Highlighted.Message) (plain : Bool) : Inline genre + leanOutputInline (message : Highlighted.Message) (plain : Bool) (expandTraces : List Lean.Name := []) : Inline genre /-- A block element for rendering Lean messages. -/ - leanOutputBlock (message : Highlighted.Message) (summarize : Bool := false) : Block genre + leanOutputBlock (message : Highlighted.Message) (summarize : Bool := false) (expandTraces : List Lean.Name := []) : Block genre open ExternalCode @@ -150,9 +150,16 @@ structure MessageContext extends CodeContext where The desired severity of the message. -/ severity : WithSyntax MessageSeverity + /-- + Traces classes to show expanded by default + -/ + expandTraces : List Lean.Name + +private partial def many (p : ArgParse m α) : ArgParse m (List α) := + (· :: ·) <$> p <*> many p <|> pure [] instance : FromArgs MessageContext m where - fromArgs := (fun s x => MessageContext.mk x s) <$> .positional' `severity <*> fromArgs + fromArgs := (fun s ts x => MessageContext.mk x s ts) <$> .positional' `severity <*> many (.named `expandTrace .name false) <*> fromArgs /-- A specification of which module to look in to find a quoted name, potentially made more specific with @@ -572,15 +579,15 @@ Requires that the genre have an `ExternalCode` instance. @[code_block_expander moduleOut] def moduleOut : CodeBlockExpander | args, str => withTraceNode `Elab.Verso (fun _ => pure m!"moduleOut") <| do - let {module := moduleName, anchor?, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args + let {module := moduleName, anchor?, severity, expandTraces, showProofStates := _, defSite := _} ← parseThe MessageContext args withAnchored moduleName anchor? fun hl => do let infos : Array _ := allInfo hl for (msg, _) in infos do - if messagesMatch msg.toString str.getString then + if messagesMatch (msg.toString (expandTraces := expandTraces)) str.getString then if msg.severity == .ofSeverity severity.1 then - return #[← ``(leanOutputBlock $(quote msg))] + return #[← ``(leanOutputBlock $(quote msg) (expandTraces := $(quote expandTraces)))] else let wanted ← severityName msg.severity.toSeverity throwError "Mismatched severity. Expected '{repr severity.1}', got '{wanted}'.{← severityHint wanted severity.2}" @@ -628,15 +635,15 @@ def moduleOutRole : RoleExpander | args, inls => withTraceNode `Elab.Verso (fun _ => pure m!"moduleOutRole") <| do let str? ← oneCodeStr? inls - let {module := moduleName, anchor?, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args + let {module := moduleName, anchor?, expandTraces, severity, showProofStates := _, defSite := _} ← parseThe MessageContext args withAnchored moduleName anchor? fun hl => do let infos := allInfo hl if let some str := str? then for (msg, _) in infos do - if messagesMatch msg.toString str.getString then + if messagesMatch (msg.toString (expandTraces := expandTraces)) str.getString then if msg.severity == .ofSeverity severity.1 then - return #[← ``(leanOutputInline $(quote msg) true)] + return #[← ``(leanOutputInline $(quote msg) true (expandTraces := $(quote expandTraces)))] else let wanted ← severityName msg.severity.toSeverity throwError "Mismatched severity. Expected '{repr severity.1}', got '{wanted}'.{← severityHint wanted severity.2}" diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index 1c847e1b1..e1e19130c 100644 --- a/src/verso/Verso/Code/Highlighted.lean +++ b/src/verso/Verso/Code/Highlighted.lean @@ -455,17 +455,18 @@ defmethod Highlighted.Goal.toHtml (exprHtml : expr → HighlightHtmlM g Html) (i | .never => #[("checked", "checked")] | .subsequent => if index = 0 then #[("checked", "checked")] else #[] -partial defmethod Highlighted.MessageContents.toHtml (maxTraceDepth : Nat) (exprHtml : expr → HighlightHtmlM g Html) : Highlighted.MessageContents expr → HighlightHtmlM g Html +partial defmethod Highlighted.MessageContents.toHtml (expandTraces : List Lean.Name) (maxTraceDepth : Nat) (exprHtml : expr → HighlightHtmlM g Html) : Highlighted.MessageContents expr → HighlightHtmlM g Html | .text s => pure {{{{s}}}} | .term e => do return {{{{← exprHtml e}}}} | .append xs => xs.foldlM (init := Html.empty) fun html m => - (html ++ ·) <$> m.toHtml maxTraceDepth exprHtml + (html ++ ·) <$> m.toHtml expandTraces maxTraceDepth exprHtml | .trace cls msg children collapsed => do - let msgHtml ← msg.toHtml maxTraceDepth exprHtml + let msgHtml ← msg.toHtml expandTraces maxTraceDepth exprHtml + let collapsed := collapsed && cls ∉ expandTraces let childHtml ← if maxTraceDepth = 0 then pure Html.empty else - let cs ← children.mapM (·.toHtml (maxTraceDepth - 1) exprHtml) + let cs ← children.mapM (·.toHtml expandTraces (maxTraceDepth - 1) exprHtml) pure {{}} if children.size > 0 then return {{
s!"[{cls}]" " " {{msgHtml}}{{childHtml}}
@@ -510,7 +511,7 @@ partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM g Html {{← infos.mapM fun (s, info) => do return {{ - {{← info.toHtml 10 toHtml}} }} + {{← info.toHtml [] 10 toHtml}} }} }} @@ -541,7 +542,7 @@ partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM g Html else toHtml hl | .point s info => do - let info ← info.toHtml 10 toHtml + let info ← info.toHtml [] 10 toHtml return {{ {{info}} }} @@ -560,15 +561,15 @@ defmethod Highlighted.inlineHtml (contextName : Option String) (code : Highlight else pure {{ {{ ← code.toHtml }} }} -defmethod Highlighted.Message.toHtml (message : Highlighted.Message) (maxTraceDepth : Nat := 10) : HighlightHtmlM g Html := do - let contents ← message.contents.toHtml maxTraceDepth (·.toHtml) +defmethod Highlighted.Message.toHtml (message : Highlighted.Message) (expandTraces : List Lean.Name) (maxTraceDepth : Nat := 10) : HighlightHtmlM g Html := do + let contents ← message.contents.toHtml expandTraces maxTraceDepth (·.toHtml) return {{{{contents}}}} -defmethod Highlighted.Message.blockHtml (message : Highlighted.Message) (summarize : Bool) (maxTraceDepth : Nat := 10) : HighlightHtmlM g Html := do +defmethod Highlighted.Message.blockHtml (message : Highlighted.Message) (summarize : Bool) (expandTraces : List Lean.Name := []) (maxTraceDepth : Nat := 10) : HighlightHtmlM g Html := do let wrap html := if summarize then {{
"Expand..."
{{html}}
}} else {{
{{html}}
}} - wrap <$> message.toHtml (maxTraceDepth := maxTraceDepth) + wrap <$> message.toHtml expandTraces (maxTraceDepth := maxTraceDepth) -- TODO CSS variables, and document them