5. Output Formats🔗

Verso provides genre authors with tools for generating HTML and TeX code via embedded languages that reduce the syntactic overhead of constructing ASTs. These libraries may also be used by authors of extensions to the Manual genre, who need to define how each new element should be rendered to each supported backend.

5.1. HTML🔗

While most users of Verso don't need to worry about the specific details of the HTML that it produces, authors of new genres or of substantial extensions to existing genres may need to produce custom HTML. Verso's HTML output follows a number of conventions and uses built-in libraries and features.

Lean's Html type represents HTML documents.

inductive type

Lean.Html : Type
Lean.Html : Type

HTML content, which may be either a single node or a sequence of sibling nodes.

This type is optimized for convenient authoring of HTML documents. It is not formally related to the HTML DOM representation. It is analogous to React's Fragment.

Constructors

Lean.Html.element (tag : String)
  (attrs : Array (String × String)) (children : Html) : Html

An element with the given tag name, attributes, and children.

Lean.Html.text : String → Html

Textual content.

The characters &, <, and > are always escaped to HTML entities during rendering. Use raw in raw text elements (script and style) instead.

Lean.Html.raw : String → Html

Characters to be copied verbatim (and not escaped) during rendering.

Lean.Html.seq : Array Html → Html

A sequence of HTML values.

def

Lean.Html.empty : Html
Lean.Html.empty : Html

Empty HTML.

def

Lean.Html.ofArray (hs : Array Html) : Html
Lean.Html.ofArray (hs : Array Html) : Html

Merges an array of HTML values by appending them.

Like seq, but may produce a more compact representation.

def

Lean.Html.ofList (hs : List Html) : Html
Lean.Html.ofList (hs : List Html) : Html

Merges a list of HTML values by appending them.

Like seq hs.toArray, but may produce a more compact representation.

def

Lean.Html.append : Html → Html → Html
Lean.Html.append : Html → Html → Html

Appends two HTML forests.

opaque

Lean.Html.rewritePostM.{u_1} {m : Type → Type u_1} [Monad m]
  (fn : Html → m Html) : Html → m Html
Lean.Html.rewritePostM.{u_1}
  {m : Type → Type u_1} [Monad m]
  (fn : Html → m Html) : Html → m Html

Rewrites the forest by using fn to transform every node. Traversal proceeds in post-order: fn receives element and seq nodes with already-rewritten children.

def

Lean.Html.render (h : Html) : String
Lean.Html.render (h : Html) : String

Renders into a string to be consumed by browsers. The input's structure is respected as much as possible:

No whitespace is added or removed.
Tag names are not escaped.

The output uses HTML5 syntax. It is not compatible with XML syntax for HTML.

Details of the output syntax

We make the following XML-compatible choices:

Void elements with isEmpty children are rendered as self-closing tags.
- Void elements with non-isEmpty children are rendered like normal elements. Such elements are forbidden by the HTML spec.
Attribute values are always double-quoted.

And the following incompatible choices:

Attributes with empty values are minimized.

HTML documents are typically produced using an embedded DSL, accessible via the html%{…} literal syntax. For example, this definition creates a <ul> list:

def mkList (xs : List Html) : Html :=
  html%{<ul>{ xs.map fun x => html%{<li>{x}</li>} }</ul>}

<ul><li>A</li><li><emph>B</emph></li><li>C</li></ul>
#eval mkList ["A", html%{<emph>B</emph>}, "C"]
  |>.render
  |> IO.println

<ul><li>A</li><li><emph>B</emph></li><li>C</li></ul>

5.1.1. Conventions🔗

While Verso genres may generate whatever output is necessary, some aspects of the Verso infrastructure make assumptions about generated HTML. In particular, Verso assumes that HTML follows these conventions:

Each page contains a <base> tag that points at the site root, and all URLs are relative to the site root.
Pages are served as directories that contain an index.html file, rather than as bare HTML files. In other words, instead of page.html, the page should be served as page/index.html. This affects the meaning of relative URLs.

