Agda.Syntax.Parser.Literate

Preprocessors for literate code formats.

Documentation

literateProcessors :: [(String, (Processor, FileType))]

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.

literateExtsShortList :: [String]

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

literateSrcFile :: [Layer] -> SrcFile

literateTeX :: Position -> String -> [Layer]

Preprocessor for literate TeX.

literateRsT :: Position -> String -> [Layer]

Preprocessor for reStructuredText.

literateMd :: Position -> String -> [Layer]

Preprocessor for Markdown.

literateOrg :: Position -> String -> [Layer]

Preprocessor for Org mode documents.

illiterate :: [Layer] -> String

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.

atomizeLayers :: Layers -> [(LayerRole, Char)]

type Processor = Position -> String -> [Layer]

Type of a literate preprocessor: Invariants:

f : Processor

proposition> f pos s /= []

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

type Layers = [Layer]

A list of contiguous layers.

data Layer

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

Constructors

Layer

Fields

• layerRole :: LayerRole
• interval :: Interval
• layerContent :: String

Instances

HasRange Layer

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range

Show Layer

Defined in Agda.Syntax.Parser.Literate

Methods

showsPrec :: Int -> Layer -> ShowS

show :: Layer -> String

showList :: [Layer] -> ShowS

data LayerRole

Role of a character in the file.

Constructors

Markup

Comment

Code

Instances

Show LayerRole

Defined in Agda.Syntax.Parser.Literate

Methods

showsPrec :: Int -> LayerRole -> ShowS

show :: LayerRole -> String

showList :: [LayerRole] -> ShowS

Eq LayerRole

Defined in Agda.Syntax.Parser.Literate

Methods

(==) :: LayerRole -> LayerRole -> Bool

(/=) :: LayerRole -> LayerRole -> Bool

isCode :: LayerRole -> Bool

Returns True if the role corresponds to Agda code.

isCodeLayer :: Layer -> Bool

Returns True if the layer contains Agda code.