Lean4
/-- Render the unfolds of `e` as given by `filteredUnfolds`, with buttons at each suggestion
for pasting the rewrite tactic. Return `none` when there are no unfolds. -/
def renderUnfolds (e : Expr) (occ : Option Nat) (loc : Option Name) (range : Lsp.Range)
(doc : FileWorker.EditableDocument) : MetaM (Option Html) := do
let results ← filteredUnfolds e
if results.isEmpty then
return none
let core ←
results.mapM fun unfold => do
let tactic ← tacticSyntax e unfold occ loc
let tactic ← tacticPasteString tactic range
return
<li>{.element "p" #[] <|
#[<span
className="font-code"style={json%
{"white-space":
"pre-wrap"}}>{Html.ofComponent MakeEditLink (.ofReplaceRange doc.meta range tactic)
#[.text <| Format.pretty <| (← Meta.ppExpr unfold)]}</span>]}</li>
return
<details
«open»={true}><summary
className="mv2 pointer">{.text
"Definitional rewrites:"}</summary>{.element "ul" #[("style", json% {"padding-left": "30px"})]
core}</details>
