lean-termcolor

ANSI colors and styled text for Lean 4. Text is pure data; terminal IO is provided by the optional detection and terminal packages.

Problem

Terminal formatting should be composable as data without forcing applications to emit escape codes or perform terminal IO.

Development

This project is maintained by its author with AI-assisted development tools. Changes are reviewed, tested, and remain the maintainer's responsibility.

Install

require termcolor from git
  "https://github.com/jonaprieto/lean-termcolor.git" @ "v1.1.2"

Quick start

import TermColor
import TermColor.Detect

open TermColor
open scoped TermColor.Style

def message : Text := Text.styled "ready" (Style.bold <+> Style.green)

#eval Text.render RenderTarget.plain message
#eval Text.render RenderTarget.ansi16 message

Color, Style, ColorScheme, Text.render, and OSC-8 hyperlinks are pure. TermColor.Detect selects a target from terminal capabilities, NO_COLOR, FORCE_COLOR, and TERM.

Build

lake build TermColor TermColor.Properties demo
lake exe demo

Related projects

termcolor-layout provides layout; termcolor-widgets provides pure views; termcolor-terminal provides terminal IO; lean-argus and oatp use the foundation.

License

Apache-2.0.