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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.Literate

Description

Preprocessors for literate code formats.

Synopsis

- literateProcessors :: [(String, (Processor, FileType))]
- literateExtsShortList :: [String]
- literateSrcFile :: [Layer] -> SrcFile
- literateTeX :: Position -> String -> [Layer]
- literateRsT :: Position -> String -> [Layer]
- literateMd :: Position -> String -> [Layer]
- literateOrg :: Position -> String -> [Layer]
- illiterate :: [Layer] -> String
- atomizeLayers :: Layers -> [(LayerRole, Char)]
- type Processor = Position -> String -> [Layer]
- type Layers = [Layer]
- data Layer = Layer {
  - layerRole :: LayerRole
  - interval :: Interval
  - layerContent :: String
  }
- data LayerRole
  - = Markup
  - | Comment
  - | Code
- isCode :: LayerRole -> Bool
- isCodeLayer :: Layer -> Bool

# 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.

literateSrcFile :: [Layer] -> SrcFile Source #

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.

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

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 |

Fields

- layerRole :: LayerRole
- interval :: Interval
- layerContent :: String

Instances

Show Layer Source # |
Instance details Defined in Agda.Syntax.Parser.Literate Methods showsPrec :: Int -> Layer -> ShowS Source # show :: Layer -> String Source # showList :: [Layer] -> ShowS Source #
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 Methods (==) :: LayerRole -> LayerRole -> Bool Source # (/=) :: LayerRole -> LayerRole -> Bool Source #
Show LayerRole Source # |
Instance details Defined in Agda.Syntax.Parser.Literate Methods showsPrec :: Int -> LayerRole -> ShowS Source # show :: LayerRole -> String Source # showList :: [LayerRole] -> ShowS Source #

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.