{-# LANGUAGE ViewPatterns #-}

-- | Preprocessors for literate code formats.

module Agda.Syntax.Parser.Literate
  ( literateProcessors
  , literateExtsShortList
  , literateSrcFile
  , literateTeX
  , literateRsT
  , literateMd
  , literateOrg
  , illiterate
  , atomizeLayers
  , Processor
  , Layers
  , Layer(..)
  , LayerRole(..)
  , isCode
  , isCodeLayer
  )
  where

import Control.Monad ((<=<))
import Data.Char (isSpace)
import Data.List (isPrefixOf)
import Text.Regex.TDFA
  ( Regex, getAllTextSubmatches, match, matchM
  , makeRegexOpts, blankCompOpt, blankExecOpt, newSyntax, caseSensitive
  )

import Agda.Syntax.Common
import Agda.Syntax.Position

import Agda.Utils.List
import qualified Agda.Utils.List1 as List1

import Agda.Utils.Impossible

-- | Role of a character in the file.

data LayerRole = Markup | Comment | Code
  deriving (Int -> LayerRole -> ShowS
[LayerRole] -> ShowS
LayerRole -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [LayerRole] -> ShowS
$cshowList :: [LayerRole] -> ShowS
show :: LayerRole -> [Char]
$cshow :: LayerRole -> [Char]
showsPrec :: Int -> LayerRole -> ShowS
$cshowsPrec :: Int -> LayerRole -> ShowS
Show, LayerRole -> LayerRole -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LayerRole -> LayerRole -> Bool
$c/= :: LayerRole -> LayerRole -> Bool
== :: LayerRole -> LayerRole -> Bool
$c== :: LayerRole -> LayerRole -> Bool
Eq)

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

data Layer = Layer
  { Layer -> LayerRole
layerRole    :: LayerRole
  , Layer -> Interval
interval     :: Interval
  , Layer -> [Char]
layerContent :: String
  } deriving Int -> Layer -> ShowS
[Layer] -> ShowS
Layer -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Layer] -> ShowS
$cshowList :: [Layer] -> ShowS
show :: Layer -> [Char]
$cshow :: Layer -> [Char]
showsPrec :: Int -> Layer -> ShowS
$cshowsPrec :: Int -> Layer -> ShowS
Show

-- | A list of contiguous layers.

type Layers = [Layer]

instance HasRange Layer where
  getRange :: Layer -> Range
getRange = forall a. HasRange a => a -> Range
getRange forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layer -> Interval
interval

-- | Annotates a tokenized string with position information.

mkLayers :: Position -> [(LayerRole, String)] -> Layers
mkLayers :: Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
pos []            = Position -> [Layer]
emptyLiterate Position
pos
mkLayers Position
pos ((LayerRole
_,[Char]
"") : [(LayerRole, [Char])]
xs) = Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
pos [(LayerRole, [Char])]
xs
                             -- Empty layers are ignored.
mkLayers Position
pos ((LayerRole
ty,[Char]
s) : [(LayerRole, [Char])]
xs) =
  LayerRole -> Interval -> [Char] -> Layer
Layer LayerRole
ty (forall a. Position' a -> Position' a -> Interval' a
Interval Position
pos Position
next) [Char]
s forall a. a -> [a] -> [a]
: Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
next [(LayerRole, [Char])]
xs
  where
  next :: Position
next = forall (t :: * -> *) a.
Foldable t =>
Position' a -> t Char -> Position' a
movePosByString Position
pos [Char]
s

unMkLayers :: Layers -> [(LayerRole, String)]
unMkLayers :: [Layer] -> [(LayerRole, [Char])]
unMkLayers = forall a b. (a -> b) -> [a] -> [b]
map ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Layer -> LayerRole
layerRole forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Layer -> [Char]
layerContent)

atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers :: [Layer] -> [(LayerRole, Char)]
atomizeLayers = (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b. (a, b) -> b
snd) forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [Layer] -> [(LayerRole, [Char])]
unMkLayers

-- | Type of a literate preprocessor:
--   Invariants:
--
--   > f : Processor
--
--   prop> f pos s /= []
--
--   prop> f pos s >>= layerContent == s

type Processor = Position -> String -> [Layer]

literateSrcFile :: [Layer] -> SrcFile
literateSrcFile :: [Layer] -> Maybe RangeFile
literateSrcFile []                    = forall a. HasCallStack => a
__IMPOSSIBLE__
literateSrcFile (Layer{Interval
interval :: Interval
interval :: Layer -> Interval
interval} : [Layer]
_) = forall a. Interval' a -> a
getIntervalFile Interval
interval

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

literateProcessors :: [(String, (Processor, FileType))]
literateProcessors :: [([Char], (Position -> [Char] -> [Layer], FileType))]
literateProcessors =
  ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char]
