Skip to content

Commit

Permalink
refactor: move argToHtml to DocGen4.Output.Arg
Browse files Browse the repository at this point in the history
  • Loading branch information
cppio committed Dec 17, 2024
1 parent a34441f commit 7cd7193
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 13 deletions.
22 changes: 22 additions & 0 deletions DocGen4/Output/Arg.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
import DocGen4.Output.Base

namespace DocGen4
namespace Output

open scoped DocGen4.Jsx

/--
Render an `Arg` as HTML, adding opacity effects etc. depending on what
type of binder it has.
-/
def argToHtml (arg : Process.Arg) : HtmlM Html := do
let node ← infoFormatToHtml arg.binder
let inner := <span class="fn">[node]</span>
let html := Html.element "span" false #[("class", "decl_args")] #[inner]
if arg.implicit then
return <span class="impl_arg">{html}</span>
else
return html

end Output
end DocGen4
14 changes: 1 addition & 13 deletions DocGen4/Output/Inductive.lean
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
import DocGen4.Output.Arg
import DocGen4.Output.Template
import DocGen4.Output.DocString
import DocGen4.Process
Expand All @@ -8,19 +9,6 @@ namespace Output
open scoped DocGen4.Jsx
open Lean

/--
Render an `Arg` as HTML, adding opacity effects etc. depending on what
type of binder it has.
-/
def argToHtml (arg : Process.Arg) : HtmlM Html := do
let node ← infoFormatToHtml arg.binder
let inner := <span class="fn">[node]</span>
let html := Html.element "span" false #[("class", "decl_args")] #[inner]
if arg.implicit then
return <span class="impl_arg">{html}</span>
else
return html

def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
pure
<details id={s!"instances-for-list-{typeName}"} «class»="instances-for-list">
Expand Down

0 comments on commit 7cd7193

Please sign in to comment.