Lean4
/-- Render the given rewrite results. -/
def renderRewrites (e : Expr) (results : Array (Array RewriteInterface × Kind)) (init : Option Html) (range : Lsp.Range)
(doc : FileWorker.EditableDocument) (showNames : Bool) : MetaM Html := do
let htmls ← results.filterMapM (renderSection showNames)
let htmls :=
match init with
| some html => #[html] ++ htmls
| none => htmls
if htmls.isEmpty then
return <p>No rewrites found for <InteractiveCode fmt={← ppExprTagged e}/></p>
else
return .element "div" #[("style", json% {"marginLeft": "4px"})] htmls
where
/-- Render one section of rewrite results. -/
renderSection (showNames : Bool) (sec : Array RewriteInterface × Kind) : MetaM (Option Html) := do
let some head := sec.1[0]? |
return none
let suffix :=
match sec.2 with
| .hypothesis => " (local hypotheses)"
| .fromFile => " (lemmas from current file)"
| .fromCache => ""
return
<details
«open»={true}><summary
className="mv2 pointer">Pattern
{←
pattern head.lemmaType head.symm
(return
<InteractiveCode
fmt={←
ppExprTagged ·}/>)}{.text suffix}</summary>{renderSectionCore showNames sec.1}</details>
/-- Render the list of rewrite results in one section. -/
renderSectionCore (showNames : Bool) (sec : Array RewriteInterface) : Html :=
.element "ul" #[("style", json% {"padding-left": "30px"})] <|
sec.map fun rw =>
<li>{.element "p" #[] <|
let button :=
<span
className="font-code">{Html.ofComponent MakeEditLink (.ofReplaceRange doc.meta range rw.tactic)
#[.text rw.replacementString]}</span>
let extraGoals :=
rw.extraGoals.flatMap fun extraGoal =>
#[<br/>, <strong className="goal-vdash">⊢ </strong>, <InteractiveCode fmt={extraGoal}/>]
#[button] ++ extraGoals ++
if showNames then #[<br/>, <InteractiveCode fmt={rw.prettyLemma}/>] else #[]}</li>
