d4f9deb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Highlight keywords in expressions

d4f9debDavid Raymond Christiansen11 years ago

src/Idris/ParseExpr.hs+41−23

compare with master

unifiedsplit

@@ -256,7 +256,9 @@ Impossible ::= 'impossible'

256@

257-}

258impossible :: IdrisParser PTerm

259−impossible = PImpossible <$ reserved "impossible"

259+impossible = do fc <- reservedFC "impossible"

260+ highlightP fc AnnKeyword

261+ return PImpossible

260

262

261{- | Parses a case expression

263{- | Parses a case expression

262@

264@

@@ -265,9 +267,11 @@ CaseExpr ::=

265@

267@

266-}

268-}

267caseExpr :: SyntaxInfo -> IdrisParser PTerm

269caseExpr :: SyntaxInfo -> IdrisParser PTerm

268−caseExpr syn = do reserved "case"; fc <- getFC

270+caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC

269− scr <- expr syn; reserved "of";

271+ scr <- expr syn; kw2 <- reservedFC "of";

270 opts <- indentedBlock1 (caseOption syn)

272 opts <- indentedBlock1 (caseOption syn)

273+ highlightP kw1 AnnKeyword

274+ highlightP kw2 AnnKeyword

271 return (PCase fc scr opts)

275 return (PCase fc scr opts)

272 <?> "case expression"

276 <?> "case expression"

273

277

@@ -292,8 +296,9 @@ ProofExpr ::=

292@

296@

293-}

297-}

294proofExpr :: SyntaxInfo -> IdrisParser PTerm

298proofExpr :: SyntaxInfo -> IdrisParser PTerm

295−proofExpr syn = do reserved "proof"

299+proofExpr syn = do kw <- reservedFC "proof"

296 ts <- indentedBlock1 (tactic syn)

300 ts <- indentedBlock1 (tactic syn)

301+ highlightP kw AnnKeyword

297 return $ PProof ts

302 return $ PProof ts

298 <?> "proof block"

303 <?> "proof block"

299

304

@@ -305,8 +310,9 @@ TacticsExpr :=

305@

310@

306-}

311-}

307tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

312tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

308−tacticsExpr syn = do reserved "tactics"

313+tacticsExpr syn = do kw <- reservedFC "tactics"

309 ts <- indentedBlock1 (tactic syn)

314 ts <- indentedBlock1 (tactic syn)

315+ highlightP kw AnnKeyword

310 return $ PTactics ts

316 return $ PTactics ts

311 <?> "tactics block"

317 <?> "tactics block"

312

318

@@ -508,8 +514,9 @@ UnifyLog ::=

508 ;

514 ;

509-}

515-}

510unifyLog :: SyntaxInfo -> IdrisParser PTerm

516unifyLog :: SyntaxInfo -> IdrisParser PTerm

511−unifyLog syn = do try (lchar '%' *> reserved "unifyLog")

517+unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")

512 tm <- simpleExpr syn

518 tm <- simpleExpr syn

519+ highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

513 return (PUnifyLog tm)

520 return (PUnifyLog tm)

514 <?> "unification log expression"

521 <?> "unification log expression"

515

522

@@ -519,10 +526,10 @@ RunTactics ::=

519 ;

526 ;

520-}

527-}

521runElab :: SyntaxInfo -> IdrisParser PTerm

528runElab :: SyntaxInfo -> IdrisParser PTerm

522−runElab syn = do try (lchar '%' *> reserved "runElab")

529+runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")

523 fc <- getFC

530 fc <- getFC

524 tm <- simpleExpr syn

531 tm <- simpleExpr syn

525− i <- get

532+ highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword

526 return $ PRunElab fc tm (syn_namespace syn)

533 return $ PRunElab fc tm (syn_namespace syn)

527 <?> "new-style tactics expression"

534 <?> "new-style tactics expression"

528

535

@@ -532,11 +539,12 @@ Disamb ::=

532 ;

539 ;

533-}

540-}

534disamb :: SyntaxInfo -> IdrisParser PTerm

541disamb :: SyntaxInfo -> IdrisParser PTerm

535−disamb syn = do reserved "with";

542+disamb syn = do kw <- reservedFC "with"

536 ns <- sepBy1 (fst <$> name) (lchar ',')

543 ns <- sepBy1 (fst <$> name) (lchar ',')

537 tm <- expr' syn

544 tm <- expr' syn

545+ highlightP kw AnnKeyword

538 return (PDisamb (map tons ns) tm)

546 return (PDisamb (map tons ns) tm)

539− <?> "unification log expression"

547+ <?> "namespace disambiguation expression"

540 where tons (NS n s) = txt (show n) : s

548 where tons (NS n s) = txt (show n) : s

541 tons n = [txt (show n)]

549 tons n = [txt (show n)]

542{- | Parses a no implicits expression

550{- | Parses a no implicits expression

@@ -715,12 +723,13 @@ FieldType ::=

715-}

723-}

716recordType :: SyntaxInfo -> IdrisParser PTerm

724recordType :: SyntaxInfo -> IdrisParser PTerm

717recordType syn =

725recordType syn =

718− do reserved "record"

726+ do kw <- reservedFC "record"

719 lchar '{'

727 lchar '{'

720 fgs <- fieldGetOrSet

728 fgs <- fieldGetOrSet

721 lchar '}'

729 lchar '}'

722 fc <- getFC

730 fc <- getFC

723 rec <- optional (simpleExpr syn)

731 rec <- optional (simpleExpr syn)

732+ highlightP kw AnnKeyword

724 case fgs of

733 case fgs of

725 Left fields ->

734 Left fields ->

726 case rec of

735 case rec of

@@ -842,11 +851,13 @@ RewriteTerm ::=

