feat: summaries of long output in blog genre

src/verso-blog/Verso/Genre/Blog.lean

@@ -245,6 +245,7 @@ def lean : CodeBlockExpander
 structure LeanOutputConfig where
   name : Ident
   severity : Option MessageSeverity
+  summarize : Bool
 
 def LeanOutputConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (args : Array Arg) : m LeanOutputConfig := do
   if h : 0 < args.size then
@@ -253,11 +254,15 @@ def LeanOutputConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [
     let (severityArgs, args) := takeNamed `severity <| args.extract 1 args.size
     let severityArg ← takeVal `severity severityArgs >>= Option.mapM (asSeverity `severity)
 
+    let (summarizeArgs, args) := takeNamed `summarize args
+    let summarizeArg ← takeVal `summarize summarizeArgs >>= Option.mapM (asBool `summarize)
+
     if !args.isEmpty then
       throwError s!"Unexpected arguments: {repr args}"
     pure {
       name := outputName
       severity := severityArg
+      summarize := summarizeArg.getD false
     }
   else throwError "No arguments provided, expected at least a context name"
 where
@@ -270,6 +275,14 @@ where
       else if b' == ``MessageSeverity.information then pure MessageSeverity.information
       else throwErrorAt b "Expected 'error' or 'warning' or 'information'"
     | other => throwError "Expected severity for '{name}', got {repr other}"
+  asBool (name : Name) (v : ArgVal) : m Bool := do
+    match v with
+    | .name b => do
+      let b' ← resolveGlobalConstNoOverloadWithInfo b
+      if b' == ``true then pure true
+      else if b' == ``false then pure false
+      else throwErrorAt b "Expected 'true' or 'false'"
+    | other => throwError "Expected Boolean for '{name}', got {repr other}"
   takeVal {α} (key : Name) (vals : Array α) : m (Option α) := do
     if vals.size = 0 then pure none
     else if h : vals.size = 1 then
@@ -291,7 +304,16 @@ def leanOutput : Doc.Elab.CodeBlockExpander
         if let some s := config.severity then
           if s != m.severity then
             throwErrorAt str s!"Expected severity {sev s}, but got {sev m.severity}"
-        return #[← ``(Block.other (Blog.BlockExt.htmlDiv $(quote (sev m.severity))) #[Block.code none #[] 0 $(quote str.getString)])]
+        let content ← if config.summarize then
+            let lines := str.getString.splitOn "\n"
+            let pre := lines.take 3
+            let post := String.join (lines.drop 3 |>.intersperse "\n")
+            let preHtml : Html := pre.map (fun (l : String) => {{<code>{{l}}</code>}})
+            ``(Block.other (Blog.BlockExt.htmlDetails $(quote (sev m.severity)) $(quote preHtml)) #[Block.code none #[] 0 $(quote post)])
+          else
+            ``(Block.other (Blog.BlockExt.htmlDiv $(quote (sev m.severity))) #[Block.code none #[] 0 $(quote str.getString)])
+
+        return #[content]
     for m in messages do
       Verso.Doc.Suggestion.saveSuggestion str (m.take 30 ++ "…") m
     throwErrorAt str "Didn't match - expected one of: {indentD (toMessageData messages)}\nbut got:{indentD (toMessageData str.getString)}"

src/verso-blog/Verso/Genre/Blog/Basic.lean

@@ -15,6 +15,7 @@ inductive BlockExt where
   | highlightedCode (contextName : Lean.Name) (highlighted : Highlighted)
   | lexedText (content : LexedText)
   | htmlDiv (classes : String)
+  | htmlDetails (classes : String) (summary : Html)
   | blob (html : Html)
 deriving Repr
 

src/verso-blog/Verso/Genre/Blog/Template.lean

@@ -167,6 +167,8 @@ def blockHtml (g : Genre) (go : Block g → HtmlT g IO Html) : Blog.BlockExt →
     pure {{ <pre class=s!"lexed {content.name}"> {{ content.toHtml }} </pre> }}
   | .highlightedCode contextName hls, _contents => do
     pure {{ <pre class="hl lean" "data-lean-context"={{toString contextName}}> {{ hls.toHtml }} </pre> }}
+  | .htmlDetails classes summary, contents => do
+    pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM go}}</details>}}
   | .htmlDiv classes, contents => do
     pure {{ <div class={{classes}}> {{← contents.mapM go}} </div> }}
   | .blob html, _ => pure html

src/verso/Verso/Output/Html.lean

@@ -15,6 +15,21 @@ inductive Html where
   | seq (contents : Array Html)
 deriving Repr, Inhabited, TypeName
 
+open Syntax in
+partial instance : Quote Html where
+  quote := q
+where
+  quoteArray {α : _} (_inst : Quote α) (xs : Array α) : TSyntax `term :=
+    mkCApp ``List.toArray #[quote xs.toList]
+
+  q
+    | .text esc str =>
+      mkCApp ``Html.text #[quote esc, quote str]
+    | .tag name attrs contents =>
+      mkCApp ``Html.tag #[quote name, quote attrs, q contents]
+    | .seq contents =>
+      mkCApp ``Html.seq #[quoteArray ⟨q⟩ contents]
+
 def Html.empty : Html := .seq #[]
 
 def Html.append : Html → Html → Html