{-# 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 Prelude hiding (getLine)
import Data.Char (isSpace)
import Data.List (isPrefixOf)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Text.Regex.TDFA

import Agda.Utils.Impossible

-- | Role of a character in the file.

data LayerRole = Markup | Comment | Code
  deriving (Int -> LayerRole -> ShowS
[LayerRole] -> ShowS
LayerRole -> String
(Int -> LayerRole -> ShowS)
-> (LayerRole -> String)
-> ([LayerRole] -> ShowS)
-> Show LayerRole
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LayerRole] -> ShowS
$cshowList :: [LayerRole] -> ShowS
show :: LayerRole -> String
$cshow :: LayerRole -> String
showsPrec :: Int -> LayerRole -> ShowS
$cshowsPrec :: Int -> LayerRole -> ShowS
Show, LayerRole -> LayerRole -> Bool
(LayerRole -> LayerRole -> Bool)
-> (LayerRole -> LayerRole -> Bool) -> Eq LayerRole
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 -> String
layerContent :: String
  } deriving Int -> Layer -> ShowS
[Layer] -> ShowS
Layer -> String
(Int -> Layer -> ShowS)
-> (Layer -> String) -> ([Layer] -> ShowS) -> Show Layer
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Layer] -> ShowS
$cshowList :: [Layer] -> ShowS
show :: Layer -> String
$cshow :: Layer -> String
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 = Interval -> Range
forall t. HasRange t => t -> Range
getRange (Interval -> Range) -> (Layer -> Interval) -> Layer -> Range
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, String)] -> [Layer]
mkLayers Position
pos []            = Position -> [Layer]
emptyLiterate Position
pos
mkLayers Position
pos ((LayerRole
_,String
"") : [(LayerRole, String)]
xs) = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos [(LayerRole, String)]
xs
                             -- Empty layers are ignored.
mkLayers Position
pos ((LayerRole
ty,String
s) : [(LayerRole, String)]
xs) =
  LayerRole -> Interval -> String -> Layer
Layer LayerRole
ty (Position -> Position -> Interval
forall a. Position' a -> Position' a -> Interval' a
Interval Position
pos Position
next) String
s Layer -> [Layer] -> [Layer]
forall a. a -> [a] -> [a]
: Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
next [(LayerRole, String)]
xs
  where
  next :: Position
next = Position -> String -> Position
forall a. Position' a -> String -> Position' a
movePosByString Position
pos String
s

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

atomizeLayers :: Layers -> [(LayerRole, Char)]
atomizeLayers :: [Layer] -> [(LayerRole, Char)]
atomizeLayers = ([(LayerRole, String)]
-> ((LayerRole, String) -> [(LayerRole, Char)])
-> [(LayerRole, Char)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Char -> (LayerRole, Char)) -> String -> [(LayerRole, Char)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Char -> (LayerRole, Char)) -> String -> [(LayerRole, Char)])
-> ((LayerRole, String) -> Char -> (LayerRole, Char))
-> (LayerRole, String)
-> String
-> [(LayerRole, Char)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((,) (LayerRole -> Char -> (LayerRole, Char))
-> ((LayerRole, String) -> LayerRole)
-> (LayerRole, String)
-> Char
-> (LayerRole, Char)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LayerRole, String) -> LayerRole
forall a b. (a, b) -> a
fst) ((LayerRole, String) -> String -> [(LayerRole, Char)])
-> ((LayerRole, String) -> String)
-> (LayerRole, String)
-> [(LayerRole, Char)]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (LayerRole, String) -> String
forall a b. (a, b) -> b
snd) ([(LayerRole, String)] -> [(LayerRole, Char)])
-> ([Layer] -> [(LayerRole, String)])
-> [Layer]
-> [(LayerRole, Char)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Layer] -> [(LayerRole, String)]
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] -> SrcFile
literateSrcFile []                    = SrcFile
forall a. HasCallStack => a
__IMPOSSIBLE__
literateSrcFile (Layer{Interval
interval :: Interval
interval :: Layer -> Interval
interval} : [Layer]
_) = Interval -> SrcFile
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 :: [(String, (Processor, FileType))]
literateProcessors =
  ((,) (String
 -> (Processor, FileType) -> (String, (Processor, FileType)))
-> ((String, (Processor, FileType)) -> String)
-> (String, (Processor, FileType))
-> (Processor, FileType)
-> (String, (Processor, FileType))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String
".lagda" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> ((String, (Processor, FileType)) -> String)
-> (String, (Processor, FileType))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, (Processor, FileType)) -> String
forall a b. (a, b) -> a
fst ((String, (Processor, FileType))
 -> (Processor, FileType) -> (String, (Processor, FileType)))
-> ((String, (Processor, FileType)) -> (Processor, FileType))
-> (String, (Processor, FileType))
-> (String, (Processor, FileType))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String, (Processor, FileType)) -> (Processor, FileType)
forall a b. (a, b) -> b
snd) ((String, (Processor, FileType))
 -> (String, (Processor, FileType)))
