Agda.Syntax.Parser.Literate

List of valid extensions for literate Agda files, and their corresponding preprocessors.

If you add new extensions, remember to update test/Utils.hs so that test cases ending in the new extensions are found.

Short list of extensions for literate Agda files. For display purposes.

Preprocessor for literate TeX.

Preprocessor for reStructuredText.

Preprocessor for Markdown.

Preprocessor for Org mode documents.

Blanks the non-code parts of a given file, preserving positions of characters corresponding to code. This way, there is a direct correspondence between source positions and positions in the processed result.

Type of a literate preprocessor: Invariants:

f : Processor

proposition> f pos s /= []

proposition> f pos s >>= layerContent == s

A list of contiguous layers.

A sequence of characters in a file playing the same role.

Role of a character in the file.

Returns True if the role corresponds to Agda code.

Returns True if the layer contains Agda code.