5.1.1.1. CSS🔗

The names of CSS variables that are intended for customization begin with --verso-, with a single - before the variable's name. Variables that are a part of the Verso implementation and are not intended to be directly customized use two - characters, and thus begin with --verso--.

The customizable variables and their default values are defined in verso-vars.css, which is included as the string constant Html.«verso-vars.css». Each page should include this stylesheet.

def

Verso.Output.Html.«verso-vars.css» : String
Verso.Output.Html.«verso-vars.css» :
  String

CSS variables used by all genres that should support HTML output.

5.1.1.2. Lean Code in HTML🔗

Lean code is rendered using a set of built-in CSS rules. The colors and fonts that they use are controlled by CSS variables, documented in verso-vars.css.

Each category of token that can be highlighted supports customization of its color, font weight, font style, and font family. Constants (such as List or id) are controlled by the --verso-code-const- family, keywords (such as def or induction) by the --verso-code-keyword- family, and local bindings (such as x in let x := 5) by the --verso-code-var- family. For example, keywords are styled by --verso-code-keyword-color, --verso-code-keyword-weight, --verso-code-keyword-style, and --verso-code-keyword-font-family.

Each message severity (info, warning, and error) has four sets of related styles, exemplified here for the error severity:

the affected code itself, via --verso-code-error-color, --verso-code-error-bg-color, --verso-code-error-hover-color, and --verso-code-error-hover-bg-color, plus --verso-error-indicator-color for the wavy underline that marks the presence of a message,
the text of the message, via --verso-message-error-color,
the tooltip that displays the message, via --verso-tooltip-error-color, --verso-tooltip-error-bg-color, and --verso-tooltip-error-border-color, and
the marker bar on output blocks, via --verso-output-error-color.

For readability, message text is rendered in a single color. Syntax highlighting of embedded Lean code is limited to typographic properties such as weight.

Tooltips share a generic palette (--verso-tooltip-color, --verso-tooltip-bg-color, --verso-tooltip-border-color, and --verso-tooltip-separator-color) that the severity-specific tooltip colors default to. Proof states are styled by the --verso-tactic-state- and --verso-tactic-toggle- variable families, and the hover highlight on interactive code by --verso-code-hover-bg-color.

Data intended for hovers is deduplicated while generating HTML. The content of all hovers is saved in -verso-docs.json in the site root. The data-verso-hover attribute stores the index of the hover information in this file.

Rendering highlighted code requires supporting CSS and JavaScript on each page that contains it:

highlightingStyle contains the CSS rules that style highlighted code.
highlightingJs produces JavaScript code that displays hovers and highlights other occurrences of an identifier. By default, it obtains hover content using fetchDocsJson.
Hovers are displayed using the tippy.js and popper.js libraries. Copies of them are included as the string constants Highlighted.WebAssets.tippy and Highlighted.WebAssets.popper, with source maps Highlighted.WebAssets.tippy.map and Highlighted.WebAssets.popper.map and a stylesheet Highlighted.WebAssets.tippy.border.css.
Markdown in documentation shown in hovers is rendered by the marked library, included as the string constant Highlighted.WebAssets.marked with source map Highlighted.WebAssets.marked.map.

def

Verso.Code.highlightingStyle : String
Verso.Code.highlightingStyle : String

CSS rules that style highlighted Lean code, including its tokens, messages, and proof states.

Pages that contain highlighted code should include these rules in a stylesheet. The colors and fonts that the rules apply are controlled by CSS variables, documented in verso-vars.css.

def

Verso.Code.highlightingJs
  (highlightJsonPromise : String := fetchDocsJson) : String
Verso.Code.highlightingJs
  (highlightJsonPromise : String :=
    fetchDocsJson) :
  String

JavaScript code that implements the interactive features of highlighted Lean code, displaying hovers and highlighting other occurrences of an identifier.

The parameter highlightJsonPromise is a JavaScript expression that evaluates to a promise that provides the hover content.

def

