7a2dc7b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2450 from david-christiansen/parser-hl-decls

Highlight all keywords with the parser

commit7a2dc7b150219b5d83aa39371af787f0c636f5cf authorDavid Christiansen <david@davidchristiansen.dk> dateMon 20 Jul 2015, 09:04 (11 years ago) parent00cffbd 4297500

3 files changed+76−66

compare with master

unifiedsplit

src/Idris/ParseData.hs+12−11 src/Idris/ParseHelpers.hs+4 src/Idris/Parser.hs+60−55

src/Idris/ParseData.hs+12−11

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

5757 let tyn = expandNS syn tyn_in

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

5959 syn_namespace syn }

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

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

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

6262 case cname of

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

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

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

108108

109109 constructor :: IdrisParser (Name, FC)

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

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

111111

112112

113113 endPlicity :: Maybe Char -> IdrisParser Plicity

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

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

145145-}

146146dataI :: IdrisParser DataOpts

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

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

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

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

149149

150150recordI :: IdrisParser DataOpts

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

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

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

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

153153

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

155155DefaultEliminator ::= 'noelim'?

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

197197 ty <- typeExpr (allowImp syn)

198198 let tyn = expandNS syn tyn_in

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

200− reserved "where"

200+ reservedHL "where"

201201 cons <- indentedBlock (constructor syn)

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

203203 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

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

206206 let tyn = expandNS syn tyn_in

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

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

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

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

210210 let n = show tyn_in ++ " "

211211 let s = kw ++ n

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

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

277277 -}

278278dsl :: SyntaxInfo -> IdrisParser PDecl

279−dsl syn = do reserved "dsl"

279+dsl syn = do reservedHL "dsl"

280280 n <- fst <$> fnName

281281 bs <- indentedBlock (overload syn)

282282 let dsl = mkDSL bs (dsl_info syn)

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

314314Overload ::= OverloadIdentifier '=' Expr;

315315-}

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

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

318− return "let"

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

318+ return ("let", fc)

319319 if o `notElem` overloadable

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

321321 else do

322+ highlightP fc AnnKeyword

322323 lchar '='

323324 t <- expr syn

324325 return (o, t)

src/Idris/ParseHelpers.hs+4

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

286286 Tok.reserve idrisStyle str

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

288288

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

290+reservedHL :: String -> IdrisParser ()

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

292+

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

290294-- | Parses a reserved operator

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

src/Idris/Parser.hs+60−55

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

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

9999moduleHeader = try (do docs <- optional docComment

100100 noArgs docs

101− modFC <- reservedFC "module"

102− highlightP modFC AnnKeyword

101+ reservedHL "module"

103102 (i, ifc) <- identifier

104103 option ';' (lchar ';')

105104 let modName = moduleName i

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

131130 -}

132131import_ :: IdrisParser ImportInfo

133132import_ = do fc <- getFC

134− reserved "import"

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

133+ reservedHL "import"

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

135+ return True)

136136 (id, idfc) <- identifier

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

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

138+ identifier)

138139 option ';' (lchar ';')

139140 return $ ImportInfo reexport (toPath id)

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

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

286287syntaxRule syn

287288 = do sty <- try (do

288289 pushIndent

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

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

291− reserved "syntax"

290+ sty <- option AnySyntax

291+ (do reservedHL "term"; return TermSyntax

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

293+ reservedHL "syntax"

292294 return sty)

293295 syms <- some syntaxSym

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

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

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

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

484486fnOpts opts

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

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

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

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

489− fnOpts (CExport c : opts)

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

491− fnOpts (NoImplicit : opts)

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

493− fnOpts (Inlinable : opts)

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

495− fnOpts (AssertTotal : opts)

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

497− fnOpts (ErrorHandler : opts)

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

499− fnOpts (ErrorReverse : opts)

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

501− fnOpts (Reflection : opts)

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

503− fnOpts (AutoHint : opts)

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

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

506− fnOpts (Specialise ns : opts)

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

508− <|> return opts

509− <?> "function modifier"

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

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

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

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

491+ fnOpts (CExport c : opts)

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

493+ fnOpts (NoImplicit : opts)

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

495+ fnOpts (Inlinable : opts)

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

497+ fnOpts (AssertTotal : opts)

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

499+ fnOpts (ErrorHandler : opts)

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

501+ fnOpts (ErrorReverse : opts)

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

503+ fnOpts (Reflection : opts)

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

505+ fnOpts (AutoHint : opts)

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

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

508+ fnOpts (Specialise ns : opts)

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

510+ <|> return opts

511+ <?> "function modifier"

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

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

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

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

543545 addAcc n acc

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

545547 <?> "postulate"

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

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

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

548550{- | Parses a using declaration

549551

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

555557 -}

556558using_ :: SyntaxInfo -> IdrisParser [PDecl]

557559using_ syn =

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

560+ do reservedHL "using"

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

559562 openBlock

560563 let uvars = using syn

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

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

573576 -}

