Documentation with Verso

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🔗

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.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}

5.3. Themes for Code🔗

A code theme is a genre-neutral description of how rendered code should look, including colors, token styling, and font choices. Any Verso genre can use code themes. The built-in Manual genre extends code themes with further fonts and colors. Please refer to its theming documentation for more information.

A code theme is a value of type CodeTheme with the @[code_theme] attribute.

5.3.1. Colors and Palettes🔗

5.3.1.1. The Color Type and color% Literal🔗

Colors are represented by the Color type.

🔗inductive type
Verso.Theme.Color : Type
Verso.Theme.Color : Type

A color.

Constructors

Verso.Theme.Color.rgba (red green blue alpha : UInt8) :
  Theme.Color

A color in sRGB with an alpha channel, each channel a byte.

🔗def
Verso.Theme.Color.rgb (red green blue : UInt8) : Theme.Color
Verso.Theme.Color.rgb
  (red green blue : UInt8) : Theme.Color

Constructs an opaque color.

A number of built-in color constants are provided:

🔗def
Verso.Theme.Color.white : Theme.Color
Verso.Theme.Color.white : Theme.Color

Opaque white.

🔗def
Verso.Theme.Color.black : Theme.Color
Verso.Theme.Color.black : Theme.Color

Opaque black.

🔗def
Verso.Theme.Color.gray : Theme.Color
Verso.Theme.Color.gray : Theme.Color

