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.

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

inductive type

Verso.Output.Html : Type
Verso.Output.Html : Type

A representation of HTML, used to render Verso to the web.

Constructors

Verso.Output.Html.text (escape : Bool) (string : String) :
  Html

Textual content. If escape is true, then characters such as '&' are escaped to entities such as "&" during rendering.

Verso.Output.Html.tag (name : String)
  (attrs : Array (String × String)) (contents : Html) : Html

A tag with the given name and attributes.

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

A sequence of HTML values.

def

Verso.Output.Html.empty : Html
Verso.Output.Html.empty : Html

The empty HTML document.

def

Verso.Output.Html.fromArray (htmls : Array Html) : Html
Verso.Output.Html.fromArray
  (htmls : Array Html) : Html

Converts an array of HTML elements into a single element by appending them.

This is equivalent to using Html.seq, but may result a more compact representation.

def

Verso.Output.Html.fromList (htmls : List Html) : Html
Verso.Output.Html.fromList
  (htmls : List Html) : Html

Converts a list of HTML elements into a single element by appending them.

This is equivalent to using Html.seq on the corresponding array, but may result in a more compact representation.

def

Verso.Output.Html.append : Html → Html → Html
Verso.Output.Html.append :
  Html → Html → Html

Appends two HTML documents.

opaque

Verso.Output.Html.visitM.{u_1} {m : Type → Type u_1} [Monad m]
  (text : Bool → String → m (Option Html) := fun x x_1 => pure none)
  (tag : String → Array (String × String) → Html → m (Option Html) :=
    fun x x_1 x_2 => pure none)
  (seq : Array Html → m (Option Html) := fun x => pure none)
  (html : Html) : m Html
Verso.Output.Html.visitM.{u_1}
  {m : Type → Type u_1} [Monad m]
  (text :
    Bool → String → m (Option Html) :=
    fun x x_1 => pure none)
  (tag :
    String →
      Array (String × String) →
        Html → m (Option Html) :=
    fun x x_1 x_2 => pure none)
  (seq : Array Html → m (Option Html) :=
    fun x => pure none)
  (html : Html) : m Html

Visit the entire tree, applying rewrites in some monad. Return none to signal that no rewrites are to be performed.

opaque

Verso.Output.Html.format : Html → Std.Format
Verso.Output.Html.format :
  Html → Std.Format

Converts HTML into a pretty-printer document. This is useful for debugging, but it does not preserve whitespace around preformatted content and scripts.

opaque

Verso.Output.Html.asString (html : Html) (indent : Nat := 0)
  (breakLines : Bool := true) : String
Verso.Output.Html.asString (html : Html)
  (indent : Nat := 0)
  (breakLines : Bool := true) : String

Converts HTML into a string that's suitable for sending to browsers, but is also readable.

HTML documents are written in double curly braces, in a syntax very much like HTML itself. The differences are:

Double curly braces escape back to Lean. This can be done for HTML elements, attribute values, or whole sets of attributes.
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 <ul> list:

open Verso.Output.Html

def mkList (xs : List Html) : Html :=
  {{ <ul> {{ xs.map ({{<li>{{·}}</li>}}) }} </ul>}}

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

#eval mkList ["A", {{<emph>"B"</emph>}}, "C"]
  |>.asString
  |> 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.

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}