| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Syntax.Parser.Comments

Description
This module defines the lex action to lex nested comments. As is well-known this cannot be done by regular expressions (which, incidently, is probably the reason why C-comments don't nest). When scanning nested comments we simply keep track of the nesting level, counting up for open comments and down for close comments.
Synopsis

keepComments :: LexPredicate
keepCommentsM :: Parser Bool
nestedComment :: LexAction Token
hole :: LexAction Token
skipBlock :: String -> String -> LookAhead ()

Documentation

keepComments :: LexPredicate | Source

Should comment tokens be output?

keepCommentsM :: Parser Bool | Source

Should comment tokens be output?

nestedComment :: LexAction Token | Source

Manually lexing a block comment. Assumes an open comment has been lexed. In the end the comment is discarded and `lexToken` is called to lex a real token.

hole :: LexAction Token | Source

Lex a hole (`{! ... !}`). Holes can be nested. Returns ``TokSymbol` `SymQuestionMark``.

skipBlock :: String -> String -> LookAhead () | Source

Skip a block of text enclosed by the given open and close strings. Assumes the first open string has been consumed. Open-close pairs may be nested.
Produced by Haddock version 2.4.2