A medium gray, matching the CSS gray keyword (#808080).

🔗def
Verso.Theme.Color.red : Theme.Color
Verso.Theme.Color.red : Theme.Color

Opaque red, matching the CSS red keyword (#ff0000).

🔗def
Verso.Theme.Color.green : Theme.Color
Verso.Theme.Color.green : Theme.Color

Opaque green, matching the CSS green keyword (#008000, not full-intensity #00ff00).

🔗def
Verso.Theme.Color.blue : Theme.Color
Verso.Theme.Color.blue : Theme.Color

Opaque blue, matching the CSS blue keyword (#0000ff).

🔗def
Verso.Theme.Color.transparent : Theme.Color
Verso.Theme.Color.transparent :
  Theme.Color

Fully transparent (zero alpha).

5.3.1.2. Named Reference Palettes🔗

To support bundled themes, Verso ships with a number of popular color palettes. Each palette has an associated namespace that contains the named colors from the palette along with a name : String and a sourceLink of type SourceLink, which is a source that can be linked to in theme-selection UIs.

🔗structure
Verso.Theme.SourceLink : Type
Verso.Theme.SourceLink : Type

A hyperlink: the URL plus the visible link text. Surfaced by the picker UI alongside a theme or palette so readers can follow the link to its canonical reference.

Constructor

Verso.Theme.SourceLink.mk

Fields

url : String

The URL the link points to.

text : String

The visible link text.

Okabe-Ito

Masataka Okabe and Kei Ito's eight-hue colorblind-safe palette, published in 2002 as part of their guidance on accessible color use in scientific visualization. The hues stay distinguishable under protanopia, deuteranopia, and tritanopia, which makes them a standard reference set for code highlighting that must remain readable to dichromat readers. The namespace Verso.Theme.Color.Palettes.OkabeIto provides black, orange, skyBlue, bluishGreen, yellow, blue, vermillion, and reddishPurple.

Solarized

Ethan Schoonover's standard cream-on-paper palette of sixteen colors: eight monotones plus eight accent hues. Schoonover's rebasing rule splits the monotones by substrate: base0 and base1 are dark-mode foreground tones (body text and emphasized content, respectively), base00 and base01 are the light-mode counterparts, and the four remaining shades (base02, base03, base2, base3) are background and highlight tones for each substrate. The namespace Verso.Theme.Color.Palettes.Solarized provides base03 through base3 for the monotones and yellow, orange, red, magenta, violet, blue, cyan, and green for the accent hues.

Dracula and Alucard

The canonical dark Dracula palette and its light-substrate counterpart Alucard, from the official Dracula spec. Each palette shares twelve color slots — background, current line, selection, foreground, comment, red, orange, yellow, green, cyan, purple, pink — with documented semantic intent that ports the palette into syntax highlighting (pink for keywords, cyan for classes and types, orange for numbers and booleans, yellow for strings, green for functions, purple for instance reserved words, red for errors). The namespaces Verso.Theme.Color.Palettes.DraculaClassic and Verso.Theme.Color.Palettes.AlucardClassic each provide the twelve named colors.

Nord

Sven Greb's arctic, north-bluish palette of sixteen colors organized in four groups: Polar Night (nord0 through nord3) for dark-substrate backgrounds and code surfaces, Snow Storm (nord4 through nord6) for body text on dark backgrounds and substrates on light variants, Frost (nord7 through nord10) for the canonical syntax accents, and Aurora (nord11 through nord15) for warm accent hues used by diagnostics and additional syntax categories. The namespace Verso.Theme.Color.Palettes.Nord provides each numbered constant.

5.3.2. Fonts and Typefaces🔗

The Typeface type represents a general typeface. There are three built-in faces, Typeface.sans, Typeface.serif, and Typeface.mono, which stand for unspecified sans-serif, serif, and monospaced font faces. Specific font faces may be provided using the Typeface.files constructor, which bundles font files with sufficient metadata to use them in a theme.

🔗inductive type
Verso.Typeface : Type
Verso.Typeface : Type

A concrete font for theme text. The sans, serif, and mono constructors refer to some arbitrary built-in family that may vary from system to system, while files is used to refer to specific files.

Constructors

Verso.Typeface.sans : Typeface

Some sans-serif font

Verso.Typeface.serif : Typeface

Some serif font

Verso.Typeface.mono : Typeface

Some monospace font

Verso.Typeface.files (family : String)
  (faces : Array FontFace) : Typeface

A specific font, provided as files

5.3.2.1. define_font_face🔗

To make it easier to include custom fonts, Verso provides the define_font_face command, which declares a FontFace value by name and embeds the font file into the resulting .olean at compile time. This allows themes that include fonts to be distributed as ordinary Lean libraries.

🔗def
Verso.defineFontFace : Lean.ParserDescr
Verso.defineFontFace : Lean.ParserDescr

Defines a FontFace whose FontFace.bytes are embedded from a file at compile time.

The fields, in any order: format (required), file (required, a string literal path relative to the current source file), weights (defaults to (.fixed .regular : FaceWeights)), weight (sugar: weight := w is rewritten to a fixed-weight value), and style (defaults to (.normal : FontStyle)). For example:

define_font_face sourceSansVariable where
  weights := .variable .thin .black
  format := .ttf
  file := "fonts/SourceSans3-VF.ttf"

These FontFace declarations are then composed into a Typeface via the Typeface.files constructor.

5.3.3. The CodeTheme Structure🔗

🔗structure
Verso.Theme.CodeTheme : Type
Verso.Theme.CodeTheme : Type

A typed code theme. Defaults reproduce today's hardcoded chrome, so a default-constructed theme is visually unchanged from the pre-theming look.

Many field defaults refer to earlier fields (for example a token color defaults to codeColor, which in turn defaults to textColor). Lean evaluates defaults at the moment a theme value is constructed, so on a fresh construction overriding a referenced field propagates to every later field that defaulted from it. A with update against an existing theme value freezes the defaults that were already computed there, so a substantially different theme (a dark variant of a light base, say) needs to set the dependent fields explicitly.

Constructor

Verso.Theme.CodeTheme.mk

Fields

name : String

A human-readable name for the theme (shown in the picker).

appearance : Theme.Appearance

Whether this theme is intended for a light or a dark display.

description : Option String

An optional one- or two-sentence description shown alongside the theme in the picker. Useful for noting design intent, palette family, or accessibility trade-offs.

sourceLink : Option Theme.SourceLink

An optional canonical reference for the theme: a URL plus link text shown next to the name in the picker. Points readers at an upstream homepage or specification when the theme is a port.

codeFace : Typeface

The font used for code blocks and inline code.

background : Theme.Color

The page and content background color. The contrast reference for body text.

codeBlockBackground : Theme.Color

The background behind code blocks. The contrast reference for token colors.

inlineBackground : Option Theme.Color

The background behind inline code in prose. When set, inline code gets padding and rounding.

textColor : Theme.Color

The color of body prose text.

codeColor : Theme.Color

The color of code text.

structureColor : Theme.Color

The color used for structural decoration (such as case labels).

selectedColor : Theme.Color

The background color used to highlight a selected token in code.

infoColor : Theme.Color

The message-text color for informational diagnostics.

infoIndicatorColor : Theme.Color

The accent color (left border, underline) for informational diagnostics.

warningColor : Theme.Color

The message-text color for warning diagnostics.

warningIndicatorColor : Theme.Color

The accent color (left border, underline) for warning diagnostics.

errorColor : Theme.Color

The message-text color for error diagnostics.

errorIndicatorColor : Theme.Color

The accent color (left border, underline) for error diagnostics.

const : Theme.TokenStyle

Token styling for constants.

keyword : Theme.TokenStyle

Token styling for keywords.

var : Theme.TokenStyle

Token styling for variables (bound names).

literal : Theme.TokenStyle

Token styling for literal tokens.

literalString : Theme.TokenStyle

Token styling for string literals.

literalNumber : Theme.TokenStyle

Token styling for numeric literals.

literalChar : Theme.TokenStyle

Token styling for character literals.

docComment : Theme.TokenStyle

Token styling for docstrings.

comment : Theme.TokenStyle

Token styling for the body text of ordinary comments, both line comments and block comments.

commentDelim : Theme.TokenStyle

Token styling for comment delimiters — the opener of a line comment and the /-/-/ openers/closers of a block comment.

sort : Theme.TokenStyle

Token styling for sort formers: Type, Prop, Sort.

levelVar : Theme.TokenStyle

Token styling for universe-level variables (u, v, … in a universe-parameter context).

levelConst : Theme.TokenStyle

Token styling for universe-level numeric constants (the 3 in Type 3).

levelOp : Theme.TokenStyle

Token styling for universe-level operators (max, imax, +).

moduleName : Theme.TokenStyle

Token styling for module names (e.g. an import target).

delim : Theme.TokenStyle

Token styling for built-in syntactic delimiters such as :=, =>, ←, @, :, |. CSS class .delim.

operator : Theme.TokenStyle

Token styling for symbolic operator atoms such as +, ::, >>=. CSS class .punctuation.operator.

bracket : Theme.TokenStyle

Token styling for paired delimiter atoms such as ( ), [ ], { }, ⟨, ⟩.

separator : Theme.TokenStyle

Token styling for item-separator atoms such as , and ;.

hoverBackground : Theme.Color

The background of hover popups, diagnostic boxes, and tooltips.

hoverBorderColor : Theme.Color

The border color of hover popups and plain tooltips.

hoverText : Theme.Color

The text color inside hover popups.

hoverSeparatorColor : Theme.Color

The separator line color inside hover popups.

tokenHighlightBackground : Theme.Color

The background tint applied to a token on hover (independent of severity).

tacticStateBackground : Theme.Color

The background of a displayed tactic state.

tacticStateBorderColor : Theme.Color

The border color of a displayed tactic state.

highlightOnCode : Theme.Color

An accent background drawn behind highlighted code. codeColor must read on it.

highlightOnText : Theme.Color

An accent background drawn behind highlighted code or prose. Both code and text must read on it.

uiOnCode : Theme.Color

A neutral UI element color drawn against codeBlockBackground (e.g. a toggle pill).

extraCss : String → String

Theme-specific CSS appended after the standard variable block. The asset root path the function receives is relative to verso-themes.css so url() references resolve from there.

assets : Array Theme.ThemeAsset

Non-font assets (such as images) bundled with the theme.

Remember to register code themes using the @[code_theme] attribute.

5.3.4. Accessibility Checking🔗

Code themes are checked for accessibility. These checks are by nature incomplete: they can discover the presence of problems, but not their absence. Nonetheless, ensuring that the default theme used by a document passes these tests is a good first step towards accessibility.

🔗def
Verso.Theme.CodeTheme.checkAccessibility (theme : Theme.CodeTheme) :
  Array Theme.Color.Issue
Verso.Theme.CodeTheme.checkAccessibility
  (theme : Theme.CodeTheme) :
  Array Theme.Color.Issue

Checks a theme for contrast and color-vision-deficiency problems. The checker is pure and genre neutral: it returns an Array of Issue values whose Issue.kind field a caller routes to its severity flag.

Body text uses the WCAG AA 4.5 threshold; UI accents and large-text positions use 3.0. Token distinguishability uses the CIEDE2000 threshold from distinguishableThreshold.

The check compares the color fields of a CodeTheme and returns an array of Issue values, one per problem found.

Themes may contain arbitrary CSS. In this case, some other means of checking accessibility should be used.

5.3.4.1. Contrast🔗

The contrast checker uses two thresholds: WCAG AA's 4.5:1 ratio for primary text and 3:1 for UI accents and large-text positions.

The following contrasts are checked at the text threshold (4.5:1):

  • Body, error-message, warning-message, and info-message text against the page background.

  • Each themed token color against the code-block background.

  • The code color against the inline-code background, when one is set.

  • The code color against both highlight backgrounds, and body text against the prose-highlight background.

  • Hover-popup text against the hover-popup background and against the tactic-state background.

  • Code against the tactic-state background.

The following contrasts are checked at the large text threshold (3:1):

  • Each diagnostic accent (error, warning, info indicator) against the page background.

  • The neutral UI-element color against the code-block background.

  • The tactic-state border against the tactic-state background.

Images that contain text are not automatically checked, and must be checked for accessibility in some other way.

5.3.4.2. Color Perception🔗

The eleven token colors are checked for perceptual distinctness in four separate modes:

  • unmodified

  • simulated protanopia

  • simulated deuteranopia

  • simulated tritanopia.

Every pair must remain perceptibly distinct (CIEDE2000 ΔE above a tunable threshold). A pair of identical colors is not an issue, because such themes have explicitly decided not to distinguish that pair using color.

A translucent foreground is composited over its background (via Color.over) before checking. A translucent background, by contrast, is itself reported as a contrast issue, because the effective backdrop is unknown.

5.3.4.3. The Issue Type🔗

Issues are reported using the type Issue, which describes the accessibility issue.

🔗structure
Verso.Theme.Color.Issue : Type
Verso.Theme.Color.Issue : Type

An accessibility problem found while checking a set of colors. It carries no severity; the caller maps IssueKind to a severity. The offending colors are recorded for error messages.

Constructor

Verso.Theme.Color.Issue.mk

Fields

kind : Theme.Color.IssueKind

Whether this is a contrast or a color-vision-deficiency problem.

message : String

A human-readable description of the problem.

offending : Array Theme.Color

The colors involved, for inclusion in error messages.