".lagda" forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b. (a, b) -> b
snd) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ ([Char]
""    , (Position -> [Char] -> [Layer]
literateTeX, FileType
TexFileType))
    , ([Char]
".rst", (Position -> [Char] -> [Layer]
literateRsT, FileType
RstFileType))
    , ([Char]
".tex", (Position -> [Char] -> [Layer]
literateTeX, FileType
TexFileType))
    , ([Char]
".md",  (Position -> [Char] -> [Layer]
literateMd,  FileType
MdFileType ))
    , ([Char]
".org", (Position -> [Char] -> [Layer]
literateOrg, FileType
OrgFileType))
    ]

-- | Returns @True@ if the role corresponds to Agda code.

isCode :: LayerRole -> Bool
isCode :: LayerRole -> Bool
isCode LayerRole
Code    = Bool
True
isCode LayerRole
Markup  = Bool
False
isCode LayerRole
Comment = Bool
False

-- | Returns @True@ if the layer contains Agda code.

isCodeLayer :: Layer -> Bool
isCodeLayer :: Layer -> Bool
isCodeLayer = LayerRole -> Bool
isCode forall b c a. (b -> c) -> (a -> b) -> a -> c
. Layer -> LayerRole
layerRole

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

illiterate :: [Layer] -> String
illiterate :: [Layer] -> [Char]
illiterate [Layer]
xs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ (if LayerRole -> Bool
isCode LayerRole
layerRole then forall a. a -> a
id else ShowS
bleach) [Char]
layerContent
  | Layer{LayerRole
layerRole :: LayerRole
layerRole :: Layer -> LayerRole
layerRole, [Char]
layerContent :: [Char]
layerContent :: Layer -> [Char]
layerContent} <- [Layer]
xs
  ]

-- | Replaces non-space characters in a string with spaces.

bleach :: String -> String
bleach :: ShowS
bleach = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ \ Char
c -> if Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
&& Char
c forall a. Eq a => a -> a -> Bool
/= Char
'\t' then Char
c else Char
' '

-- | Check if a character is a blank character.

isBlank :: Char -> Bool
isBlank :: Char -> Bool
isBlank = Bool -> Bool -> Bool
(&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Char -> Bool
isSpace forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. Eq a => a -> a -> Bool
/= Char
'\n')

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

literateExtsShortList :: [String]
literateExtsShortList :: [[Char]]
literateExtsShortList = [[Char]
".lagda"]

-- | Returns a tuple consisting of the first line of the input, and the rest
--   of the input.

caseLine :: a -> (String -> String -> a) -> String -> a
caseLine :: forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine a
a [Char] -> [Char] -> a
k = \case
  []   -> a
a
  Char
x:[Char]
xs -> [Char] -> [Char] -> a
k (forall l. IsList l => l -> [Item l]
List1.toList List1 Char
line) [Char]
rest
    where
    (List1 Char
line, [Char]
rest) = forall a. (a -> Bool) -> a -> [a] -> (List1 a, [a])
breakAfter1 (forall a. Eq a => a -> a -> Bool
== Char
'\n') Char
x [Char]
xs

-- | Canonical decomposition of an empty literate file.

emptyLiterate :: Position -> [Layer]
emptyLiterate :: Position -> [Layer]
emptyLiterate Position
pos = [LayerRole -> Interval -> [Char] -> Layer
Layer LayerRole
Markup (forall a. Position' a -> Position' a -> Interval' a
Interval Position
pos Position
pos) [Char]
""]

-- | Create a regular expression that:
--   - Must match the whole string
--   - Works across line boundaries

rex :: String -> Regex
rex :: [Char] -> Regex
rex [Char]
s =
  forall regex compOpt execOpt source.
RegexMaker regex compOpt execOpt source =>
compOpt -> execOpt -> source -> regex
makeRegexOpts forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
blankCompOpt{newSyntax :: Bool
newSyntax = Bool
True} forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
blankExecOpt forall a b. (a -> b) -> a -> b
$
    [Char]
"\\`" forall a. [a] -> [a] -> [a]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
"\\'"

-- | Preprocessor for literate TeX.

literateTeX :: Position -> String -> [Layer]
literateTeX :: Position -> [Char] -> [Layer]
literateTeX Position
pos [Char]
s = Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
pos ([Char] -> [(LayerRole, [Char])]
tex [Char]
s)
  where
  tex :: String -> [(LayerRole, String)]
  tex :: [Char] -> [(LayerRole, [Char])]