-> [(String, (Processor, FileType))]
-> [(String, (Processor, FileType))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ (String
""    , (Processor
literateTeX, FileType
TexFileType))
    , (String
".rst", (Processor
literateRsT, FileType
RstFileType))
    , (String
".tex", (Processor
literateTeX, FileType
TexFileType))
    , (String
".md",  (Processor
literateMd,  FileType
MdFileType ))
    , (String
".org", (Processor
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 (LayerRole -> Bool) -> (Layer -> LayerRole) -> Layer -> Bool
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] -> String
illiterate [Layer]
xs = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ (if LayerRole -> Bool
isCode LayerRole
layerRole then ShowS
forall a. a -> a
id else ShowS
bleach) String
layerContent
  | Layer{LayerRole
layerRole :: LayerRole
layerRole :: Layer -> LayerRole
layerRole, String
layerContent :: String
layerContent :: Layer -> String
layerContent} <- [Layer]
xs
  ]

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

bleach :: String -> String
bleach :: ShowS
bleach String
s = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
go String
s
  where
  go :: Char -> Char
go Char
c | Char -> Bool
isSpace Char
c = Char
c
  go Char
_             = Char
' '

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

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

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

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

-- | Breaks a list just /after/ an element satisfying the predicate is
--   found.
--
--   >>> break1 even [1,3,5,2,4,7,8]
--   ([1,3,5,2],[4,7,8])

break1 :: (a -> Bool) -> [a] -> ([a],[a])
break1 :: (a -> Bool) -> [a] -> ([a], [a])
break1 a -> Bool
_ []           =  ([], [])
break1 a -> Bool
p (a
x:[a]
xs) | a -> Bool
p a
x = (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[],[a]
xs)
break1 a -> Bool
p (a
x:[a]
xs)       = let ([a]
ys,[a]
zs) = (a -> Bool) -> [a] -> ([a], [a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break1 a -> Bool
p [a]
xs in (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys,[a]
zs)

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

getLine :: String -> (String, String)
getLine :: String -> (String, String)
getLine = (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break1 (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n')

-- | Canonical decomposition of an empty literate file.

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

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

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

-- | Preprocessor for literate TeX.

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

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

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

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

-- | Preprocessor for Markdown.

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

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

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

  -- A non-Agda code block.
  code_other :: String -> [(LayerRole, String)]
  code_other :: String -> [(LayerRole, String)]
code_other [] = []
  code_other String
s  =
    let (String
line, String
rest) = String -> (String, String)
getLine String
s in
    (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
:
    if Regex
md_end Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line
    then String -> [(LayerRole, String)]
md String
rest
    else String -> [(LayerRole, String)]
code_other String
rest

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

-- | Preprocessor for reStructuredText.

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

  maybe_code :: String -> [(LayerRole, String)]
maybe_code String
s =
    if Regex
r_comment Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line then
      [(LayerRole, String)]
not_code
    else case Regex
r_code Regex -> String -> [[String]]
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line of
      []                         -> [(LayerRole, String)]
not_code
      [[String
_, String
before, String
"::", String
after]] ->
        -- Code starts
        if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
before Bool -> Bool -> Bool
|| Char -> Bool
isBlank (String -> Char
forall a. [a] -> a
last String
before) then
          (LayerRole
Markup, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
        else
          (LayerRole
Comment, String
before String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":") (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Markup, String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
after) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
      [[String]]
_ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    where
    (String
line, String
rest) = String -> (String, String)
getLine String
s
    not_code :: [(LayerRole, String)]
not_code     = (LayerRole
Comment, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
rst String
rest

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

  -- Process an indented block.
  indented :: String -> String -> [(LayerRole, String)]
  indented :: String -> String -> [(LayerRole, String)]
indented String
_   [] = []
  indented String
ind String
s  =
    let (String
line, String
rest) = String -> (String, String)
getLine String
s in
    if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
line then
      (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> String -> [(LayerRole, String)]
indented String
ind String
rest
    else if String
ind String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
line then
      (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> String -> [(LayerRole, String)]
indented String
ind String
rest
    else
      String -> [(LayerRole, String)]
maybe_code String
s

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

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

-- | Preprocessor for Org mode documents.

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

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

  code :: String -> [(LayerRole, String)]
  code :: String -> [(LayerRole, String)]
code [] = []
  code String
s  =
    let (String
line, String
rest) = String -> (String, String)
getLine String
s in
    if Regex
org_end Regex -> String -> Bool
forall regex source target.
RegexContext regex source target =>
regex -> source -> target
`match` String
line then
      (LayerRole
Markup, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
org String
rest
    else
      (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest

  org_end :: Regex
org_end = String -> Regex
rex' String
"\\`([[: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' :: String -> Regex
rex' = CompOption -> ExecOption -> String -> Regex
forall regex compOpt execOpt source.
RegexMaker regex compOpt execOpt source =>
compOpt -> execOpt -> source -> regex
makeRegexOpts CompOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
blankCompOpt{newSyntax :: Bool
newSyntax = Bool
True, caseSensitive :: Bool
caseSensitive = Bool
False} ExecOption
forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
blankExecOpt