Verso.Code.fetchDocsJson : String
Verso.Code.fetchDocsJson : String

A JavaScript expression that fetches hover content from -verso-docs.json in the site root.

This is the default means by which the code generated by highlightingJs obtains hover content.

5.1.1.3. Math🔗

TeX-style mathematical notation (written $`f(x)` or $$`f(x)`, and represented by the Inline.math constructor) is rendered to a <code> element with the class math, together with the class inline or display according to the requested mode. The element's text content is the TeX code, which is not processed while generating HTML. For example, $`\frac{1}{2}` is represented in HTML as <code class="math inline">\frac{1}{2}</code>.

Math is typeset in the browser using the bundled KaTeX library. When a page has loaded, the script in Html.math.js renders every element with these classes. Pages that contain mathematical notation should include this script together with KaTeX itself: its stylesheet (Html.katex.css), its code (Html.katex.js), and its fonts (Html.katexFonts). The stylesheet refers to the fonts by relative paths, so the file layout described in their docstrings should be preserved.

def

Verso.Output.Html.katex.css : String
Verso.Output.Html.katex.css : String

The minified KaTeX CSS file's contents, to be placed parallel to the JS and fonts, in a file named katex/katex.min.css.

def

Verso.Output.Html.katex.js : String
Verso.Output.Html.katex.js : String

The minified KaTeX JS file's contents, to be placed parallel to the CSS and fonts, in a file named katex/katex.min.js.

def

Verso.Output.Html.katexFonts : Array (String × ByteArray)
Verso.Output.Html.katexFonts :
  Array (String × ByteArray)

The KaTeX font files. Keys are filenames of the form katex/fonts/....

def

Verso.Output.Html.math.js : String
Verso.Output.Html.math.js : String

A short script that renders all Verso math using KaTeX.

5.2. TeX🔗

Verso's TeX type represents LaTeX documents. They are typically produced using an embedded DSL that is available when the namespace Verso.Output.TeX is opened.

inductive type

Verso.Output.TeX : Type
Verso.Output.TeX : Type

TeX output

Constructors

Verso.Output.TeX.text (string : String) : TeX

Text to be shown in the document, escaped as needed.

Verso.Output.TeX.raw (string : String) : TeX

Raw TeX code to be included without escaping.

Verso.Output.TeX.command (name : String)
  (optArgs args : Array TeX) : TeX

A LaTeX command, with the provided optional and mandatory arguments (in square and curly brackets, respectively)

Verso.Output.TeX.environment (name : String)
  (optArgs args content : Array TeX) : TeX

A LaTeX environment, with the provided optional and mandatory arguments (in square and curly brackets, respectively)

Verso.Output.TeX.paragraphBreak : TeX

A paragraph break, rendered to TeX as a blank line

Verso.Output.TeX.seq (contents : Array TeX) : TeX

Concatenation of TeX

def

Verso.Output.TeX.empty : TeX
Verso.Output.TeX.empty : TeX

The empty TeX document

opaque

Verso.Output.TeX.asString (doc : TeX) : String
Verso.Output.TeX.asString (doc : TeX) :
  String

Converts a TeX document to a string to be processed by LaTeX

TeX documents are written in \TeX{...}, in a syntax very much like LaTeX itself. The differences are:

\Lean{...} escapes back to Lean, expecting a value of type TeX.
Text content is written as Lean string literals to facilitate precise control over whitespace.
Interpolated Lean strings (with s!) may be used in any context that expects a string.

For example, this definition creates a bulleted list list:

open Verso.Output.TeX

def mkList (xs : List TeX) : TeX :=
  \TeX{
    \begin{itemize}
      \Lean{xs.map (\TeX{\item " " \Lean{·} "\n"})}
    \end{itemize}
  }

\begin{itemize}
\item A
\item \emph{B}
\item C

\end{itemize}

#eval mkList ["A", \TeX{\emph{"B"}}, "C"]
  |>.asString
  |> IO.println

\begin{itemize}
\item A
\item \emph{B}
\item C

\end{itemize}