Skip to content

Block

type Block =
    | Heading of level: int * text: string * anchor: string
    | Documented of decl: int * anchor: string * docHtml: string * arguments: ArgumentRow array * statementHtml: string * proofs: ProofBlock array * refs: RefLists
    | Quiet of decl: int * anchor: string * statementHtml: string * proofs: ProofBlock array * refs: RefLists
    | Command of html: string
    | Import of html: string
    | Prose of html: string
Assembly Nacara.Plugin.Rocq

One unit of a page. Source-bearing fields decode to the exact source text.

Cases

Heading of level: int * text: string * anchor: string

A heading comment's heading. Anchors are unique on the page.

Documented of decl: int * anchor: string * docHtml: string * arguments: ArgumentRow array * statementHtml: string * proofs: ProofBlock array * refs: RefLists

A declaration with attached documentation.

Quiet of decl: int * anchor: string * statementHtml: string * proofs: ProofBlock array * refs: RefLists

A declaration with no attached documentation.

Command of html: string

A sentence outside any declaration, or the whitespace between two blocks.

Import of html: string

A sentence collected into the file's imports block. A page shows its imports together.

Prose of html: string

A comment attached to no declaration, or the text around a comment's headings.

Properties

member IsCommand: bool
member IsDocumented: bool
member IsHeading: bool
member IsImport: bool
member IsProse: bool
member IsQuiet: bool