tex = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    case Regex
r_begin forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` [Char]
line of
      Just (forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [[Char]
_, [Char]
pre, [Char]
_, [Char]
markup, [Char]
whitespace]) ->
        (LayerRole
Comment, [Char]
pre) forall a. a -> [a] -> [a]
: (LayerRole
Markup, [Char]
markup) forall a. a -> [a] -> [a]
:
        (LayerRole
Code, [Char]
whitespace) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest
      Just AllTextSubmatches [] [Char]
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] [Char])
Nothing -> (LayerRole
Comment, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
tex [Char]
rest

  r_begin :: Regex
r_begin = [Char] -> Regex
rex [Char]
"(([^\\%]|\\\\.)*)(\\\\begin\\{code\\}[^\n]*)(\n)?"

  code :: String -> [(LayerRole, String)]
  code :: [Char] -> [(LayerRole, [Char])]
code = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    case Regex
r_end forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` [Char]
line of
      Just (forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [[Char]
_, [Char]
code, [Char]
markup, [Char]
post]) ->
        (LayerRole
Code, [Char]
code) forall a. a -> [a] -> [a]
: (LayerRole
Markup, [Char]
markup) forall a. a -> [a] -> [a]
: (LayerRole
Comment, [Char]
post) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
tex [Char]
rest
      Just AllTextSubmatches [] [Char]
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] [Char])
Nothing -> (LayerRole
Code, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest

  r_end :: Regex
r_end = [Char] -> Regex
rex [Char]
"([[:blank:]]*)(\\\\end\\{code\\})(.*)"

-- | Preprocessor for Markdown.

literateMd :: Position -> String -> [Layer]
literateMd :: Position -> [Char] -> [Layer]
literateMd Position
pos [Char]
s = Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
pos forall a b. (a -> b) -> a -> b
$ [Char] -> [(LayerRole, [Char])]
md [Char]
s
  where
  md :: String -> [(LayerRole, String)]
  md :: [Char] -> [(LayerRole, [Char])]
md = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    case Regex
md_begin forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` [Char]
line of
      Just (forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [[Char]
_, [Char]
pre, [Char]
markup, [Char]
_]) ->
        (LayerRole
Comment, [Char]
pre) forall a. a -> [a] -> [a]
: (LayerRole
Markup, [Char]
markup) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest
      Just AllTextSubmatches [] [Char]
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] [Char])
Nothing ->
        (LayerRole
Comment, [Char]
line) forall a. a -> [a] -> [a]
:
        if Regex
md_begin_other forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` [Char]
line
        then [Char] -> [(LayerRole, [Char])]
code_other [Char]
rest
        else [Char] -> [(LayerRole, [Char])]
md [Char]
rest

  md_begin :: Regex
md_begin       = [Char] -> Regex
rex [Char]
"(.*)([[:space:]]*```(agda)?[[:space:]]*)"
  md_begin_other :: Regex
md_begin_other = [Char] -> Regex
rex [Char]
"[[:space:]]*```[a-zA-Z0-9-]*[[:space:]]*"

  code :: String -> [(LayerRole, String)]
  code :: [Char] -> [(LayerRole, [Char])]
code = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    case Regex
md_end forall regex source target (m :: * -> *).
(RegexContext regex source target, MonadFail m) =>
regex -> source -> m target
`matchM` [Char]
line of
      Just (forall (f :: * -> *) b. AllTextSubmatches f b -> f b
getAllTextSubmatches -> [[Char]
_, [Char]
markup]) ->
        (LayerRole
Markup, [Char]
markup) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
md [Char]
rest
      Just AllTextSubmatches [] [Char]
_  -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Maybe (AllTextSubmatches [] [Char])
Nothing -> (LayerRole
Code, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest

  -- A non-Agda code block.
  code_other :: String -> [(LayerRole, String)]
  code_other :: [Char] -> [(LayerRole, [Char])]
code_other = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    (LayerRole
Comment, [Char]
line) forall a. a -> [a] -> [a]
:
    if Regex
md_end forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` [Char]
line
    then [Char] -> [(LayerRole, [Char])]
md [Char]
rest
    else [Char] -> [(LayerRole, [Char])]
code_other [Char]
rest

  md_end :: Regex
md_end = [Char] -> Regex
rex [Char]
"([[:space:]]*```[[:space:]]*)"

-- | Preprocessor for reStructuredText.

literateRsT :: Position -> String -> [Layer]
literateRsT :: Position -> [Char] -> [Layer]
literateRsT Position
pos [Char]
s = Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
pos forall a b. (a -> b) -> a -> b
$ [Char] -> [(LayerRole, [Char])]
rst [Char]
s
  where
  rst :: String -> [(LayerRole, String)]
  rst :: [Char] -> [(LayerRole, [Char])]
rst = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] [Char] -> [Char] -> [(LayerRole, [Char])]
maybe_code

  maybe_code :: [Char] -> [Char] -> [(LayerRole, [Char])]
