Agda-2.5.4.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Parser.Literate

Description

Preprocessors for literate code formats

Synopsis

Documentation

literateProcessors :: [(String, Processor)] 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.

literateExts :: [String] Source #

Possible extensions for a literate Agda file

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

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
f pos s /= []
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
Show Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

showsPrec :: Int -> Layer -> ShowS #

show :: Layer -> String #

showList :: [Layer] -> ShowS #

HasRange Layer Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Methods

getRange :: Layer -> Range Source #

data LayerRole Source #

Role of a character in the file

Constructors

Markup 
Comment 
Code 
Instances
Eq LayerRole Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

Show LayerRole Source # 
Instance details

Defined in Agda.Syntax.Parser.Literate

isCode :: LayerRole -> Bool Source #

Returns True if a role corresponds to Agda code

isCodeLayer :: Layer -> Bool Source #

Returns True a layer contains Agda code