4297500 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Highlight all keywords with the parser

4297500David Raymond Christiansen11 years ago

src/Idris/ParseData.hs+12−11

compare with master

unifiedsplit

@@ -57,7 +57,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

57 let tyn = expandNS syn tyn_in

58 let rsyn = syn { syn_namespace = show (nsroot tyn) :

59 syn_namespace syn }

60− params <- manyTill (recordParameter rsyn) (reserved "where")

60+ params <- manyTill (recordParameter rsyn) (reservedHL "where")

61 (fields, cname, cdoc) <- indentedBlockS $ recordBody rsyn tyn

62 case cname of

63 Just cn' -> accData acc tyn [fst cn']

@@ -107,7 +107,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

107 return (n, p, t, doc')

108

109 constructor :: IdrisParser (Name, FC)

110− constructor = (reserved "constructor") *> fnName

110+ constructor = (reservedHL "constructor") *> fnName

111

112

113 endPlicity :: Maybe Char -> IdrisParser Plicity

@@ -144,12 +144,12 @@ recordParameter syn =

144DataI ::= 'data' | 'codata';

145-}

146dataI :: IdrisParser DataOpts

147−dataI = do reserved "data"; return []

147+dataI = do reservedHL "data"; return []

148− <|> do reserved "codata"; return [Codata]

148+ <|> do reservedHL "codata"; return [Codata]

149

150recordI :: IdrisParser DataOpts

151−recordI = do reserved "record"; return []

151+recordI = do reservedHL "record"; return []

152− <|> do reserved "corecord"; return [Codata]

152+ <|> do reservedHL "corecord"; return [Codata]

153

154{- | Parses if a data should not have a default eliminator

155DefaultEliminator ::= 'noelim'?

@@ -197,7 +197,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

197 ty <- typeExpr (allowImp syn)

198 let tyn = expandNS syn tyn_in

199 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

200− reserved "where"

200+ reservedHL "where"

201 cons <- indentedBlock (constructor syn)

202 accData acc tyn (map (\ (_, _, n, _, _, _, _) -> n) cons)

203 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn nfc ty cons))) <|> (do

@@ -205,7 +205,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

205 let ty = bindArgs (map (const (PType fc)) args) (PType fc)

206 let tyn = expandNS syn tyn_in

207 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn nfc ty)) (do

208− try (lchar '=') <|> do reserved "where"

208+ try (lchar '=') <|> do reservedHL "where"

209 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

210 let n = show tyn_in ++ " "

211 let s = kw ++ n

@@ -276,7 +276,7 @@ simpleConstructor syn

276DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

277 -}

278dsl :: SyntaxInfo -> IdrisParser PDecl

279−dsl syn = do reserved "dsl"

279+dsl syn = do reservedHL "dsl"

280 n <- fst <$> fnName

281 bs <- indentedBlock (overload syn)

282 let dsl = mkDSL bs (dsl_info syn)

@@ -314,11 +314,12 @@ OverloadIdentifier ::= 'let' | Identifier;

314Overload ::= OverloadIdentifier '=' Expr;

315-}

316overload :: SyntaxInfo -> IdrisParser (String, PTerm)

317−overload syn = do o <- (fst <$> identifier) <|> do reserved "let"

317+overload syn = do (o, fc) <- identifier <|> do fc <- reservedFC "let"

318− return "let"

318+ return ("let", fc)

319 if o `notElem` overloadable

320 then fail $ show o ++ " is not an overloading"

321 else do

322+ highlightP fc AnnKeyword

322 lchar '='

323 lchar '='

323 t <- expr syn

324 t <- expr syn

324 return (o, t)

325 return (o, t)

src/Idris/ParseHelpers.hs+4

@@ -286,6 +286,10 @@ reservedFC str = do (FC file (l, c) _) <- getFC

286 Tok.reserve idrisStyle str

287 return $ FC file (l, c) (l, c + length str)

288

289+-- | Parse a reserved identfier, highlighting its span as a keyword

290+reservedHL :: String -> IdrisParser ()

291+reservedHL str = reservedFC str >>= flip highlightP AnnKeyword

292+

289-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

293-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

290-- | Parses a reserved operator

