module Text.Highlighting.Kate.Syntax.Agda
(highlight, parseExpression, syntaxName, syntaxExtensions)
where
import Text.Highlighting.Kate.Types
import Text.Highlighting.Kate.Common
import Text.ParserCombinators.Parsec hiding (State)
import Control.Monad.State
import Data.Char (isSpace)
import qualified Data.Set as Set
syntaxName :: String
syntaxName :: [Char]
syntaxName = [Char]
"Agda"
syntaxExtensions :: String
syntaxExtensions :: [Char]
syntaxExtensions = [Char]
"*.agda"
highlight :: String -> [SourceLine]
highlight :: [Char] -> [SourceLine]
highlight [Char]
input = forall s a. State s a -> s -> a
evalState (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Char] -> State SyntaxState SourceLine
parseSourceLine forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
lines [Char]
input) SyntaxState
startingState
parseSourceLine :: String -> State SyntaxState SourceLine
parseSourceLine :: [Char] -> State SyntaxState SourceLine
parseSourceLine = KateParser Token -> [Char] -> State SyntaxState SourceLine
mkParseSourceLine (Maybe ([Char], [Char]) -> KateParser Token
parseExpression forall a. Maybe a
Nothing)
parseExpression :: Maybe (String,String)
-> KateParser Token
parseExpression :: Maybe ([Char], [Char]) -> KateParser Token
parseExpression Maybe ([Char], [Char])
mbcontext = do
([Char]
lang,[Char]
cont) <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([Char], [Char])
mbcontext
Token
result <- ([Char], [Char]) -> KateParser Token
parseRules ([Char]
lang,[Char]
cont)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional forall a b. (a -> b) -> a -> b
$ do forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof
forall (m :: * -> *) u s. Monad m => (u -> u) -> ParsecT s u m ()
updateState forall a b. (a -> b) -> a -> b
$ \SyntaxState
st -> SyntaxState
st{ synStPrevChar :: Char
synStPrevChar = Char
'\n' }
ParsecT [Char] SyntaxState Identity ()
pEndLine
forall (m :: * -> *) a. Monad m => a -> m a
return Token
result
startingState :: SyntaxState
startingState = SyntaxState {synStContexts :: ContextStack
synStContexts = [([Char]
"Agda",[Char]
"code")], synStLineNumber :: Int
synStLineNumber = Int
0, synStPrevChar :: Char
synStPrevChar = Char
'\n', synStPrevNonspace :: Bool
synStPrevNonspace = Bool
False, synStContinuation :: Bool
synStContinuation = Bool
False, synStCaseSensitive :: Bool
synStCaseSensitive = Bool
True, synStKeywordCaseSensitive :: Bool
synStKeywordCaseSensitive = Bool
True, synStCaptures :: [[Char]]
synStCaptures = []}
pEndLine :: ParsecT [Char] SyntaxState Identity ()
pEndLine = do
forall (m :: * -> *) u s. Monad m => (u -> u) -> ParsecT s u m ()
updateState forall a b. (a -> b) -> a -> b
$ \SyntaxState
st -> SyntaxState
st{ synStPrevNonspace :: Bool
synStPrevNonspace = Bool
False }
([Char], [Char])
context <- KateParser ([Char], [Char])
currentContext
ContextStack
contexts <- SyntaxState -> ContextStack
synStContexts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` forall (m :: * -> *) s u. Monad m => ParsecT s u m u
getState
SyntaxState
st <- forall (m :: * -> *) s u. Monad m => ParsecT s u m u
getState
if forall (t :: * -> *) a. Foldable t => t a -> Int
length ContextStack
contexts forall a. Ord a => a -> a -> Bool
>= Int
2
then case ([Char], [Char])
context of
([Char], [Char])
_ | SyntaxState -> Bool
synStContinuation SyntaxState
st -> forall (m :: * -> *) u s. Monad m => (u -> u) -> ParsecT s u m ()
updateState forall a b. (a -> b) -> a -> b
$ \SyntaxState
st -> SyntaxState
st{ synStContinuation :: Bool
synStContinuation = Bool
False }
([Char]
"Agda",[Char]
"code") -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
([Char]
"Agda",[Char]
"comment") -> (ParsecT [Char] SyntaxState Identity ()
popContext) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] SyntaxState Identity ()
pEndLine
([Char]
"Agda",[Char]
"comments") -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
([Char]
"Agda",[Char]
"hole") -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
([Char]
"Agda",[Char]
"char") -> (ParsecT [Char] SyntaxState Identity ()
popContext) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT [Char] SyntaxState Identity ()
pEndLine
([Char]
"Agda",[Char]
"string") -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
([Char], [Char])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
else forall (m :: * -> *) a. Monad m => a -> m a
return ()
withAttribute :: a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute a
attr [Char]
txt = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
txt) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail [Char]
"Parser matched no text"
forall (m :: * -> *) u s. Monad m => (u -> u) -> ParsecT s u m ()
updateState forall a b. (a -> b) -> a -> b
$ \SyntaxState
st -> SyntaxState
st { synStPrevChar :: Char
synStPrevChar = forall a. [a] -> a
last [Char]
txt
, synStPrevNonspace :: Bool
synStPrevNonspace = SyntaxState -> Bool
synStPrevNonspace SyntaxState
st Bool -> Bool -> Bool
|| Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace [Char]
txt) }
forall (m :: * -> *) a. Monad m => a -> m a
return (a
attr, [Char]
txt)
list_reserved_keywords :: Set [Char]
list_reserved_keywords = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words forall a b. (a -> b) -> a -> b
$ [Char]
"abstract codata coinductive constructor data field forall hiding import in inductive infix infixl infixr let open pattern postulate primitive private public module mutual quote quoteGoal quoteTerm record renaming rewrite syntax to unquote using where with"
regex_'5c'7b'2d'23'2e'2a'23'2d'5c'7d :: Regex
regex_'5c'7b'2d'23'2e'2a'23'2d'5c'7d = Bool -> [Char] -> Regex
compileRegex Bool
True [Char]
"\\{-#.*#-\\}"
regex_'28Prop'7cSet'5b₀'2d₉'5d'2b'7cSet'5b0'2d9'5d'2a'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 :: Regex
regex_'28Prop'7cSet'5b₀'2d₉'5d'2b'7cSet'5b0'2d9'5d'2a'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = Bool -> [Char] -> Regex
compileRegex Bool
True [Char]
"(Prop|Set[\8320-\8329]+|Set[0-9]*)(?=([_;.\"(){}@]|\\s|$))"
regex_'28'2d'3e'7c'2192'7c'2200'7cλ'7c'3a'7c'3d'7c'5c'7c'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 :: Regex
regex_'28'2d'3e'7c'2192'7c'2200'7cλ'7c'3a'7c'3d'7c'5c'7c'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = Bool -> [Char] -> Regex
compileRegex Bool
True [Char]
"(->|\8594|\8704|\955|:|=|\\|)(?=([_;.\"(){}@]|\\s|$))"
regex_'5cd'2b'5c'2e'5cd'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 :: Regex
regex_'5cd'2b'5c'2e'5cd'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = Bool -> [Char] -> Regex
compileRegex Bool
True [Char]
"\\d+\\.\\d+(?=([_;.\"(){}@]|\\s|$))"
regex_'5b0'2d9'5d'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 :: Regex
regex_'5b0'2d9'5d'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 = Bool -> [Char] -> Regex
compileRegex Bool
True [Char]
"[0-9]+(?=([_;.\"(){}@]|\\s|$))"
regex_'5b'5e'5f'3b'2e'22'28'29'7b'7d'40'5cs'5d'2b :: Regex
regex_'5b'5e'5f'3b'2e'22'28'29'7b'7d'40'5cs'5d'2b = Bool -> [Char] -> Regex
compileRegex Bool
True [Char]
"[^_;.\"(){}@\\s]+"
parseRules :: ([Char], [Char]) -> KateParser Token
parseRules ([Char]
"Agda",[Char]
"code") =
(((Regex -> KateParser [Char]
pRegExpr Regex
regex_'5c'7b'2d'23'2e'2a'23'2d'5c'7d forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
PreprocessorTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(([Char] -> Set [Char] -> KateParser [Char]
pKeyword [Char]
" \n\t.();{}_;.\"(){}@" Set [Char]
list_reserved_keywords forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
KeywordTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Regex -> KateParser [Char]
pRegExpr Regex
regex_'28Prop'7cSet'5b₀'2d₉'5d'2b'7cSet'5b0'2d9'5d'2a'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
DataTypeTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Regex -> KateParser [Char]
pRegExpr Regex
regex_'28'2d'3e'7c'2192'7c'2200'7cλ'7c'3a'7c'3d'7c'5c'7c'29'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
OtherTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Regex -> KateParser [Char]
pRegExpr Regex
regex_'5cd'2b'5c'2e'5cd'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
FloatTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Regex -> KateParser [Char]
pRegExpr Regex
regex_'5b0'2d9'5d'2b'28'3f'3d'28'5b'5f'3b'2e'22'28'29'7b'7d'40'5d'7c'5cs'7c'24'29'29 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
DecValTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> KateParser [Char]
pDetectChar Bool
False Char
'\'' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CharTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ ([Char], [Char]) -> ParsecT [Char] SyntaxState Identity ()
pushContext ([Char]
"Agda",[Char]
"char"))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> KateParser [Char]
pDetectChar Bool
False Char
'"' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
StringTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ ([Char], [Char]) -> ParsecT [Char] SyntaxState Identity ()
pushContext ([Char]
"Agda",[Char]
"string"))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'-' Char
'-' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CommentTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ ([Char], [Char]) -> ParsecT [Char] SyntaxState Identity ()
pushContext ([Char]
"Agda",[Char]
"comment"))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'{' Char
'-' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CommentTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ ([Char], [Char]) -> ParsecT [Char] SyntaxState Identity ()
pushContext ([Char]
"Agda",[Char]
"comments"))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'{' Char
'!' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
OtherTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ ([Char], [Char]) -> ParsecT [Char] SyntaxState Identity ()
pushContext ([Char]
"Agda",[Char]
"hole"))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(([Char] -> KateParser [Char]
pAnyChar [Char]
"_;.\"(){}@\\\\" forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
OtherTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Regex -> KateParser [Char]
pRegExpr Regex
regex_'5b'5e'5f'3b'2e'22'28'29'7b'7d'40'5cs'5d'2b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
NormalTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Char], [Char])
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (([Char], [Char])
x forall a. Eq a => a -> a -> Bool
== ([Char]
"Agda",[Char]
"code")) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> KateParser [Char]
pDefault forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
NormalTok))
parseRules ([Char]
"Agda",[Char]
"comment") =
(KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Char], [Char])
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (([Char], [Char])
x forall a. Eq a => a -> a -> Bool
== ([Char]
"Agda",[Char]
"comment")) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> KateParser [Char]
pDefault forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CommentTok)
parseRules ([Char]
"Agda",[Char]
"comments") =
(((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'{' Char
'-' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CommentTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ ([Char], [Char]) -> ParsecT [Char] SyntaxState Identity ()
pushContext ([Char]
"Agda",[Char]
"comments"))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'-' Char
'}' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CommentTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ (ParsecT [Char] SyntaxState Identity ()
popContext))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Char], [Char])
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (([Char], [Char])
x forall a. Eq a => a -> a -> Bool
== ([Char]
"Agda",[Char]
"comments")) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> KateParser [Char]
pDefault forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CommentTok))
parseRules ([Char]
"Agda",[Char]
"hole") =
(((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'!' Char
'}' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
OtherTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ (ParsecT [Char] SyntaxState Identity ()
popContext))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Char], [Char])
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (([Char], [Char])
x forall a. Eq a => a -> a -> Bool
== ([Char]
"Agda",[Char]
"hole")) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> KateParser [Char]
pDefault forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
OtherTok))
parseRules ([Char]
"Agda",[Char]
"char") =
(((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'\\' Char
'\'' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CharTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> KateParser [Char]
pDetectChar Bool
False Char
'\'' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CharTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ (ParsecT [Char] SyntaxState Identity ()
popContext))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Char], [Char])
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (([Char], [Char])
x forall a. Eq a => a -> a -> Bool
== ([Char]
"Agda",[Char]
"char")) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> KateParser [Char]
pDefault forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
CharTok))
parseRules ([Char]
"Agda",[Char]
"string") =
(((Bool -> Char -> Char -> KateParser [Char]
pDetect2Chars Bool
False Char
'\\' Char
'"' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
StringTok))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
((Bool -> Char -> KateParser [Char]
pDetectChar Bool
False Char
'"' forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
StringTok) forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
>>~ (ParsecT [Char] SyntaxState Identity ()
popContext))
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|>
(KateParser ([Char], [Char])
currentContext forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \([Char], [Char])
x -> forall (f :: * -> *). Alternative f => Bool -> f ()
guard (([Char], [Char])
x forall a. Eq a => a -> a -> Bool
== ([Char]
"Agda",[Char]
"string")) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> KateParser [Char]
pDefault forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {m :: * -> *} {a} {s}.
Monad m =>
a -> [Char] -> ParsecT s SyntaxState m (a, [Char])
withAttribute TokenType
StringTok))
parseRules ([Char], [Char])
x = ([Char], [Char]) -> KateParser Token
parseRules ([Char]
"Agda",[Char]
"code") forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"Unknown context" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ([Char], [Char])
x)