Should comment tokens be output?
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Parser.Comments
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
- value keepComments
- value keepCommentsM
- value nestedComment
- value hole
- value skipBlock
- PackageAgda-2.8.0.2
- Exports5
- LanguageHaskell2010
- LicenceMIT
- SourceComments.hs
Should comment tokens be output?
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.
Lex a hole ({! ... !}). Holes can be nested.
Returns TokSymbol SymQuestionMark.
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.