294-- | Parses a reserved operator

291reservedOp :: MonadicParsing m => String -> m ()

295reservedOp :: MonadicParsing m => String -> m ()

src/Idris/Parser.hs+60−55

@@ -98,8 +98,7 @@ import System.IO

98moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])

99moduleHeader = try (do docs <- optional docComment

100 noArgs docs

101− modFC <- reservedFC "module"

101+ reservedHL "module"

102− highlightP modFC AnnKeyword

103 (i, ifc) <- identifier

102 (i, ifc) <- identifier

104 option ';' (lchar ';')

103 option ';' (lchar ';')

105 let modName = moduleName i

104 let modName = moduleName i

@@ -131,10 +130,12 @@ data ImportInfo = ImportInfo { import_reexport :: Bool

131 -}

130 -}

132import_ :: IdrisParser ImportInfo

131import_ :: IdrisParser ImportInfo

133import_ = do fc <- getFC

132import_ = do fc <- getFC

134− reserved "import"

133+ reservedHL "import"

135− reexport <- option False (do reserved "public"; return True)

134+ reexport <- option False (do reservedHL "public"

135+ return True)

136 (id, idfc) <- identifier

137− newName <- optional (reserved "as" *> identifier)

137+ newName <- optional (do reservedHL "as"

138+ identifier)

138 option ';' (lchar ';')

139 option ';' (lchar ';')

139 return $ ImportInfo reexport (toPath id)

140 return $ ImportInfo reexport (toPath id)

140 (fmap (\(n, fc) -> (toPath n, fc)) newName)

141 (fmap (\(n, fc) -> (toPath n, fc)) newName)

@@ -286,9 +287,10 @@ syntaxRule :: SyntaxInfo -> IdrisParser Syntax

286syntaxRule syn

287syntaxRule syn

287 = do sty <- try (do

288 = do sty <- try (do

288 pushIndent

289 pushIndent

290+ sty <- option AnySyntax

289− sty <- option AnySyntax (do reserved "term"; return TermSyntax

291+ (do reservedHL "term"; return TermSyntax

290− <|> do reserved "pattern"; return PatternSyntax)

292+ <|> do reservedHL "pattern"; return PatternSyntax)

291− reserved "syntax"

293+ reservedHL "syntax"

292 return sty)

294 return sty)

293 syms <- some syntaxSym

295 syms <- some syntaxSym

294 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

296 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

@@ -482,31 +484,31 @@ NameTimesList ::=

482-- https://github.com/idris-lang/Idris-dev/issues/1574

484-- https://github.com/idris-lang/Idris-dev/issues/1574

483fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

485fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

484fnOpts opts

486fnOpts opts

485− = do reserved "total"; fnOpts (TotalFn : opts)

487+ = do reservedHL "total"; fnOpts (TotalFn : opts)

486− <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))

488+ <|> do reservedHL "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))

487− <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

489+ <|> do reservedHL "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

488− <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

490+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

489− fnOpts (CExport c : opts)

491+ fnOpts (CExport c : opts)

490− <|> do try (lchar '%' *> reserved "no_implicit");

492+ <|> do try (lchar '%' *> reserved "no_implicit");

491− fnOpts (NoImplicit : opts)

493+ fnOpts (NoImplicit : opts)

492− <|> do try (lchar '%' *> reserved "inline");

494+ <|> do try (lchar '%' *> reserved "inline");

493− fnOpts (Inlinable : opts)

495+ fnOpts (Inlinable : opts)

494− <|> do try (lchar '%' *> reserved "assert_total");

496+ <|> do try (lchar '%' *> reserved "assert_total");

495− fnOpts (AssertTotal : opts)

497+ fnOpts (AssertTotal : opts)

496− <|> do try (lchar '%' *> reserved "error_handler");

498+ <|> do try (lchar '%' *> reserved "error_handler");

497− fnOpts (ErrorHandler : opts)

499+ fnOpts (ErrorHandler : opts)

498− <|> do try (lchar '%' *> reserved "error_reverse");

500+ <|> do try (lchar '%' *> reserved "error_reverse");

499− fnOpts (ErrorReverse : opts)

501+ fnOpts (ErrorReverse : opts)

