Article

module Article


Assembly	`Nacara.Plugin.Rocq`

The content of a module's page: its source file in source order, as blocks of prose and code.

Declared inside


`ArgumentRow`	A row of a declaration's Arguments list
`Block`	One unit of a page
`Links`	The site-specific inputs of a page
`ProofBlock`	A proof, with any comments before the next proof
`RefItem`	An entry in a declaration's reference lists
`RefLists`	The cross-references of a declaration

Functions and values

blocks (project: RocqProject) (links: Links) (fileIndex: int) : Block array

A file's blocks in source order. The source-bearing fields, read in order, give every byte of the file apart from the comments rendered as prose.

Parameter
`project`	The project holding the file.
`links`	Builds the URLs of references.
`fileIndex`	The index in `RocqProject.Files`.

toHtml (blocks: Block array) : string

The HTML of a page's blocks, with no badges and every code body plain.

toHtmlWith (config: Config) (badge: int -> string) (blocks: Block array) : string

The HTML of a page's blocks. Proofs, imports and reference lists fold with details and need no script. The imports appear together, closed, after the page's opening heading and prose.

Parameter
`config`	The settings selecting which code bodies fold.
`badge`	The badge markup of a documented declaration, by its index in `RocqProject.Declarations`. Empty for none.
`blocks`	The page's blocks in order.

withPrintedTypes (printed: int -> string -> string option) (blocks: Block array) : Block array

Fills each argument row with no written type from Rocq's printed binders, for a row matching a statement binder.

Parameter
`printed`	The printed type, by declaration index and binder name.
`blocks`	The page's blocks.