Color Customization🔗

All colors in Verso's rendering of Lean code are controlled by CSS custom properties, documented in verso-vars.css. Each message severity (info, warning, error) has four configurations (here exemplified for the error severity, but also present for warning and info):

• variables for the affected code itself, via the --verso-code-error-color, --verso-code-error-bg-color, and --verso-code-error-hover-color and --verso-code-error-hover-bg-color families, plus --verso-error-indicator-color for the wavy underline,

• a variable for the text of the message, via --verso-message-error-color,

• variables for the tooltip that displays the message, via --verso-tooltip-error-color, --verso-tooltip-error-bg-color, and --verso-tooltip-error-border-color, and

• a variable for 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.

Breaking change: the variables --verso-error-color, --verso-warning-color, and --verso-info-color no longer exist. Sites that override them to recolor diagnostics should set --verso-message-error-color, --verso-message-warning-color, and --verso-message-info-color instead.

Versioned Release Note Entries🔗

An entry is a file under doc/UsersGuide/Releases/Entries/ that names the version it describes. The sections of this chapter are derived from those versions, so an entry written before a release and merged after one lands in the section for the version it actually shipped in. Pull requests are checked for an entry, and for naming the version that is under development.

Development Server🔗

Verso now includes a small HTTP server for previewing generated HTML on your own machine. Running lake exe verso-serve serves the current directory at http://127.0.0.1:8000/, and a directory and --port may be given on the command line.

The server is meant for local writing and development. It binds to 127.0.0.1 only and offers no HTTPS or authentication.

Its defaults suit Verso output. Additionally, a verso-serve.toml file configures mounts, redirects, and custom headers for projects that need more than a single directory. Because the server ships with Verso, previewing a site no longer depends on having another language ecosystem installed.

See the development server documentation for the full set of options.

Labeled Groups in Rendered Docstrings🔗

They were headings, which placed them in the document's heading outline even though they name parts of a declaration rather than sections of the text. Each label is now a paragraph tied by aria-labelledby to a container with role="group", so heading navigation reaches the document's own structure.

Logging Abstraction🔗

The build pipeline previously threaded a bare String → IO Unit error callback through traversal and output generation, and several monads carried their own ad-hoc error loggers. There was no way to emit a warning.

This release introduces Verso.MonadBuildLog, a uniform logging interface shared across the genres. A message carries a Verso.Severity (either Verso.Severity.error or Verso.Severity.warning) and an optional source location.

Breaking Change: ExtraStep🔗

Verso.Genre.Manual.ExtraStep no longer takes a String → IO Unit error callback. Instead, it runs in a monad that has an instance of Verso.MonadBuildLog, so a step can emit both errors and warnings with Verso.reportError and Verso.reportWarning.

Full-Page Search Interface🔗

Pressing "Enter" in the search box now leads to a full-page search interface that shows more results with more context and includes checkboxes to filter the results by their semantic domain. As a result, domains with custom search CSS should replace the #search-wrapper selector with the .verso-search-results class.

Search Result Prioritization🔗

This release gives authors the ability to affect search result ordering by assigning custom priorities. Priorities may be assigned as follows:

• Semantic vs full-text results can be assigned overall priority levels.

• Semantic domains may be weighted, e.g. to boost all technical terms.

• Within a domain, items may be prioritized, e.g. to lower the priority of release notes relative to other text. This is done in JavaScript in the domain mapper.

• A genre may weight full-text results for parts based on part metadata.

In the Manual genre, sections can be assigned search priority values using the metadata field Manual.PartMetadata.searchPriority, which affects their full-text and semantic results, both for themselves and their children.

Literate Programming🔗

Verso now supports a simple literate programming system, in which module docstrings are rendered as the text of a page. While no configuration is necessary to use it, aside from adding Verso as a dependency, some configuration is possible in order to customize aspects of the display. See its section in this guide for more details.