Source

module Source


Assembly	`Nacara.Plugin.Rocq`

Renders byte ranges of a Rocq source file as HTML. Decoding the HTML gives back the exact source text.

Declared inside


`Ref`	A reference site on a page

Functions and values

encode (value: string) : string

Encodes text for an element or a double-quoted attribute. A prime stays literal, so an anchor and its links compare equal as written.

indent (line: string) : int

The width of a line's leading spaces and tabs. A blank line has none.

lines (html: string) : string array

An HTML fragment's lines. Each keeps its newline and balances its own tags, and the concatenated text equals the fragment's text.

render (file: RocqFile) (refAt: Span -> Ref option) (span: Span) : string

Renders span, with keywords and comments marked and a data-ref element at each reference and binder site refAt keys. An overlapping site after the first is rendered as plain text.

Parameter
`file`	The file holding the span.
`refAt`	The key of a reference or binder site, or `None` to render it as plain text.
`span`	The byte range. It must fall on UTF-8 character boundaries.

stripTags (html: string) : string

The text of an HTML fragment: tags removed and entities decoded once.

text (file: RocqFile) (span: Span) : string

The exact source text of span.