@@ -256,7 +256,9 @@ Impossible ::= 'impossible'
256256@
257257-}
258258impossible :: IdrisParser PTerm
259−impossible = PImpossible <$ reserved "impossible"
259+impossible = do fc <- reservedFC "impossible"
260+ highlightP fc AnnKeyword
261+ return PImpossible
260262
261263{- | Parses a case expression
262264@
@@ -265,9 +267,11 @@ CaseExpr ::=
265267@
266268-}
267269caseExpr :: SyntaxInfo -> IdrisParser PTerm
268−caseExpr syn = do reserved "case"; fc <- getFC
269− scr <- expr syn; reserved "of";
270+caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC
271+ scr <- expr syn; kw2 <- reservedFC "of";
270272 opts <- indentedBlock1 (caseOption syn)
273+ highlightP kw1 AnnKeyword
274+ highlightP kw2 AnnKeyword
271275 return (PCase fc scr opts)
272276 <?> "case expression"
273277
@@ -292,8 +296,9 @@ ProofExpr ::=
292296@
293297-}
294298proofExpr :: SyntaxInfo -> IdrisParser PTerm
295−proofExpr syn = do reserved "proof"
299+proofExpr syn = do kw <- reservedFC "proof"
296300 ts <- indentedBlock1 (tactic syn)
301+ highlightP kw AnnKeyword
297302 return $ PProof ts
298303 <?> "proof block"
299304
@@ -305,8 +310,9 @@ TacticsExpr :=
305310@
306311-}
307312tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
308−tacticsExpr syn = do reserved "tactics"
313+tacticsExpr syn = do kw <- reservedFC "tactics"
309314 ts <- indentedBlock1 (tactic syn)
315+ highlightP kw AnnKeyword
310316 return $ PTactics ts
311317 <?> "tactics block"
312318
@@ -508,8 +514,9 @@ UnifyLog ::=
508514 ;
509515-}
510516unifyLog :: SyntaxInfo -> IdrisParser PTerm
511−unifyLog syn = do try (lchar '%' *> reserved "unifyLog")
517+unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")
512518 tm <- simpleExpr syn
519+ highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
513520 return (PUnifyLog tm)
514521 <?> "unification log expression"
515522
@@ -519,10 +526,10 @@ RunTactics ::=
519526 ;
520527-}
521528runElab :: SyntaxInfo -> IdrisParser PTerm
522−runElab syn = do try (lchar '%' *> reserved "runElab")
529+runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")
523530 fc <- getFC
524531 tm <- simpleExpr syn
525− i <- get
532+ highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
526533 return $ PRunElab fc tm (syn_namespace syn)
527534 <?> "new-style tactics expression"
528535
@@ -532,11 +539,12 @@ Disamb ::=
532539 ;
533540-}
534541disamb :: SyntaxInfo -> IdrisParser PTerm
535−disamb syn = do reserved "with";
542+disamb syn = do kw <- reservedFC "with"
536543 ns <- sepBy1 (fst <$> name) (lchar ',')
537544 tm <- expr' syn
545+ highlightP kw AnnKeyword
538546 return (PDisamb (map tons ns) tm)
539− <?> "unification log expression"
547+ <?> "namespace disambiguation expression"
540548 where tons (NS n s) = txt (show n) : s
541549 tons n = [txt (show n)]
542550{- | Parses a no implicits expression
@@ -715,12 +723,13 @@ FieldType ::=
715723-}
716724recordType :: SyntaxInfo -> IdrisParser PTerm
717725recordType syn =
718− do reserved "record"
726+ do kw <- reservedFC "record"
719727 lchar '{'
720728 fgs <- fieldGetOrSet
721729 lchar '}'
722730 fc <- getFC
723731 rec <- optional (simpleExpr syn)
732+ highlightP kw AnnKeyword
724733 case fgs of
725734 Left fields ->
726735 case rec of
@@ -842,11 +851,13 @@ RewriteTerm ::=
842851@
843852-}
844853rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
845−rewriteTerm syn = do reserved "rewrite"
854+rewriteTerm syn = do kw <- reservedFC "rewrite"
846855 fc <- getFC
847856 prf <- expr syn
848857 giving <- optional (do symbol "==>"; expr' syn)
849− reserved "in"; sc <- expr syn
858+ kw' <- reservedFC "in"; sc <- expr syn
859+ highlightP kw AnnKeyword
860+ highlightP kw' AnnKeyword
850861 return (PRewrite fc
851862 (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc
852863 giving)
@@ -864,9 +875,10 @@ TypeSig' ::=
864875@
865876 -}
866877let_ :: SyntaxInfo -> IdrisParser PTerm
867−let_ syn = try (do reserved "let"
878+let_ syn = try (do kw <- reservedFC "let"
868879 ls <- indentedBlock (let_binding syn)
869− reserved "in"; sc <- expr syn
880+ kw' <- reservedFC "in"; sc <- expr syn
881+ highlightP kw AnnKeyword; highlightP kw' AnnKeyword
870882 return (buildLets ls sc))
871883 <?> "let binding"
872884 where buildLets [] sc = sc
@@ -911,12 +923,13 @@ QuoteGoal ::=
911923@
912924 -}
913925quoteGoal :: SyntaxInfo -> IdrisParser PTerm
914−quoteGoal syn = do reserved "quoteGoal"; n <- fst <$> name;
915− reserved "by"
926+quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;
927+ kw2 <- reservedFC "by"
916928 r <- expr syn
917− reserved "in"
929+ kw3 <- reservedFC "in"
918930 fc <- getFC
919931 sc <- expr syn
932+ mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]
920933 return (PGoal fc r n sc)
921934 <?> "quote goal expression"
922935
@@ -948,17 +961,18 @@ explicitPi opts st syn
948961 return (bindList (PPi binder) xt sc)
949962
950963autoImplicit opts st syn
951− = do reserved "auto"
964+ = do kw <- reservedFC "auto"
952965 when (st == Static) $ fail "auto implicits can not be static"
953966 xt <- typeDeclList syn
954967 lchar '}'
955968 symbol "->"
956969 sc <- expr syn
970+ highlightP kw AnnKeyword
957971 return (bindList (PPi
958972 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)
959973
960974defaultImplicit opts st syn = do
961− reserved "default"
975+ kw <- reservedFC "default"
962976 when (st == Static) $ fail "default implicits can not be static"
963977 ist <- get
964978 script' <- simpleExpr syn
@@ -967,6 +981,7 @@ defaultImplicit opts st syn = do
967981 lchar '}'
968982 symbol "->"
969983 sc <- expr syn
984+ highlightP kw AnnKeyword
970985 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)
971986
972987normalImplicit opts st syn = do
@@ -1159,8 +1174,9 @@ DoBlock ::=
11591174 -}
11601175doBlock :: SyntaxInfo -> IdrisParser PTerm
11611176doBlock syn
1162− = do reserved "do"
1177+ = do kw <- reservedFC "do"
11631178 ds <- indentedBlock1 (do_ syn)
1179+ highlightP kw AnnKeyword
11641180 return (PDoBlock ds)
11651181 <?> "do block"
11661182
@@ -1177,19 +1193,21 @@ Do ::=
11771193-}
11781194do_ :: SyntaxInfo -> IdrisParser PDo
11791195do_ syn
1180− = try (do reserved "let"
1196+ = try (do kw <- reservedFC "let"
11811197 (i, ifc) <- name
11821198 ty <- option Placeholder (do lchar ':'
11831199 expr' syn)
11841200 reservedOp "="
11851201 fc <- getFC
11861202 e <- expr syn
1203+ highlightP kw AnnKeyword
11871204 return (DoLet fc i ifc ty e))
1188− <|> try (do reserved "let"
1205+ <|> try (do kw <- reservedFC "let"
11891206 i <- expr' syn
11901207 reservedOp "="
11911208 fc <- getFC
11921209 sc <- expr syn
1210+ highlightP kw AnnKeyword
11931211 return (DoLetP fc i sc))
11941212 <|> try (do (i, ifc) <- name
11951213 symbol "<-"