842@

851@

843-}

852-}

844rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

853rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

845−rewriteTerm syn = do reserved "rewrite"

854+rewriteTerm syn = do kw <- reservedFC "rewrite"

846 fc <- getFC

855 fc <- getFC

847 prf <- expr syn

856 prf <- expr syn

848 giving <- optional (do symbol "==>"; expr' syn)

857 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

850 return (PRewrite fc

861 return (PRewrite fc

851 (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

862 (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

852 giving)

863 giving)

@@ -864,9 +875,10 @@ TypeSig' ::=

864@

875@

865 -}

876 -}

866let_ :: SyntaxInfo -> IdrisParser PTerm

877let_ :: SyntaxInfo -> IdrisParser PTerm

867−let_ syn = try (do reserved "let"

878+let_ syn = try (do kw <- reservedFC "let"

868 ls <- indentedBlock (let_binding syn)

879 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

870 return (buildLets ls sc))

882 return (buildLets ls sc))

871 <?> "let binding"

883 <?> "let binding"

872 where buildLets [] sc = sc

884 where buildLets [] sc = sc

@@ -911,12 +923,13 @@ QuoteGoal ::=

911@

923@

912 -}

924 -}

913quoteGoal :: SyntaxInfo -> IdrisParser PTerm

925quoteGoal :: SyntaxInfo -> IdrisParser PTerm

914−quoteGoal syn = do reserved "quoteGoal"; n <- fst <$> name;

926+quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;

915− reserved "by"

927+ kw2 <- reservedFC "by"

916 r <- expr syn

928 r <- expr syn

917− reserved "in"

929+ kw3 <- reservedFC "in"

918 fc <- getFC

930 fc <- getFC

919 sc <- expr syn

931 sc <- expr syn

932+ mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]

920 return (PGoal fc r n sc)

933 return (PGoal fc r n sc)

921 <?> "quote goal expression"

934 <?> "quote goal expression"

922

935

@@ -948,17 +961,18 @@ explicitPi opts st syn

948 return (bindList (PPi binder) xt sc)

961 return (bindList (PPi binder) xt sc)

949

962

950autoImplicit opts st syn

963autoImplicit opts st syn

951− = do reserved "auto"

964+ = do kw <- reservedFC "auto"

952 when (st == Static) $ fail "auto implicits can not be static"

965 when (st == Static) $ fail "auto implicits can not be static"

953 xt <- typeDeclList syn

966 xt <- typeDeclList syn

954 lchar '}'

967 lchar '}'

955 symbol "->"

968 symbol "->"

956 sc <- expr syn

969 sc <- expr syn

970+ highlightP kw AnnKeyword

957 return (bindList (PPi

971 return (bindList (PPi

958 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)

972 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing []]))) xt sc)

959

973

960defaultImplicit opts st syn = do

974defaultImplicit opts st syn = do

961− reserved "default"

975+ kw <- reservedFC "default"

962 when (st == Static) $ fail "default implicits can not be static"

976 when (st == Static) $ fail "default implicits can not be static"

963 ist <- get

977 ist <- get

964 script' <- simpleExpr syn

978 script' <- simpleExpr syn

@@ -967,6 +981,7 @@ defaultImplicit opts st syn = do

967 lchar '}'

981 lchar '}'

968 symbol "->"

982 symbol "->"

969 sc <- expr syn

983 sc <- expr syn

984+ highlightP kw AnnKeyword

970 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

985 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)

971

986

972normalImplicit opts st syn = do

987normalImplicit opts st syn = do

@@ -1159,8 +1174,9 @@ DoBlock ::=

1159 -}

1174 -}

1160doBlock :: SyntaxInfo -> IdrisParser PTerm

1175doBlock :: SyntaxInfo -> IdrisParser PTerm

1161doBlock syn

1176doBlock syn

1162− = do reserved "do"

1177+ = do kw <- reservedFC "do"

1163 ds <- indentedBlock1 (do_ syn)

1178 ds <- indentedBlock1 (do_ syn)

1179+ highlightP kw AnnKeyword

1164 return (PDoBlock ds)

1180 return (PDoBlock ds)

1165 <?> "do block"

1181 <?> "do block"

1166

1182

@@ -1177,19 +1193,21 @@ Do ::=

1177-}

1193-}

1178do_ :: SyntaxInfo -> IdrisParser PDo

1194do_ :: SyntaxInfo -> IdrisParser PDo

1179do_ syn

1195do_ syn

1180− = try (do reserved "let"

1196+ = try (do kw <- reservedFC "let"

1181 (i, ifc) <- name

1197 (i, ifc) <- name

1182 ty <- option Placeholder (do lchar ':'

1198 ty <- option Placeholder (do lchar ':'

1183 expr' syn)

1199 expr' syn)

1184 reservedOp "="

1200 reservedOp "="

1185 fc <- getFC

1201 fc <- getFC

1186 e <- expr syn

1202 e <- expr syn

1203+ highlightP kw AnnKeyword

1187 return (DoLet fc i ifc ty e))

1204 return (DoLet fc i ifc ty e))

1188− <|> try (do reserved "let"

1205+ <|> try (do kw <- reservedFC "let"

1189 i <- expr' syn

1206 i <- expr' syn

1190 reservedOp "="

1207 reservedOp "="

1191 fc <- getFC

1208 fc <- getFC

1192 sc <- expr syn

1209 sc <- expr syn

1210+ highlightP kw AnnKeyword

1193 return (DoLetP fc i sc))

1211 return (DoLetP fc i sc))

1194 <|> try (do (i, ifc) <- name

1212 <|> try (do (i, ifc) <- name

1195 symbol "<-"

1213 symbol "<-"