module Agda.Syntax.Parser.Literate (
literateProcessors,
literateExts,
literateExtsShortList,
literateSrcFile,
literateTeX,
literateRsT,
illiterate,
isCode,
Processor,
Layer(..),
LayerType(..)
)
where
import Prelude hiding (getLine)
import Data.Char (isSpace, isControl)
import Data.List (isPrefixOf)
import Agda.Syntax.Position
import Text.Regex.TDFA
#if __GLASGOW_HASKELL__ <= 708
import Control.Applicative ((<$>),(<*>))
#endif
#include "undefined.h"
import Agda.Utils.Impossible
data LayerType = Markup | Comment | Code
deriving (Show, Eq)
data Layer = Layer {
layerType :: LayerType
,interval :: Interval
,layerContent :: String
} deriving (Show)
instance HasRange Layer where
getRange = getRange . interval
mkLayers :: Position -> [(LayerType, String)] -> [Layer]
mkLayers pos [] = emptyLiterate pos
mkLayers pos ((_,""):xs) = mkLayers pos xs
mkLayers pos ((ty,s):xs) = let next = movePosByString pos s in
(Layer ty (Interval pos next) s):(mkLayers next xs)
isCode :: Layer -> Bool
isCode Layer{layerType=Code} = True
isCode Layer{layerType=Markup } = False
isCode Layer{layerType=Comment} = False
type Processor = Position -> String -> [Layer]
literateSrcFile :: [Layer] -> SrcFile
literateSrcFile [] = __IMPOSSIBLE__
literateSrcFile (Layer{interval}:_) = getIntervalFile interval
literateProcessors :: [(String, Processor)]
literateProcessors = map ((,) <$> (".lagda" ++) . fst <*> snd)
[("" , literateTeX)
,(".rst", literateRsT)
,(".tex", literateTeX)
]
illiterate :: [Layer] -> String
illiterate xs = concat [
(if isCode m then id else bleach) layerContent
| m@Layer{layerContent} <- xs]
bleach :: String -> String
bleach s = map go s
where
go c | isSpace c = c
go _ = ' '
isBlank :: Char -> Bool
isBlank = (&&) <$> isSpace <*> not . (== '\n')
literateExts :: [String]
literateExts = map fst literateProcessors
literateExtsShortList :: [String]
literateExtsShortList = [".lagda"]
break1 :: (a -> Bool) -> [a] -> ([a],[a])
break1 _ [] = ([], [])
break1 p (x:xs) | p x = (x:[],xs)
break1 p (x:xs) = let (ys,zs) = break1 p xs in (x:ys,zs)
getLine :: String -> (String, String)
getLine = break1 (== '\n')
emptyLiterate :: Position -> [Layer]
emptyLiterate pos = [Layer (Markup) (Interval pos pos) ""]
rex :: String -> Regex
rex s = makeRegexOpts blankCompOpt{newSyntax = True} blankExecOpt$ "\\`" ++ s ++ "\\'"
literateTeX :: Position -> String -> [Layer]
literateTeX pos s = mkLayers pos$ tex s
where
tex :: String -> [(LayerType, String)]
tex [] = []
tex s = let (line, rest) = getLine s in
case r_begin `matchM` line of
Just (getAllTextSubmatches -> [_, pre, markup]) ->
(Comment, pre):(Markup, markup):code rest
Just _ -> __IMPOSSIBLE__
Nothing -> (Comment, line):tex rest
r_begin = rex "(.*)([[:space:]]*\\\\begin\\{code\\}[[:space:]]*)"
code :: String -> [(LayerType, String)]
code [] = []
code s = let (line, rest) = getLine s in
case r_end `matchM` line of
Just (getAllTextSubmatches -> [_, markup, post]) ->
(Markup, markup):(Comment, post):tex rest
Just _ -> __IMPOSSIBLE__
Nothing -> (Code, line):code rest
r_end = rex "([[:space:]]*\\\\end\\{code\\}[[:space:]]*)(.*)"
literateRsT :: Position -> String -> [Layer]
literateRsT pos s = mkLayers pos$ rst s
where
rst :: String -> [(LayerType, String)]
rst [] = []
rst s = maybe_code s
maybe_code s =
if r_comment `match` line then
not_code
else case r_code `match` line of
[] -> not_code
[[_, before, "::", after]] ->
if null before || isBlank (last before) then
(Markup, line):code rest
else
(Comment, before ++ ":"):(Markup, ':':after):code rest
_ -> __IMPOSSIBLE__
where
(line, rest) = getLine s
not_code = (Comment, line):rst rest
code :: String -> [(LayerType, String)]
code [] = []
code s = let (line, rest) = getLine s in
if all isSpace line then
(Markup, line):(code rest)
else
let (xs,ys) = span isBlank line in
case xs of
[] -> maybe_code s
_ -> (Code, line):
(indented xs rest)
indented :: String -> String -> [(LayerType, String)]
indented _ [] = []
indented ind s = let (line, rest) = getLine s in
if all isSpace line then
(Code, line):(indented ind rest)
else if ind `isPrefixOf` line then
(Code, line):(indented ind rest)
else
maybe_code s
r_code = rex "(.*)(::)([[:space:]]*)"
r_comment = rex "[[:space:]]*\\.\\.([[:space:]].*)?"