| 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
- 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
proposition> f pos s /= []
proposition> f pos s >>= layerContent == s
A sequence of characters in a file playing the same role.
isCodeLayer :: Layer -> Bool Source #
Returns True if the layer contains Agda code.