500− <|> do try (lchar '%' *> reserved "reflection");

502+ <|> do try (lchar '%' *> reserved "reflection");

501− fnOpts (Reflection : opts)

503+ fnOpts (Reflection : opts)

502− <|> do try (lchar '%' *> reserved "hint");

504+ <|> do try (lchar '%' *> reserved "hint");

503− fnOpts (AutoHint : opts)

505+ fnOpts (AutoHint : opts)

504− <|> do lchar '%'; reserved "specialise";

506+ <|> do lchar '%'; reserved "specialise";

505− lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

507+ lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

506− fnOpts (Specialise ns : opts)

508+ fnOpts (Specialise ns : opts)

507− <|> do reserved "implicit"; fnOpts (Implicit : opts)

509+ <|> do reservedHL "implicit"; fnOpts (Implicit : opts)

508− <|> return opts

510+ <|> return opts

509− <?> "function modifier"

511+ <?> "function modifier"

510 where nameTimes :: IdrisParser (Name, Maybe Int)

512 where nameTimes :: IdrisParser (Name, Maybe Int)

511 nameTimes = do n <- fst <$> fnName

513 nameTimes = do n <- fst <$> fnName

512 t <- option Nothing (do reds <- fmap fst natural

514 t <- option Nothing (do reds <- fmap fst natural

@@ -543,7 +545,7 @@ postulate syn = do (doc, ext)

543 addAcc n acc

545 addAcc n acc

544 return (PPostulate ext doc syn fc nfc opts' n ty)

546 return (PPostulate ext doc syn fc nfc opts' n ty)

545 <?> "postulate"

547 <?> "postulate"

546− where ppostDecl = do reserved "postulate"; return False

548+ where ppostDecl = do fc <- reservedHL "postulate"; return False

547 <|> do lchar '%'; reserved "extern"; return True

549 <|> do lchar '%'; reserved "extern"; return True

548{- | Parses a using declaration

550{- | Parses a using declaration

549

551

@@ -555,7 +557,8 @@ Using ::=

555 -}

557 -}

556using_ :: SyntaxInfo -> IdrisParser [PDecl]

558using_ :: SyntaxInfo -> IdrisParser [PDecl]

557using_ syn =

559using_ syn =

560+ do reservedHL "using"

558− do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'

561+ lchar '('; ns <- usingDeclList syn; lchar ')'

559 openBlock

562 openBlock

560 let uvars = using syn

563 let uvars = using syn

561 ds <- many (decl (syn { using = uvars ++ ns }))

564 ds <- many (decl (syn { using = uvars ++ ns }))

@@ -573,7 +576,7 @@ Params ::=

573 -}

576 -}

574params :: SyntaxInfo -> IdrisParser [PDecl]

577params :: SyntaxInfo -> IdrisParser [PDecl]

575params syn =

578params syn =

576− do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

579+ do reservedHL "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

577 let ns' = [(n, ty) | (n, _, ty) <- ns]

580 let ns' = [(n, ty) | (n, _, ty) <- ns]

578 openBlock

581 openBlock

579 let pvars = syn_params syn

582 let pvars = syn_params syn

@@ -593,7 +596,7 @@ Mutual ::=

593-}

596-}

594mutual :: SyntaxInfo -> IdrisParser [PDecl]

597mutual :: SyntaxInfo -> IdrisParser [PDecl]

595mutual syn =

598mutual syn =

596− do reserved "mutual"

599+ do reservedHL "mutual"

597 openBlock

600 openBlock

598 let pvars = syn_params syn

601 let pvars = syn_params syn

599 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

602 ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

@@ -612,7 +615,7 @@ Namespace ::=

612-}

615-}

613namespace :: SyntaxInfo -> IdrisParser [PDecl]

616namespace :: SyntaxInfo -> IdrisParser [PDecl]

614namespace syn =

617namespace syn =

615− do reserved "namespace"

618+ do reservedHL "namespace"

616 (n, nfc) <- identifier

619 (n, nfc) <- identifier

617 openBlock

620 openBlock

618 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })

621 ds <- some (decl syn { syn_namespace = n : syn_namespace syn })

@@ -627,7 +630,7 @@ namespace syn =

