Agda-2.8.0: 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 :: List1 String
- literateTeX :: Processor
- literateRsT :: Processor
- literateMd :: Processor
- literateOrg :: Processor
- illiterate :: [Layer] -> String
- atomizeLayers :: Layers -> [(LayerRole, Char)]
- type Processor = PositionWithoutFile -> String -> [Layer]
- type Layers = [Layer]
- data Layer = Layer {
  - layerRole :: LayerRole
  - interval :: IntervalWithoutFile
  - 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 :: List1 String Source #

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

literateTeX :: Processor Source #

Preprocessor for literate TeX.

literateRsT :: Processor Source #

Preprocessor for reStructuredText.

literateMd :: Processor Source #

Preprocessor for Markdown.

literateOrg :: Processor 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 = PositionWithoutFile -> 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 |

Fields

- layerRole :: LayerRole
- interval :: IntervalWithoutFile
- layerContent :: String

#### Instances

Instances details

HasRangeWithoutFile Layer Source # |
Instance details Defined in Agda.Syntax.Parser.Literate Methods getRangeWithoutFile :: Layer -> RangeWithoutFile Source #
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 #

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