md4lean

a Lean wrapper for the MD4C Markdown parser

Parser flags

The default behavior is to recognize only Markdown syntax defined by the CommonMark specification.

However, with appropriate flags, the behavior can be tuned to enable some extensions.

def MD4Lean.MD_FLAG_COLLAPSEWHITESPACE : UInt32

With the flag MD_FLAG_COLLAPSEWHITESPACE, a non-trivial whitespace is collapsed into a single space.

Equations

• MD4Lean.MD_FLAG_COLLAPSEWHITESPACE = 1

def MD4Lean.MD_FLAG_PERMISSIVEATXHEADERS : UInt32

Do not require space in ATX headers ( ###header )

Equations

• MD4Lean.MD_FLAG_PERMISSIVEATXHEADERS = 2

def MD4Lean.MD_FLAG_PERMISSIVEURLAUTOLINKS : UInt32

With the flag MD_FLAG_PERMISSIVEURLAUTOLINKS permissive URL autolinks (not enclosed in < and >) are supported.

Equations

• MD4Lean.MD_FLAG_PERMISSIVEURLAUTOLINKS = 4

def MD4Lean.MD_FLAG_PERMISSIVEEMAILAUTOLINKS : UInt32

With the flag MD_FLAG_PERMISSIVEEMAILAUTOLINKS, permissive e-mail autolinks (not enclosed in < and >) are supported.

Equations

• MD4Lean.MD_FLAG_PERMISSIVEEMAILAUTOLINKS = 8

def MD4Lean.MD_FLAG_NOINDENTEDCODEBLOCKS : UInt32

Disable indented code blocks. (Only fenced code works.)

Equations

• MD4Lean.MD_FLAG_NOINDENTEDCODEBLOCKS = 16

def MD4Lean.MD_FLAG_NOHTMLBLOCKS : UInt32

Disable raw HTML blocks.

Equations

• MD4Lean.MD_FLAG_NOHTMLBLOCKS = 32

def MD4Lean.MD_FLAG_NOHTMLSPANS : UInt32

Disable raw HTML (inline).

Equations

• MD4Lean.MD_FLAG_NOHTMLSPANS = 64

def MD4Lean.MD_FLAG_TABLES : UInt32

With the flag MD_FLAG_TABLES, GitHub-style tables are supported.

Equations

• MD4Lean.MD_FLAG_TABLES = 256

def MD4Lean.MD_FLAG_STRIKETHROUGH : UInt32

With the flag MD_FLAG_STRIKETHROUGH, strike-through spans are enabled (text enclosed in tilde marks, e.g. ~foo bar~).

Equations

• MD4Lean.MD_FLAG_STRIKETHROUGH = 512

def MD4Lean.MD_FLAG_PERMISSIVEWWWAUTOLINKS : UInt32

With the flag MD_FLAG_PERMISSIVEWWWAUTOLINKS permissive WWW autolinks without any scheme specified (e.g. www.example.com) are supported. MD4C then assumes http: scheme.

Equations

• MD4Lean.MD_FLAG_PERMISSIVEWWWAUTOLINKS = 1024

def MD4Lean.MD_FLAG_TASKLISTS : UInt32

With the flag MD_FLAG_TASKLISTS, GitHub-style task lists are supported.

Equations

• MD4Lean.MD_FLAG_TASKLISTS = 2048

def MD4Lean.MD_FLAG_LATEXMATHSPANS : UInt32

With the flag MD_FLAG_LATEXMATHSPANS LaTeX math spans ($...$) and LaTeX display math spans ($$...$$) are supported. (Note though that the HTML renderer outputs them verbatim in a custom tag <x-equation>.)

Equations

• MD4Lean.MD_FLAG_LATEXMATHSPANS = 4096

def MD4Lean.MD_FLAG_WIKILINKS : UInt32

With the flag MD_FLAG_WIKILINKS, wiki-style links ([[link label]] and [[target article|link label]]) are supported. (Note that the HTML renderer outputs them in a custom tag <x-wikilink>.)

Equations

• MD4Lean.MD_FLAG_WIKILINKS = 8192

def MD4Lean.MD_FLAG_UNDERLINE : UInt32

With the flag MD_FLAG_UNDERLINE, underscore (_) denotes an underline instead of an ordinary emphasis or strong emphasis.

Equations

• MD4Lean.MD_FLAG_UNDERLINE = 16384

def MD4Lean.MD_FLAG_HARD_SOFT_BREAKS : UInt32

Force all soft breaks to act as hard breaks.

Equations

• MD4Lean.MD_FLAG_HARD_SOFT_BREAKS = 32768

def MD4Lean.MD_FLAG_PERMISSIVEAUTOLINKS : UInt32

Enable all auto-linking.

Equations

• MD4Lean.MD_FLAG_PERMISSIVEAUTOLINKS = MD4Lean.MD_FLAG_PERMISSIVEEMAILAUTOLINKS ||| MD4Lean.MD_FLAG_PERMISSIVEURLAUTOLINKS ||| MD4Lean.MD_FLAG_PERMISSIVEWWWAUTOLINKS

def MD4Lean.MD_FLAG_NOHTML : UInt32

Disable raw HTML.

Equations

• MD4Lean.MD_FLAG_NOHTML = MD4Lean.MD_FLAG_NOHTMLBLOCKS ||| MD4Lean.MD_FLAG_NOHTMLSPANS

Convenient sets of flags corresponding to well-known Markdown dialects.

Note we may only support subset of features of the referred dialect. The constant just enables those extensions which bring us as close as possible given what features we implement.

ABI compatibility note: Meaning of these can change in time as new extensions, bringing the dialect closer to the original, are implemented.

def MD4Lean.MD_DIALECT_COMMONMARK : UInt32

The CommonMark dialect.

Equations

• MD4Lean.MD_DIALECT_COMMONMARK = 0

def MD4Lean.MD_DIALECT_GITHUB : UInt32

The GitHub dialect.

Equations

• MD4Lean.MD_DIALECT_GITHUB = MD4Lean.MD_FLAG_PERMISSIVEAUTOLINKS ||| MD4Lean.MD_FLAG_TABLES ||| MD4Lean.MD_FLAG_STRIKETHROUGH ||| MD4Lean.MD_FLAG_TASKLISTS

HTML renderer flags

def MD4Lean.MD_HTML_FLAG_DEBUG : UInt32

If set, debug output is sent to stderr.

Equations

• MD4Lean.MD_HTML_FLAG_DEBUG = 1

def MD4Lean.MD_HTML_FLAG_VERBATIM_ENTITIES : UInt32

If set, output the entity verbatim, otherwise translate entity to its UTF-8 equivalent.

Equations

• MD4Lean.MD_HTML_FLAG_VERBATIM_ENTITIES = 2

def MD4Lean.MD_HTML_FLAG_SKIP_UTF8_BOM : UInt32

Skip UTF-8 byte order mark (BOM) in the input string.

Equations

• MD4Lean.MD_HTML_FLAG_SKIP_UTF8_BOM = 4

def MD4Lean.MD_HTML_FLAG_XHTML : UInt32

Output XHTML (e.g. <br />) instead of HTML (e.g. <br>).

Equations

• MD4Lean.MD_HTML_FLAG_XHTML = 8

def MD4Lean.MD_HTML_FLAG_MATHJAX : UInt32

Output \( and \) (which are accepted by MathJax) instead of <x-equation> for LaTeX math spans.

Equations

• MD4Lean.MD_HTML_FLAG_MATHJAX = 4096

def MD4Lean.MD_HTML_FLAG_MATHJAX_USE_DOLLAR : UInt32

Output $ (which are accepted by MathJax) instead of <x-equation> for LaTeX math spans. Must be used with MD_HTML_FLAG_MATHJAX, otherwise it is ignored.

Equations

• MD4Lean.MD_HTML_FLAG_MATHJAX_USE_DOLLAR = 8192

AST

inductive MD4Lean.AttrText : Type

The text that can occur in attributes such as link destinations, image sources, and titles

• normal : String → AttrText

  Normal text

• entity : String → AttrText

  An HTML entity as a complete string, e.g. " ".

  No validation is performed, anything that's syntactically an entity uses this constructor.

• nullchar : AttrText

  A null character

instance MD4Lean.instInhabitedAttrText : Inhabited AttrText

Equations

• MD4Lean.instInhabitedAttrText = { default := MD4Lean.instInhabitedAttrText.default }

def MD4Lean.instInhabitedAttrText.default : AttrText

Equations

• MD4Lean.instInhabitedAttrText.default = MD4Lean.AttrText.normal default

def MD4Lean.instReprAttrText.repr : AttrText → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• MD4Lean.instReprAttrText.repr MD4Lean.AttrText.nullchar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MD4Lean.AttrText.nullchar")).group prec✝

instance MD4Lean.instReprAttrText : Repr AttrText

Equations

• MD4Lean.instReprAttrText = { reprPrec := MD4Lean.instReprAttrText.repr }

def MD4Lean.instBEqAttrText.beq : AttrText → AttrText → Bool

Equations

• MD4Lean.instBEqAttrText.beq (MD4Lean.AttrText.normal a) (MD4Lean.AttrText.normal b) = (a == b)
• MD4Lean.instBEqAttrText.beq (MD4Lean.AttrText.entity a) (MD4Lean.AttrText.entity b) = (a == b)
• MD4Lean.instBEqAttrText.beq MD4Lean.AttrText.nullchar MD4Lean.AttrText.nullchar = true
• MD4Lean.instBEqAttrText.beq x✝¹ x✝ = false

instance MD4Lean.instBEqAttrText : BEq AttrText

Equations

• MD4Lean.instBEqAttrText = { beq := MD4Lean.instBEqAttrText.beq }

inductive MD4Lean.Text : Type

Inline elements (sometimes called spans or inlines)

• normal : String → Text

  Normal text

• nullchar : Text

  A null character

• br : String → Text

  A hard line break, meaningful for the semantics of the text (see MD_FLAG_HARD_SOFT_BREAKS)

• softbr : String → Text

  A soft line break (renderers will often choose to ignore this)

• entity : String → Text

  An HTML entity as a complete string, e.g. " ".

  No validation is performed, anything that's syntactically an entity uses this constructor.

• em : Array Text → Text

  Emphasized text, typically italic

• strong : Array Text → Text

  Strong emphasis, typically boldface

• u : Array Text → Text

  Underlined text (see MD_FLAG_UNDERLINE)

• a (href title : Array AttrText) (isAuto : Bool) : Array Text → Text

  A link.

  • href is the destination
  • title is the provided link title (in quotes after the URL in Markdown syntax)
  • isAuto is true when the link was created from <...> syntax, false otherwise
• img (src title : Array AttrText) (alt : Array Text) : Text

  An image.

  • src is the source URL
  • title is the provided image title (in quotes after the URL in Markdown syntax)
  • alt is the alt text for the image, to be shown if the image isn't available
• code : Array String → Text

  Code

• del : Array Text → Text

  Deleted text, typically shown as a strikethrough

• latexMath : Array String → Text

  An inline LaTeX math element, built with $...$ (see MD_FLAG_LATEXMATHSPANS)

• latexMathDisplay : Array String → Text

  An display LaTeX math element, built with $$...$$ (see MD_FLAG_LATEXMATHSPANS)

• wikiLink (target : Array AttrText) : Array Text → Text

  A wiki-style link (see MD_FLAG_WIKILINKS)

def MD4Lean.instInhabitedText.default : Text

Equations

• MD4Lean.instInhabitedText.default = MD4Lean.Text.normal default

instance MD4Lean.instInhabitedText : Inhabited Text

Equations

• MD4Lean.instInhabitedText = { default := MD4Lean.instInhabitedText.default }

instance MD4Lean.instReprText : Repr Text

Equations

• MD4Lean.instReprText = { reprPrec := MD4Lean.instReprText.repr }

partial def MD4Lean.instReprText.repr : Text → Nat → Std.Format

partial def MD4Lean.instBEqText.beq : Text → Text → Bool

instance MD4Lean.instBEqText : BEq Text

Equations

• MD4Lean.instBEqText = { beq := MD4Lean.instBEqText.beq }

structure MD4Lean.Li (α : Type u_1) : Type u_1

A list item

• li :: (
• isTask : Bool

  Is this a task?

• taskChar : Option Char

  What is in the checkbox? Always 'X', 'x', or ' ' if not none. (see MD_FLAG_TASKLISTS)

• taskMarkOffset : Option USize

  Where is the task mark in the document? (see MD_FLAG_TASKLISTS)

• contents : Array α

  The contents of the list item

• )

instance MD4Lean.instInhabitedLi {a✝ : Type u_1} : Inhabited (Li a✝)

Equations

• MD4Lean.instInhabitedLi = { default := MD4Lean.instInhabitedLi.default }

def MD4Lean.instInhabitedLi.default {a✝ : Type u_1} : Li a✝

Equations

• MD4Lean.instInhabitedLi.default = { isTask := default, taskChar := default, taskMarkOffset := default, contents := default }

def MD4Lean.instReprLi.repr {α✝ : Type u_1} [Repr α✝] : Li α✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance MD4Lean.instReprLi {α✝ : Type u_1} [Repr α✝] : Repr (Li α✝)

Equations

• MD4Lean.instReprLi = { reprPrec := MD4Lean.instReprLi.repr }

def MD4Lean.instBEqLi.beq {α✝ : Type u_1} [BEq α✝] : Li α✝ → Li α✝ → Bool

Equations

• One or more equations did not get rendered due to their size.
• MD4Lean.instBEqLi.beq x✝¹ x✝ = false

instance MD4Lean.instBEqLi {α✝ : Type u_1} [BEq α✝] : BEq (Li α✝)

Equations

• MD4Lean.instBEqLi = { beq := MD4Lean.instBEqLi.beq }

inductive MD4Lean.Block : Type

A block-level element

• p : Array Text → Block

  A paragraph

• ul (tight : Bool) (mark : Char) : Array (Li Block) → Block

  An unordered list

• ol (tight : Bool) (start : Nat) (mark : Char) : Array (Li Block) → Block

  An ordered list

• hr : Block

  A thematic break, indicated with -------

• header : Nat → Array Text → Block

  A header

• code (info lang : Array AttrText) (fenceChar : Option Char) : Array String → Block

  A code bock (see MD_FLAG_NOINDENTEDCODEBLOCKS).

  The info field contains the rest of the text after the initial fence, while lang contains the prefix of info that specifies the language. fenceChar is the character used to delimit the block (backtick or tilde).

  For indented code blocks, info and lang are #[] and fenceChar is none.

• html : Array String → Block

  Inline HTML block (see MD_FLAG_NOHTMLBLOCKS or MD_FLAG_NOHTML)

• blockquote : Array Block → Block

  A block quote (introduced with >)

• table (head : Array (Array Text)) (body : Array (Array (Array Text))) : Block

  A table

  • head is array in which each element is a cell in the header
  • body is array in which each element is a row in the body. Each row is an array of cells.

def MD4Lean.instInhabitedBlock.default : Block

Equations

• MD4Lean.instInhabitedBlock.default = MD4Lean.Block.p default

instance MD4Lean.instInhabitedBlock : Inhabited Block

Equations

• MD4Lean.instInhabitedBlock = { default := MD4Lean.instInhabitedBlock.default }

instance MD4Lean.instReprBlock : Repr Block

Equations

• MD4Lean.instReprBlock = { reprPrec := MD4Lean.instReprBlock.repr }

partial def MD4Lean.instReprBlock.repr : Block → Nat → Std.Format

partial def MD4Lean.instBEqBlock.beq : Block → Block → Bool

instance MD4Lean.instBEqBlock : BEq Block

Equations

• MD4Lean.instBEqBlock = { beq := MD4Lean.instBEqBlock.beq }

structure MD4Lean.Document : Type

A document

• blocks : Array Block

  The block-level elements of the document

instance MD4Lean.instInhabitedDocument : Inhabited Document

Equations

• MD4Lean.instInhabitedDocument = { default := MD4Lean.instInhabitedDocument.default }

def MD4Lean.instInhabitedDocument.default : Document

Equations

• MD4Lean.instInhabitedDocument.default = { blocks := default }

instance MD4Lean.instReprDocument : Repr Document

Equations

• MD4Lean.instReprDocument = { reprPrec := MD4Lean.instReprDocument.repr }

def MD4Lean.instReprDocument.repr : Document → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance MD4Lean.instBEqDocument : BEq Document

Equations

• MD4Lean.instBEqDocument = { beq := MD4Lean.instBEqDocument.beq }

def MD4Lean.instBEqDocument.beq : Document → Document → Bool

Equations

• MD4Lean.instBEqDocument.beq { blocks := a } { blocks := b } = (a == b)
• MD4Lean.instBEqDocument.beq x✝¹ x✝ = false

Functions

@[extern lean_md4c_markdown_to_html]

opaque MD4Lean.renderHtml (input : String) (parserFlags : UInt32 := MD_DIALECT_GITHUB ||| MD_FLAG_LATEXMATHSPANS ||| MD_FLAG_NOHTML) (rendererFlags : UInt32 := MD_HTML_FLAG_XHTML ||| MD_HTML_FLAG_MATHJAX ||| MD_HTML_FLAG_MATHJAX_USE_DOLLAR) : Option String

Render Markdown into HTML.

Note only contents of <body> tag is generated. Caller must generate HTML header/footer manually before/after calling this function.

• input is the input markdown string.
• parserFlags is bitmask of MD_FLAG_xxxx.
• rendererFlags is bitmask of MD_HTML_FLAG_xxxx.

Return Option.some s if render is successful, otherwise return Option.none.

@[extern lean_md4c_markdown_parse]

opaque MD4Lean.parse (input : String) (parserFlags : UInt32 := MD_DIALECT_COMMONMARK) : Option Document

Parses Markdown into an AST.

• input is the input markdown string.
• parserFlags is bitmask of MD_FLAG_xxxx.

Returns some if the underlying md4c parser succeeds, or none if it fails.