module Agda.Syntax.Parser.Comments
where
import qualified Data.List as List
import {-# SOURCE #-} Agda.Syntax.Parser.LexActions
import Agda.Syntax.Parser.Monad
import Agda.Syntax.Parser.Tokens
import Agda.Syntax.Parser.Alex
import Agda.Syntax.Parser.LookAhead
import Agda.Syntax.Position
import Agda.Utils.Monad
keepComments :: LexPredicate
keepComments (_, s) _ _ _ = parseKeepComments s
keepCommentsM :: Parser Bool
keepCommentsM = fmap parseKeepComments getParseFlags
nestedComment :: LexAction Token
nestedComment inp inp' _ =
do setLexInput inp'
runLookAhead err $ skipBlock "{-" "-}"
keep <- keepCommentsM
if keep then do
inp'' <- getLexInput
let p1 = lexPos inp; p2 = lexPos inp''
i = posToInterval (lexSrcFile inp) p1 p2
s = case (p1, p2) of
(Pn { posPos = p1 }, Pn { posPos = p2 }) ->
List.genericTake (p2 - p1) $ lexInput inp
return $ TokComment (i, s)
else
lexToken
where
err _ = liftP $ parseErrorAt (lexPos inp) "Unterminated '{-'"
hole :: LexAction Token
hole inp inp' _ =
do setLexInput inp'
runLookAhead err $ skipBlock "{!" "!}"
p <- lexPos <$> getLexInput
return $
TokSymbol SymQuestionMark $
posToInterval (lexSrcFile inp) (lexPos inp) p
where
err _ = liftP $ parseErrorAt (lexPos inp) "Unterminated '{!'"
skipBlock :: String -> String -> LookAhead ()
skipBlock open close = scan 1
where
scan 0 = sync
scan n = match [ open ==> scan (n + 1)
, close ==> scan (n - 1)
] `other` scan n
where
(==>) = (,)
other = ($)