Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Parser.Literate

Description

Preprocessors for literate code formats.

Synopsis

Documentation

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

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] Source #

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

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

Preprocessor for literate TeX.

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

Preprocessor for reStructuredText.

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

Preprocessor for Markdown.

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

Preprocessor for Org mode documents.

illiterate :: [Layer] -> String Source #

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 Processor = Position -> String -> [Layer] Source #

Type of a literate preprocessor: Invariants:

f : Processor

proposition> f pos s /= []

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

type Layers = [Layer] Source #

A list of contiguous layers.

data Layer Source #

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

Constructors

Layer 

Instances

Instances details
HasRange Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range Source #

Show Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

showsPrec :: Int -> Layer -> ShowS

show :: Layer -> String

showList :: [Layer] -> ShowS

data LayerRole Source #

Role of a character in the file.

Constructors

Markup 
Comment 
Code 

Instances

Instances details
Show LayerRole Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

showsPrec :: Int -> LayerRole -> ShowS

show :: LayerRole -> String

showList :: [LayerRole] -> ShowS

Eq LayerRole Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

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

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

isCode :: LayerRole -> Bool Source #

Returns True if the role corresponds to Agda code.

isCodeLayer :: Layer -> Bool Source #

Returns True if the layer contains Agda code.