574577params :: SyntaxInfo -> IdrisParser [PDecl]

575578params syn =

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

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

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

578581 openBlock

579582 let pvars = syn_params syn

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

593596-}

594597mutual :: SyntaxInfo -> IdrisParser [PDecl]

595598mutual syn =

596− do reserved "mutual"

599+ do reservedHL "mutual"

597600 openBlock

598601 let pvars = syn_params syn

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

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

612615-}

613616namespace :: SyntaxInfo -> IdrisParser [PDecl]

614617namespace syn =

615− do reserved "namespace"

618+ do reservedHL "namespace"

616619 (n, nfc) <- identifier

617620 openBlock

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

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

627630@

628631-}

629632instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

630−instanceBlock syn = do reserved "where"

633+instanceBlock syn = do reservedHL "where"

631634 openBlock

632635 ds <- many (fnDecl syn)

633636 closeBlock

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

650653@

651654-}

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

653−classBlock syn = do reserved "where"

656+classBlock syn = do reservedHL "where"

654657 openBlock

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

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

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

666669

667670 where

668671 constructor :: IdrisParser (Name, FC)

669− constructor = reserved "constructor" *> fnName

672+ constructor = reservedHL "constructor" *> fnName

670673

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

672675 annotate syn ist = annotCode $ tryFullExpr syn ist

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

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

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

692695 acc <- optional accessibility

693− reserved "class"

696+ reservedHL "class"

694697 return (doc, argDocs, acc))

695698 fc <- getFC

696699 cons <- constraintList syn

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

728731-}

729732instance_ :: SyntaxInfo -> IdrisParser [PDecl]

730733instance_ syn = do (doc, argDocs)

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

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

732735 fc <- getFC

733736 en <- optional instanceName

734737 cs <- constraintList syn

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

829832@

830833-}

831834caf :: SyntaxInfo -> IdrisParser PDecl

832−caf syn = do reserved "let"

835+caf syn = do reservedHL "let"

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

834837 lchar '='

835838 t <- expr syn

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

927930 return ([], [])]

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

929932 popIndent

930− reserved "with"

933+ reservedHL "with"

931934 wval <- simpleExpr syn

932935 pn <- optProof

933936 openBlock

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

980983 put (ist { lastParse = Just n })

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

982985 popIndent

983− reserved "with"

986+ reservedHL "with"

984987 wval <- bracketed syn

985988 pn <- optProof

986989 openBlock

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

10121015 ist <- get

10131016 put (ist { lastParse = Just n })

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

1015− reserved "with"

1018+ reservedHL "with"

10161019 ist <- get

10171020 put (ist { lastParse = Just n })

10181021 wval <- bracketed syn

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

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

10261029 <?> "function clause"

10271030 where

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

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

10291032 n <- fnName

10301033 return (Just n))

10311034

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

10601063-}

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

10621065whereBlock n syn

1063− = do reserved "where"

1066+ = do reservedHL "where"

10641067 ds <- indentedBlock1 (decl syn)

10651068 let dns = concatMap (concatMap declared) ds

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

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

11761179-}

11771180totality :: IdrisParser Bool

11781181totality

1179− = do reserved "total"; return True

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

1182+ = do reservedHL "total"; return True

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

11811184

11821185{- | Parses a type provider

11831186

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

11881191 -}

11891192provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1194+ fc1 <- getFC

11911195 lchar '%'

1192− reserved "provide"

1196+ fc2 <- reservedFC "provide"

1197+ highlightP (spanFC fc1 fc2) AnnKeyword

11931198 return doc)

11941199 provideTerm doc <|> providePostulate doc

11951200 <?> "type provider"

11961201 where provideTerm doc =

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

11981203 fc <- getFC

1199− reserved "with"

1204+ reservedHL "with"

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

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

12021207 providePostulate doc =

1203− do reserved "postulate"

1208+ do reservedHL "postulate"

12041209 (n, nfc) <- fnName

12051210 fc <- getFC

1206− reserved "with"

1211+ reservedHL "with"

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

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

12091214