627@

630@

628-}

631-}

629instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

632instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

630−instanceBlock syn = do reserved "where"

633+instanceBlock syn = do reservedHL "where"

631 openBlock

634 openBlock

632 ds <- many (fnDecl syn)

635 ds <- many (fnDecl syn)

633 closeBlock

636 closeBlock

@@ -650,7 +653,7 @@ ClassBlock ::=

650@

653@

651-}

654-}

652classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

655classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

653−classBlock syn = do reserved "where"

656+classBlock syn = do reservedHL "where"

654 openBlock

657 openBlock

655 (cn, cd) <- option (Nothing, emptyDocstring) $

658 (cn, cd) <- option (Nothing, emptyDocstring) $

656 try (do (doc, _) <- option noDocs docComment

659 try (do (doc, _) <- option noDocs docComment

@@ -666,7 +669,7 @@ classBlock syn = do reserved "where"

666

669

667 where

670 where

668 constructor :: IdrisParser (Name, FC)

671 constructor :: IdrisParser (Name, FC)

669− constructor = reserved "constructor" *> fnName

672+ constructor = reservedHL "constructor" *> fnName

670

673

671 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

674 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

672 annotate syn ist = annotCode $ tryFullExpr syn ist

675 annotate syn ist = annotCode $ tryFullExpr syn ist

@@ -690,7 +693,7 @@ class_ :: SyntaxInfo -> IdrisParser [PDecl]

690class_ syn = do (doc, argDocs, acc)

693class_ syn = do (doc, argDocs, acc)

691 <- try (do (doc, argDocs) <- docstring syn

694 <- try (do (doc, argDocs) <- docstring syn

692 acc <- optional accessibility

695 acc <- optional accessibility

693− reserved "class"

696+ reservedHL "class"

694 return (doc, argDocs, acc))

697 return (doc, argDocs, acc))

695 fc <- getFC

698 fc <- getFC

696 cons <- constraintList syn

699 cons <- constraintList syn

@@ -728,7 +731,7 @@ InstanceName ::= '[' Name ']';

728-}

731-}

729instance_ :: SyntaxInfo -> IdrisParser [PDecl]

732instance_ :: SyntaxInfo -> IdrisParser [PDecl]

730instance_ syn = do (doc, argDocs)

733instance_ syn = do (doc, argDocs)

731− <- try (docstring syn <* reserved "instance")

734+ <- try (docstring syn <* reservedHL "instance")

732 fc <- getFC

735 fc <- getFC

733 en <- optional instanceName

736 en <- optional instanceName

734 cs <- constraintList syn

737 cs <- constraintList syn

@@ -829,7 +832,7 @@ CAF ::= 'let' FnName '=' Expr Terminator;

829@

832@

830-}

833-}

831caf :: SyntaxInfo -> IdrisParser PDecl

834caf :: SyntaxInfo -> IdrisParser PDecl

832−caf syn = do reserved "let"

835+caf syn = do reservedHL "let"

833 n_in <- fst <$> fnName; let n = expandNS syn n_in

836 n_in <- fst <$> fnName; let n = expandNS syn n_in

834 lchar '='

837 lchar '='

835 t <- expr syn

838 t <- expr syn

@@ -927,7 +930,7 @@ clause syn

927 return ([], [])]

930 return ([], [])]

928 return $ PClauseR fc wargs r wheres) <|> (do

931 return $ PClauseR fc wargs r wheres) <|> (do

929 popIndent

932 popIndent

930− reserved "with"

933+ reservedHL "with"

931 wval <- simpleExpr syn

934 wval <- simpleExpr syn

932 pn <- optProof

935 pn <- optProof

933 openBlock

936 openBlock

@@ -980,7 +983,7 @@ clause syn

980 put (ist { lastParse = Just n })

983 put (ist { lastParse = Just n })

981 return $ PClause fc n capp wargs rs wheres) <|> (do

984 return $ PClause fc n capp wargs rs wheres) <|> (do

982 popIndent

985 popIndent

983− reserved "with"

986+ reservedHL "with"

984 wval <- bracketed syn

987 wval <- bracketed syn

985 pn <- optProof

988 pn <- optProof

986 openBlock

989 openBlock

@@ -1012,7 +1015,7 @@ clause syn

1012 ist <- get

1015 ist <- get

1013 put (ist { lastParse = Just n })

1016 put (ist { lastParse = Just n })

1014 return $ PClause fc n capp wargs r wheres) <|> (do

1017 return $ PClause fc n capp wargs r wheres) <|> (do

1015− reserved "with"

1018+ reservedHL "with"

1016 ist <- get

1019 ist <- get

1017 put (ist { lastParse = Just n })

1020 put (ist { lastParse = Just n })

1018 wval <- bracketed syn

1021 wval <- bracketed syn

@@ -1025,7 +1028,7 @@ clause syn

1025 return $ PWith fc n capp wargs wval pn withs)

