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

text : Html

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

tag : Html

A tag with the given name and attributes.

seq : 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 : Bool) (x_1 : String) => pure none)
  (tag : String → Array (String × String) → Html → m (Option Html) :=
    fun (x : String) (x_1 : Array (String × String)) (x_2 : Html) =>
    pure none)
  (seq : Array Html → m (Option Html) := fun (x : Array Html) =>
    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 : Bool) (x_1 : String) =>
    pure none)
  (tag :
    String →
      Array (String × String) →
        Html → m (Option Html) :=
    fun (x : String)
      (x_1 : Array (String × String))
      (x_2 : Html) =>
    pure none)
  (seq : Array Html → m (Option Html) :=
    fun (x : Array Html) => 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

text : TeX

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

raw : TeX

Raw TeX code to be included without escaping.

command : TeX

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

environment : TeX

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

paragraphBreak : TeX

A paragraph break, rendered to TeX as a blank line

seq : 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}