bookshelf-doc/DocGen4/Output/Definition.lean

51 lines
1.3 KiB
Plaintext
Raw Normal View History

import DocGen4.Output.Template
2022-02-17 05:47:38 +00:00
import DocGen4.Output.DocString
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean Widget
2022-05-19 19:07:44 +00:00
/-- This is basically an arbitrary number that seems to work okay. -/
def equationLimit : Nat := 200
def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
2022-05-19 09:14:47 +00:00
pure <li class="equation">[←infoFormatToHtml c]</li>
2022-05-19 19:07:44 +00:00
/--
Attempt to render all `simp` equations for this definition. At a size
defined in `equationLimit` we stop trying since they:
- are too ugly to read most of the time
- take too long
-/
def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
2022-02-12 14:09:13 +00:00
if let some eqs := i.equations then
let equationsHtml ← eqs.mapM equationToHtml
let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit)
if equationsHtml.size ≠ filteredEquationsHtml.size then
pure #[
<details>
<summary>Equations</summary>
2022-05-19 09:14:47 +00:00
<ul class="equations">
<li class="equation">One or more equations did not get rendered due to their size.</li>
[filteredEquationsHtml]
</ul>
</details>
]
else
pure #[
<details>
<summary>Equations</summary>
2022-05-19 09:14:47 +00:00
<ul class="equations">
[filteredEquationsHtml]
</ul>
</details>
]
else
pure #[]
end Output
end DocGen4