1028 return $ PWith fc n capp wargs wval pn withs)

1026 <?> "function clause"

1029 <?> "function clause"

1027 where

1030 where

1028− optProof = option Nothing (do reserved "proof"

1031+ optProof = option Nothing (do reservedHL "proof"

1029 n <- fnName

1032 n <- fnName

1030 return (Just n))

1033 return (Just n))

1031

1034

@@ -1060,7 +1063,7 @@ WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;

1060-}

1063-}

1061whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

1064whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])

1062whereBlock n syn

1065whereBlock n syn

1063− = do reserved "where"

1066+ = do reservedHL "where"

1064 ds <- indentedBlock1 (decl syn)

1067 ds <- indentedBlock1 (decl syn)

1065 let dns = concatMap (concatMap declared) ds

1068 let dns = concatMap (concatMap declared) ds

1066 return (concat ds, map (\x -> (x, decoration syn x)) dns)

1069 return (concat ds, map (\x -> (x, decoration syn x)) dns)

@@ -1176,8 +1179,8 @@ Totality ::= 'partial' | 'total'

1176-}

1179-}

1177totality :: IdrisParser Bool

1180totality :: IdrisParser Bool

1178totality

1181totality

1179− = do reserved "total"; return True

1182+ = do reservedHL "total"; return True

1180− <|> do reserved "partial"; return False

1183+ <|> do reservedHL "partial"; return False

1181

1184

1182{- | Parses a type provider

1185{- | Parses a type provider

1183

1186

@@ -1188,22 +1191,24 @@ ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1188 -}

1191 -}

1189provider :: SyntaxInfo -> IdrisParser [PDecl]

1192provider :: SyntaxInfo -> IdrisParser [PDecl]

1190provider syn = do doc <- try (do (doc, _) <- docstring syn

1193provider syn = do doc <- try (do (doc, _) <- docstring syn

1194+ fc1 <- getFC

1191 lchar '%'

1195 lchar '%'

1192− reserved "provide"

1196+ fc2 <- reservedFC "provide"

1197+ highlightP (spanFC fc1 fc2) AnnKeyword

1193 return doc)

1198 return doc)

1194 provideTerm doc <|> providePostulate doc

1199 provideTerm doc <|> providePostulate doc

1195 <?> "type provider"

1200 <?> "type provider"

1196 where provideTerm doc =

1201 where provideTerm doc =

1197 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1202 do lchar '('; (n, nfc) <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1198 fc <- getFC

1203 fc <- getFC

1199− reserved "with"

1204+ reservedHL "with"

1200 e <- expr syn <?> "provider expression"

1205 e <- expr syn <?> "provider expression"

1201 return [PProvider doc syn fc nfc (ProvTerm t e) n]

1206 return [PProvider doc syn fc nfc (ProvTerm t e) n]

1202 providePostulate doc =

1207 providePostulate doc =

1203− do reserved "postulate"

1208+ do reservedHL "postulate"

1204 (n, nfc) <- fnName

1209 (n, nfc) <- fnName

1205 fc <- getFC

1210 fc <- getFC

1206− reserved "with"

1211+ reservedHL "with"

1207 e <- expr syn <?> "provider expression"

1212 e <- expr syn <?> "provider expression"

1208 return [PProvider doc syn fc nfc (ProvPostulate e) n]

1213 return [PProvider doc syn fc nfc (ProvPostulate e) n]

1209

1214