summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Parser/Lexer.x
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Parser/Lexer.x')
-rw-r--r--src/full/Agda/Syntax/Parser/Lexer.x23
1 files changed, 5 insertions, 18 deletions
diff --git a/src/full/Agda/Syntax/Parser/Lexer.x b/src/full/Agda/Syntax/Parser/Lexer.x
index bdb592c..966aa80 100644
--- a/src/full/Agda/Syntax/Parser/Lexer.x
+++ b/src/full/Agda/Syntax/Parser/Lexer.x
@@ -14,7 +14,7 @@ module Agda.Syntax.Parser.Lexer
( -- * The main function
lexer
-- * Lex states
- , normal, literate, code
+ , normal, code
, layout, empty_layout, bol, imp_dir
-- * Alex generated functions
, AlexReturn(..), alexScanUser
@@ -65,16 +65,6 @@ $white_nonl = $white_notab # \n
tokens :-
--- Lexing literate files
-<tex> $white_nonl* \\ "begin{code}" $white_nonl* $ { end_ }
-<tex> .+ / { keepComments } { withInterval TokTeX }
-<tex> .+ ;
-<tex> \n ;
-<tex> () / { eof } { end_ }
-<bol_,layout_>
- \\ "end{code}" / { inState code } { begin_ tex }
- -- \end{code} should only be recognized if the bottom of the stack is <code>
-
-- White space
<0,code,bol_,layout_,empty_layout_,imp_dir_>
$white_nonl+ ;
@@ -105,10 +95,10 @@ tokens :-
<pragma_> "LINE" { keyword KwLINE }
<pragma_> "MEASURE" { keyword KwMEASURE }
<pragma_> "NO_POSITIVITY_CHECK" { keyword KwNO_POSITIVITY_CHECK }
-<pragma_> "NO_SMASHING" { keyword KwNO_SMASHING }
<pragma_> "NO_TERMINATION_CHECK" { keyword KwNO_TERMINATION_CHECK }
<pragma_> "NON_TERMINATING" { keyword KwNON_TERMINATING }
<pragma_> "OPTIONS" { keyword KwOPTIONS }
+<pragma_> "POLARITY" { keyword KwPOLARITY }
<pragma_> "REWRITE" { keyword KwREWRITE }
<pragma_> "STATIC" { keyword KwSTATIC }
<pragma_> "TERMINATING" { keyword KwTERMINATING }
@@ -179,6 +169,7 @@ tokens :-
<0,code> abstract { keyword KwAbstract }
<0,code> private { keyword KwPrivate }
<0,code> instance { keyword KwInstance }
+<0,code> overlap { keyword KwOverlap }
<0,code> macro { keyword KwMacro }
<0,code> Set { keyword KwSet }
<0,code> forall { keyword KwForall }
@@ -216,6 +207,8 @@ tokens :-
<0,code> "_" { symbol SymUnderscore }
<0,code> "?" { symbol SymQuestionMark }
<0,code> "|" { symbol SymBar }
+<0,code> "(|" /[$white] { symbol SymOpenIdiomBracket }
+<0,code> "|)" { symbol SymCloseIdiomBracket }
<0,code> "(" { symbol SymOpenParen }
<0,code> ")" { symbol SymCloseParen }
<0,code> "->" { symbol SymArrow }
@@ -248,12 +241,6 @@ tokens :-
{
--- | This is the initial state for parsing a literate file. Code blocks
--- should be enclosed in @\\begin{code}@ @\\end{code}@ pairs.
-literate :: LexState
-literate = tex
-
-
-- | This is the initial state for parsing a regular, non-literate file.
normal :: LexState
normal = 0