{-# LANGUAGE ViewPatterns #-}
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
data LayerRole = Markup | | 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)
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
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
mkLayers :: Position -> [(LayerRole, String)] -> Layers
mkLayers :: Position -> [(LayerRole, String)] -> [Layer]
mkLayers pos :: Position
pos [] = Position -> [Layer]
emptyLiterate Position
pos
mkLayers pos :: Position
pos ((_,"") : xs :: [(LayerRole, String)]
xs) = Position -> [(LayerRole, String)] -> [Layer]
mkLayers Position
pos [(LayerRole, String)]
xs
mkLayers pos :: Position
pos ((ty :: LayerRole
ty,s :: String
s) : xs :: [(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 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} : _) = Interval -> SrcFile
forall a. Interval' a -> a
getIntervalFile Interval
interval
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
<$> (".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
<$>
[ ("" , (Processor
literateTeX, FileType
TexFileType))
, (".rst", (Processor
literateRsT, FileType
RstFileType))
, (".tex", (Processor
literateTeX, FileType
TexFileType))
, (".md", (Processor
literateMd, FileType
MdFileType ))
, (".org", (Processor
literateOrg, FileType
OrgFileType))
]
isCode :: LayerRole -> Bool
isCode :: LayerRole -> Bool
isCode Code = Bool
True
isCode Markup = Bool
False
isCode Comment = Bool
False
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
illiterate :: [Layer] -> String
illiterate :: [Layer] -> String
illiterate xs :: [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
]
bleach :: String -> String
bleach :: ShowS
bleach s :: String
s = (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
go String
s
where
go :: Char -> Char
go c :: Char
c | Char -> Bool
isSpace Char
c = Char
c
go _ = ' '
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
== '\n')
literateExtsShortList :: [String]
literateExtsShortList :: [String]
literateExtsShortList = [".lagda"]
break1 :: (a -> Bool) -> [a] -> ([a],[a])
break1 :: (a -> Bool) -> [a] -> ([a], [a])
break1 _ [] = ([], [])
break1 p :: a -> Bool
p (x :: a
x:xs :: [a]
xs) | a -> Bool
p a
x = (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[],[a]
xs)
break1 p :: a -> Bool
p (x :: a
x:xs :: [a]
xs) = let (ys :: [a]
ys,zs :: [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)
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
== '\n')
emptyLiterate :: Position -> [Layer]
emptyLiterate :: Position -> [Layer]
emptyLiterate pos :: 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) ""]
rex :: String -> Regex
rex :: String -> Regex
rex s :: 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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\\'"
literateTeX :: Position -> String -> [Layer]
literateTeX :: Processor
literateTeX pos :: Position
pos s :: 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 s :: String
s =
let (line :: String
line, rest :: 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 -> [_, pre :: String
pre, _, markup :: String
markup, whitespace :: 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 _ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
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 "(([^\\%]|\\\\.)*)(\\\\begin\\{code\\}[^\n]*)(\n)?"
code :: String -> [(LayerRole, String)]
code :: String -> [(LayerRole, String)]
code [] = []
code s :: String
s =
let (line :: String
line, rest :: 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 -> [_, code :: String
code, markup :: String
markup, post :: 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 _ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
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 "([[:blank:]]*)(\\\\end\\{code\\})(.*)"
literateMd :: Position -> String -> [Layer]
literateMd :: Processor
literateMd pos :: Position
pos s :: 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 s :: String
s =
let (line :: String
line, rest :: 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 -> [_, pre :: String
pre, markup :: String
markup, _]) ->
(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 _ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
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 "(.*)([[:space:]]*```(agda)?[[:space:]]*)"
md_begin_other :: Regex
md_begin_other = String -> Regex
rex "[[:space:]]*```[a-zA-Z0-9-]*[[:space:]]*"
code :: String -> [(LayerRole, String)]
code :: String -> [(LayerRole, String)]
code [] = []
code s :: String
s =
let (line :: String
line, rest :: 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 -> [_, markup :: String
markup]) ->
(LayerRole
Markup, String
markup) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
md String
rest
Just _ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
Nothing -> (LayerRole
Code, String
line) (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: String -> [(LayerRole, String)]
code String
rest
code_other :: String -> [(LayerRole, String)]
code_other :: String -> [(LayerRole, String)]
code_other [] = []
code_other s :: String
s =
let (line :: String
line, rest :: 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 "([[:space:]]*```[[:space:]]*)"
literateRsT :: Position -> String -> [Layer]
literateRsT :: Processor
literateRsT pos :: Position
pos s :: 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 s :: String
s = String -> [(LayerRole, String)]
maybe_code String
s
maybe_code :: String -> [(LayerRole, String)]
maybe_code s :: 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
[[_, before :: String
before, "::", after :: String
after]] ->
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]
++ ":") (LayerRole, String)
-> [(LayerRole, String)] -> [(LayerRole, String)]
forall a. a -> [a] -> [a]
: (LayerRole
Markup, ":" 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
_ -> [(LayerRole, String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
where
(line :: String
line, rest :: 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
code :: String -> [(LayerRole, String)]
code :: String -> [(LayerRole, String)]
code [] = []
code s :: String
s =
let (line :: String
line, rest :: 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
indented :: String -> String -> [(LayerRole, String)]
indented :: String -> String -> [(LayerRole, String)]
indented _ [] = []
indented ind :: String
ind s :: String
s =
let (line :: String
line, rest :: 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
r_code :: Regex
r_code = String -> Regex
rex "(.*)(::)([[:space:]]*)"
r_comment :: Regex
r_comment = String -> Regex
rex "[[:space:]]*\\.\\.([[:space:]].*)?"
literateOrg :: Position -> String -> [Layer]
literateOrg :: Processor
literateOrg pos :: Position
pos s :: 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 s :: String
s =
let (line :: String
line, rest :: 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
org_begin :: Regex
org_begin = String -> Regex
rex' "\\`(.*)([[:space:]]*\\#\\+begin_src agda2[[:space:]]+)"
code :: String -> [(LayerRole, String)]
code :: String -> [(LayerRole, String)]
code [] = []
code s :: String
s =
let (line :: String
line, rest :: 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' "\\`([[:space:]]*\\#\\+end_src[[:space:]]*)(.*)"
rex' :: String -> Regex
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