193589f · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+6−6

compare with master

unifiedsplit

@@ -302,8 +302,8 @@ data IState = IState {

302

303 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)

304 , idris_exports :: [Name] -- ^ Functions with ExportList

305− , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output

305+ , idris_highlightedRegions :: S.Set (FC', OutputAnnotation) -- ^ Highlighting information to output

306− , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser

306+ , idris_parserHighlights :: S.Set (FC', OutputAnnotation) -- ^ Highlighting information from the parser

307 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation

308 , idris_inmodule :: S.Set Name -- ^ Names defined in current module

309 , idris_ttstats :: M.Map Term (Int, Term)

@@ -411,7 +411,7 @@ idrisInit = IState initContext S.empty []

411 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

412 [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []

413 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

414− AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []

414+ AutomaticWidth S.empty S.empty [] [] [] M.empty [] S.empty S.empty

415 emptyContext S.empty M.empty emptyContext initialInteractiveOpts

416

417

@@ -710,19 +710,19 @@ data EState = EState {

710 case_decls :: [(Name, PDecl)]

711 , delayed_elab :: [(Int, Elab' EState ())]

712 , new_tyDecls :: [RDeclInstructions]

713− , highlighting :: [(FC, OutputAnnotation)]

713+ , highlighting :: S.Set (FC', OutputAnnotation)

714 , auto_binds :: [Name] -- ^ names bound as auto implicits

715 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)

716 }

717

718initEState :: EState

719−initEState = EState [] [] [] [] [] []

719+initEState = EState [] [] [] S.empty [] []

720

721type ElabD a = Elab' EState a

722

723highlightSource :: FC -> OutputAnnotation -> ElabD ()

724highlightSource fc annot =

725− updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })

725+ updateAux (\aux -> aux { highlighting = S.insert (FC' fc, annot) (highlighting aux) })

726

727-- | One clause of a top-level definition. Term arguments to constructors are:

728--

src/Idris/Core/TT.hs+3−3

@@ -197,10 +197,10 @@ instance Show FC where

197 show (FileFC f) = f

198

199-- | Output annotation for pretty-printed name - decides colour

200−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Generic)

200+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Ord, Generic)

201

202-- | Text formatting output

203−data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Generic)

203+data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Ord, Generic)

204

205-- | Output annotations for pretty-printing

206data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

@@ -227,7 +227,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

227 | AnnQuasiquote

228 | AnnAntiquote

229 | AnnSyntax String -- ^ type of syntax element: backslash or braces etc.

230− deriving (Show, Eq, Generic)

230+ deriving (Show, Eq, Generic, Ord)

231

232-- | Used for error reflection

233data ErrorReportPart = TextPart String

src/Idris/Directives.hs+7−5

@@ -13,6 +13,8 @@ import Idris.Core.TT

13import Idris.Imports

14import Idris.Output (sendHighlighting)

15

16+import qualified Data.Set as S

17+

16import Util.DynamicLinker

18import Util.DynamicLinker

17

19

18-- | Run the action corresponding to a directive

20-- | Run the action corresponding to a directive

@@ -81,7 +83,7 @@ directiveAction (DNameHint ty tyFC ns) = do

81 ty' <- disambiguate ty

83 ty' <- disambiguate ty

82 mapM_ (addNameHint ty' . fst) ns

84 mapM_ (addNameHint ty' . fst) ns

83 mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns

85 mapM_ (\n -> addIBC (IBCNameHint (ty', fst n))) ns

84− sendHighlighting $ [(tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (fc, AnnBoundName n False)) ns

86+ sendHighlighting $ S.fromList $ [(FC' tyFC, AnnName ty' Nothing Nothing Nothing)] ++ map (\(n, fc) -> (FC' fc, AnnBoundName n False)) ns

85

87

86directiveAction (DErrorHandlers fn nfc arg afc ns) = do

88directiveAction (DErrorHandlers fn nfc arg afc ns) = do

87 fn' <- disambiguate fn

89 fn' <- disambiguate fn

@@ -90,10 +92,10 @@ directiveAction (DErrorHandlers fn nfc arg afc ns) = do

90 return (n', fc)) ns

92 return (n', fc)) ns

91 addFunctionErrorHandlers fn' arg (map fst ns')

93 addFunctionErrorHandlers fn' arg (map fst ns')

92 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'

94 mapM_ (addIBC . IBCFunctionErrorHandler fn' arg . fst) ns'

93− sendHighlighting $

95+ sendHighlighting $ S.fromList $

94− [ (nfc, AnnName fn' Nothing Nothing Nothing)

96+ [ (FC' nfc, AnnName fn' Nothing Nothing Nothing)

95− , (afc, AnnBoundName arg False)

97+ , (FC' afc, AnnBoundName arg False)

96− ] ++ map (\(n, fc) -> (fc, AnnName n Nothing Nothing Nothing)) ns'

98+ ] ++ map (\(n, fc) -> (FC' fc, AnnName n Nothing Nothing Nothing)) ns'

97

99

98directiveAction (DLanguage ext) = addLangExt ext

100directiveAction (DLanguage ext) = addLangExt ext

99

101

src/Idris/Elab/Clause.hs+2−1

@@ -44,6 +44,7 @@ import qualified Control.Monad.State.Lazy as LState

44import Control.Monad.State.Strict as State

45import Data.List

46import Data.Maybe

47+import qualified Data.Set as S

47import Data.Word

48import Data.Word

48import Debug.Trace

49import Debug.Trace

49import Numeric

50import Numeric

@@ -1028,7 +1029,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1028 Just (n, nfc) -> Just (uniqueName n (map fst bargs))

1029 Just (n, nfc) -> Just (uniqueName n (map fst bargs))

1029

1030

1030 -- Highlight explicit proofs

1031 -- Highlight explicit proofs

1031− sendHighlighting [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

1032+ sendHighlighting $ S.fromList [(FC' fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

1032

1033

1033 logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++

1034 logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++

1034 " depends on " ++ show pdeps ++ " from " ++ show pvars)

1035 " depends on " ++ show pdeps ++ " from " ++ show pvars)

src/Idris/Elab/Data.hs+4−3

@@ -37,6 +37,7 @@ import Data.Char (isLetter, toLower)

37import Data.List

38import qualified Data.Map as Map

39import Data.Maybe

40+import qualified Data.Set as S

40import qualified Data.Text as T

41import qualified Data.Text as T

41

42

42warnLC :: FC -> Name -> Idris ()

43warnLC :: FC -> Name -> Idris ()

@@ -53,7 +54,7 @@ elabData info syn doc argDocs fc opts (PLaterdecl n nfc t_in)

53

54

54 addIBC (IBCDef n)

55 addIBC (IBCDef n)

55 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

56 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

56− sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

57+ sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]

57

58

58elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

59elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

59 = do let codata = Codata `elem` opts

60 = do let codata = Codata `elem` opts

@@ -118,9 +119,9 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

118 when (n /= sUN "=") $

119 when (n /= sUN "=") $

119 elabRewriteLemma info n cty

120 elabRewriteLemma info n cty

120 -- Emit highlighting info

121 -- Emit highlighting info

121− sendHighlighting $ [(nfc, AnnName n Nothing Nothing Nothing)] ++

122+ sendHighlighting $ S.fromList $ [(FC' nfc, AnnName n Nothing Nothing Nothing)] ++

122 map (\(_, _, n, nfc, _, _, _) ->

123 map (\(_, _, n, nfc, _, _, _) ->

123− (nfc, AnnName n Nothing Nothing Nothing))

124+ (FC' nfc, AnnName n Nothing Nothing Nothing))

124 dcons

125 dcons

125 where

126 where

126 checkDefinedAs fc n t i

127 checkDefinedAs fc n t i

src/Idris/Elab/Interface.hs+6−5

@@ -26,6 +26,7 @@ import Control.Monad

26import Data.Generics.Uniplate.Data (transform)

27import Data.List

28import Data.Maybe

29+import qualified Data.Set as S

29

30

30data MArgTy = IA Name | EA Name | CA deriving Show

31data MArgTy = IA Name | EA Name | CA deriving Show

31

32

@@ -167,11 +168,11 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

167 mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

168 mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

168 addIBC (IBCInterface tn)

169 addIBC (IBCInterface tn)

169

170

170− sendHighlighting $

171+ sendHighlighting $ S.fromList $

171− [(tnfc, AnnName tn Nothing Nothing Nothing)] ++

172+ [(FC' tnfc, AnnName tn Nothing Nothing Nothing)] ++

172− [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

173+ [(FC' pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

173− [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

174+ [(FC' fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

174− maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

175+ maybe [] (\(conN, conNFC) -> [(FC' conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

175

176

176 where

177 where

177 info = info_in { noCaseLift = tn : noCaseLift info_in }

178 info = info_in { noCaseLift = tn : noCaseLift info_in }

src/Idris/Elab/Record.hs+5−4

@@ -20,6 +20,7 @@ import Idris.Output (sendHighlighting)

20import Control.Monad

21import Data.List

22import Data.Maybe

23+import qualified Data.Set as S

23

24

24-- | Elaborate a record declaration

25-- | Elaborate a record declaration

25elabRecord :: ElabInfo

26elabRecord :: ElabInfo

@@ -66,10 +67,10 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc

66 logElab 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

67 logElab 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

67 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

68 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

68

69

69− sendHighlighting $

70+ sendHighlighting $ S.fromList $

70− [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

71+ [(FC' nfc, AnnName tyn Nothing Nothing Nothing)] ++

71− maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

72+ maybe [] (\(_, cnfc) -> [(FC' cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

72− [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

73+ [(FC' ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

73

74

74 where

75 where

75 -- | Generates a type constructor.

76 -- | Generates a type constructor.

src/Idris/Elab/Term.hs+1−1

@@ -56,7 +56,7 @@ data ElabResult = ElabResult {

56 -- | Meta-info about the new type declarations

57 , resultTyDecls :: [RDeclInstructions]

58 -- | Saved highlights from elaboration

59− , resultHighlighting :: [(FC, OutputAnnotation)]

59+ , resultHighlighting :: S.Set (FC', OutputAnnotation)

60 -- | The new global name counter

61 , resultName :: Int

62 }

src/Idris/Elab/Type.hs+2−2

@@ -205,7 +205,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

205 else ifail $ "The type " ++ show nty' ++ " is invalid for an error handler"

206 else ifail "Error handlers can only be defined when the ErrorReflection language extension is enabled."

207 -- Send highlighting information about the name being declared

208− sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

208+ sendHighlighting $ S.fromList [(FC' nfc, AnnName n Nothing Nothing Nothing)]

209 -- if it's an export list type, make a note of it

210 case (unApply usety) of

211 (P _ ut _, _)

@@ -238,7 +238,7 @@ elabPostulate info syn doc fc nfc opts n ty = do

238 elabType info syn doc [] fc opts n NoFC ty

239 putIState . (\ist -> ist{ idris_postulates = S.insert n (idris_postulates ist) }) =<< getIState

240 addIBC (IBCPostulate n)

241− sendHighlighting [(nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]

241+ sendHighlighting $ S.fromList [(FC' nfc, AnnName n (Just PostulateOutput) Nothing Nothing)]

242

243 -- remove it from the deferred definitions list

244 solveDeferred fc n

src/Idris/Elab/Value.hs+1

@@ -26,6 +26,7 @@ import Prelude hiding (id, (.))

26

27import Control.Category

28import Data.Char (toLower)

29+import qualified Data.Set as S ()

29import qualified Data.Traversable as Traversable

30import qualified Data.Traversable as Traversable

30

31

31-- | Elaborate a value, returning any new bindings created (this will only

32-- | Elaborate a value, returning any new bindings created (this will only

src/Idris/ElabDecls.hs+3−1

@@ -41,8 +41,10 @@ import Control.Category

41import Control.Monad

42import Control.Monad.State.Strict as State

43import Data.Maybe

44+import qualified Data.Set as S

44import qualified Data.Text as T

45import qualified Data.Text as T

45

46

47+

46-- | Top level elaborator info, supporting recursive elaboration

48-- | Top level elaborator info, supporting recursive elaboration

47recinfo :: FC -> ElabInfo

49recinfo :: FC -> ElabInfo

48recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 [] id elabDecl'

50recinfo fc = EInfo [] emptyContext id [] (Just fc) (fc_fname fc) 0 [] id elabDecl'

@@ -260,7 +262,7 @@ elabDecl' what info (POpenInterfaces f ns ds)

260elabDecl' what info (PNamespace n nfc ps) =

262elabDecl' what info (PNamespace n nfc ps) =

261 do mapM_ (elabDecl' what ninfo) ps

263 do mapM_ (elabDecl' what ninfo) ps

262 let ns = reverse (map T.pack newNS)

264 let ns = reverse (map T.pack newNS)

263− sendHighlighting [(nfc, AnnNamespace ns Nothing)]

265+ sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns Nothing)]

264 where

266 where

265 newNS = n : namespace info

267 newNS = n : namespace info

266 ninfo = info { namespace = newNS }

268 ninfo = info { namespace = newNS }

src/Idris/Output.hs+13−12

@@ -38,8 +38,9 @@ import Prelude hiding ((<$>))

38

39import Control.Arrow (first)

40import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)

41−import Data.List (intersperse, nub, nubBy)

41+import Data.List (intersperse, nub)

42import Data.Maybe (fromJust, fromMaybe, isJust, listToMaybe)

43+import qualified Data.Set as S

43import System.Console.Haskeline.MonadException (MonadException(controlIO),

44import System.Console.Haskeline.MonadException (MonadException(controlIO),

44 RunIO(RunIO))

45 RunIO(RunIO))

45import System.FilePath (replaceExtension)

46import System.FilePath (replaceExtension)

@@ -77,9 +78,12 @@ formatMessage w = do

77 maybeSource <- case messageSource w of

78 maybeSource <- case messageSource w of

78 Just src -> pure (Just src)

79 Just src -> pure (Just src)

79 Nothing -> readSource fc

80 Nothing -> readSource fc

80− let maybeFormattedSource = maybeSource >>= layoutSource fc (idris_highlightedRegions i)

81+ let maybeFormattedSource = maybeSource >>= layoutSource fc (regions (idris_highlightedRegions i))

81 return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)

82 return $ layoutMessage (layoutFC fc) maybeFormattedSource (messageText w)

82 where

83 where

84+ regions :: S.Set (FC', OutputAnnotation) -> [(FC, OutputAnnotation)]

85+ regions rs = map (\(FC' a,b) -> (a, b)) $ S.toList rs

86+

83 fc :: FC

87 fc :: FC

84 fc = messageExtent w

88 fc = messageExtent w

85

89

@@ -359,23 +363,21 @@ prettyDocumentedIst ist (name, ty, docs) =

359sendParserHighlighting :: Idris ()

363sendParserHighlighting :: Idris ()

360sendParserHighlighting =

364sendParserHighlighting =

361 do ist <- getIState

365 do ist <- getIState

362− let hs = map unwrap . nub . map wrap $ idris_parserHighlights ist

366+ let hs = idris_parserHighlights ist

363 sendHighlighting hs

367 sendHighlighting hs

364 ist <- getIState

368 ist <- getIState

365− putIState ist {idris_parserHighlights = []}

369+ putIState ist {idris_parserHighlights = S.empty}

366− where wrap (fc, a) = (FC' fc, a)

367− unwrap (fc', a) = (unwrapFC fc', a)

368

370

369−sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

371+sendHighlighting :: S.Set (FC', OutputAnnotation) -> Idris ()

370sendHighlighting highlights =

372sendHighlighting highlights =

371 do ist <- getIState

373 do ist <- getIState

372 case idris_outputmode ist of

374 case idris_outputmode ist of

373 RawOutput _ -> updateIState $

375 RawOutput _ -> updateIState $

374 \ist -> ist { idris_highlightedRegions =

376 \ist -> ist { idris_highlightedRegions =

375− nubBy canNub $ highlights ++ idris_highlightedRegions ist }

377+ S.union highlights (idris_highlightedRegions ist) }

376 IdeMode n h ->

378 IdeMode n h ->

377 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)

379 let fancier = [ toSExp (fc, fancifyAnnots ist False annot)

378− | (fc, annot) <- nubBy canNub highlights, fullFC fc

380+ | (FC' fc, annot) <- S.toList highlights, fullFC fc

379 ] in

381 ] in

380 case fancier of

382 case fancier of

381 [] -> return ()

383 [] -> return ()

@@ -386,14 +388,13 @@ sendHighlighting highlights =

386

388

387 where fullFC (FC _ _ _) = True

389 where fullFC (FC _ _ _) = True

388 fullFC _ = False

390 fullFC _ = False

389− canNub (fA,x) (fB,y) = show fA == show fB && x == y

390

391

391-- | Write the highlighting information to a file, for use in external tools

392-- | Write the highlighting information to a file, for use in external tools

392-- or in editors that don't support the IDE protocol

393-- or in editors that don't support the IDE protocol

393writeHighlights :: FilePath -> Idris ()

394writeHighlights :: FilePath -> Idris ()

394writeHighlights f =

395writeHighlights f =

395 do ist <- getIState

396 do ist <- getIState

396− let hs = reverse $ idris_highlightedRegions ist

397+ let hs = reverse $ map (\(FC' a, b) -> (a,b)) $ S.toList (idris_highlightedRegions ist)

397 let hfile = replaceExtension f "idh"

398 let hfile = replaceExtension f "idh"

398 let annots = toSExp [ (fc, fancifyAnnots ist False annot)

399 let annots = toSExp [ (fc, fancifyAnnots ist False annot)

399 | (fc@(FC _ _ _), annot) <- hs

400 | (fc@(FC _ _ _), annot) <- hs

@@ -401,7 +402,7 @@ writeHighlights f =

401 runIO $ writeFile hfile $ sExpToString annots

402 runIO $ writeFile hfile $ sExpToString annots

402

403

403clearHighlights :: Idris ()

404clearHighlights :: Idris ()

404−clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = [] }

405+clearHighlights = updateIState $ \ist -> ist { idris_highlightedRegions = S.empty }

405

406

406renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

407renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

407renderExternal fmt width doc

408renderExternal fmt width doc

src/Idris/Parser.hs+6−5

@@ -53,6 +53,7 @@ import qualified Data.List.Split as Spl

53import qualified Data.Map as M

54import Data.Maybe

55import Data.Ord

56+import qualified Data.Set as S

56import qualified Data.Text as T

57import qualified Data.Text as T

57import qualified System.Directory as Dir (makeAbsolute)

58import qualified System.Directory as Dir (makeAbsolute)

58import System.FilePath

59import System.FilePath

@@ -1491,7 +1492,7 @@ parseImports fname input

1491 Right (x, annots, i) ->

1492 Right (x, annots, i) ->

1492 do putIState i

1493 do putIState i

1493 fname' <- runIO $ Dir.makeAbsolute fname

1494 fname' <- runIO $ Dir.makeAbsolute fname

1494− sendHighlighting $ addPath annots fname'

1495+ sendHighlighting $ S.fromList $ addPath annots fname'

1495 return x

1496 return x

1496 where imports :: IdrisParser ((Maybe (Docstring ()), [String],

1497 where imports :: IdrisParser ((Maybe (Docstring ()), [String],

1497 [ImportInfo],

1498 [ImportInfo],

@@ -1512,11 +1513,11 @@ parseImports fname input

1512 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

1513 let ps = ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp

1513 return ((mdoc, mname, ps, mrk'), annots, i)

1514 return ((mdoc, mname, ps, mrk'), annots, i)

1514

1515

1515− addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC, OutputAnnotation)]

1516+ addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC', OutputAnnotation)]

1516 addPath [] _ = []

1517 addPath [] _ = []

1517 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

1518 addPath ((fc, AnnNamespace ns Nothing) : annots) path =

1518− (fc, AnnNamespace ns (Just path)) : addPath annots path

1519+ (FC' fc, AnnNamespace ns (Just path)) : addPath annots path

1519− addPath (annot:annots) path = annot : addPath annots path

1520+ addPath ((fc,annot):annots) path = (FC' fc, annot) : addPath annots path

1520

1521

1521 shebang :: IdrisParser ()

1522 shebang :: IdrisParser ()

1522 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()

1523 shebang = string "#!" *> many (P.satisfy $ not . isEol) *> eol *> pure ()

@@ -1664,7 +1665,7 @@ loadSource lidr f toline

1664 srcFnAbs <- case srcFn of

1665 srcFnAbs <- case srcFn of

1665 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)

1666 Just fn -> fmap Just (runIO $ Dir.makeAbsolute fn)

1666 Nothing -> return Nothing

1667 Nothing -> return Nothing

1667− sendHighlighting [(nfc, AnnNamespace ns srcFnAbs)])

1668+ sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])

1668 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

1669 [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

1669 reportParserWarnings

1670 reportParserWarnings

1670 sendParserHighlighting

1671 sendParserHighlighting

src/Idris/Parser/Helpers.hs+2−1

@@ -89,6 +89,7 @@ import Data.List

89import qualified Data.List.NonEmpty as NonEmpty

90import qualified Data.Map as M

91import Data.Maybe

92+import qualified Data.Set as S

92import qualified Data.Text as T

93import qualified Data.Text as T

93import Text.Megaparsec ((<?>))

94import Text.Megaparsec ((<?>))

94import qualified Text.Megaparsec as P

95import qualified Text.Megaparsec as P

@@ -112,7 +113,7 @@ token p = trackExtent p <* whiteSpace

112highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a

113highlight :: (MonadState IState m, Parsing m) => OutputAnnotation -> m a -> m a

113highlight annot p = do

114highlight annot p = do

114 (result, fc) <- withExtent p

115 (result, fc) <- withExtent p

115− modify $ \ist -> ist { idris_parserHighlights = (fc, annot) : idris_parserHighlights ist }

116+ modify $ \ist -> ist { idris_parserHighlights = S.insert (FC' fc, annot) (idris_parserHighlights ist) }

116 return result

117 return result

117

118

118-- | Parse a reserved identfier, highlighting it as a keyword

119-- | Parse a reserved identfier, highlighting it as a keyword