maybe_code [Char]
line [Char]
rest =
    if Regex
r_comment forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` [Char]
line then
      [(LayerRole, [Char])]
not_code
    else case Regex
r_code forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` [Char]
line of
      []                         -> [(LayerRole, [Char])]
not_code
      [[[Char]
_, [Char]
before, [Char]
"::", [Char]
after]] ->
        -- Code starts
        if forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True Char -> Bool
isBlank forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
lastMaybe [Char]
before then
          (LayerRole
Markup, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest
        else
          (LayerRole
Comment, [Char]
before forall a. [a] -> [a] -> [a]
++ [Char]
":") forall a. a -> [a] -> [a]
: (LayerRole
Markup, [Char]
":" forall a. [a] -> [a] -> [a]
++ [Char]
after) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest
      [[[Char]]]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    where
    not_code :: [(LayerRole, [Char])]
not_code     = (LayerRole
Comment, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
rst [Char]
rest

  -- Finds the next indented block in the input.
  code :: String -> [(LayerRole, String)]
  code :: [Char] -> [(LayerRole, [Char])]
code = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace [Char]
line then
      (LayerRole
Markup, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest
    else
      let xs :: [Char]
xs = forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isBlank [Char]
line in
      if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
xs
      then [Char] -> [Char] -> [(LayerRole, [Char])]
maybe_code [Char]
line [Char]
rest
      else (LayerRole
Code, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [Char] -> [(LayerRole, [Char])]
indented [Char]
xs [Char]
rest

  -- Process an indented block.
  indented :: String -> String -> [(LayerRole, String)]
  indented :: [Char] -> [Char] -> [(LayerRole, [Char])]
indented [Char]
ind = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace [Char]
line Bool -> Bool -> Bool
|| ([Char]
ind forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
line)
          then (LayerRole
Code, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [Char] -> [(LayerRole, [Char])]
indented [Char]
ind [Char]
rest
          else [Char] -> [Char] -> [(LayerRole, [Char])]
maybe_code [Char]
line [Char]
rest

  -- Beginning of a code block.
  r_code :: Regex
r_code = [Char] -> Regex
rex [Char]
"(.*)(::)([[:space:]]*)"

  -- Beginning of a comment block.
  r_comment :: Regex
r_comment = [Char] -> Regex
rex [Char]
"[[:space:]]*\\.\\.([[:space:]].*)?"

-- | Preprocessor for Org mode documents.

literateOrg :: Position -> String -> [Layer]
literateOrg :: Position -> [Char] -> [Layer]
literateOrg Position
pos [Char]
s = Position -> [(LayerRole, [Char])] -> [Layer]
mkLayers Position
pos forall a b. (a -> b) -> a -> b
$ [Char] -> [(LayerRole, [Char])]
org [Char]
s
  where
  org :: String -> [(LayerRole, String)]
  org :: [Char] -> [(LayerRole, [Char])]
org = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    if Regex
org_begin forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` [Char]
line then
      (LayerRole
Markup, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest
    else
      (LayerRole
Comment, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
org [Char]
rest

  -- Valid: #+begin_src agda2 :tangle yes
  -- Valid: #+begin_src agda2
  -- Invalid: #+begin_src adga2-foo
  org_begin :: Regex
org_begin = [Char] -> Regex
rex' [Char]
"\\`(.*)([[:space:]]*\\#\\+begin_src agda2[[:space:]]+)"

  code :: String -> [(LayerRole, String)]
  code :: [Char] -> [(LayerRole, [Char])]
code = forall a. a -> ([Char] -> [Char] -> a) -> [Char] -> a
caseLine [] forall a b. (a -> b) -> a -> b
$ \ [Char]
line [Char]
rest ->
    if Regex
org_end forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` [Char]
line then
      (LayerRole
Markup, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
org [Char]
rest
    else
      (LayerRole
Code, [Char]
line) forall a. a -> [a] -> [a]
: [Char] -> [(LayerRole, [Char])]
code [Char]
rest

  org_end :: Regex
org_end = [Char] -> Regex
rex' [Char]
"\\`([[:space:]]*\\#\\+end_src[[:space:]]*)(.*)"

  -- Explicit type annotation required to disambiguate source.
  rex' :: String -> Regex
  -- Source blocks start with `#+begin_src` but the casing does not matter.
  rex' :: [Char] -> Regex
rex' = forall regex compOpt execOpt source.
RegexMaker regex compOpt execOpt source =>
compOpt -> execOpt -> source -> regex
makeRegexOpts forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
blankCompOpt{newSyntax :: Bool
newSyntax = Bool
True, caseSensitive :: Bool
caseSensitive = Bool
False} forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
blankExecOpt