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

src/Idris/AbsSyntax.hs+3−3

@@ -1028,12 +1028,12 @@ expandParams dec ps ns infs tm = en tm

10281028expandParamsD :: Bool -> -- True = RHS only

10291029 IState ->

10301030 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

1031−expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n ty)

1031+expandParamsD rhsonly ist dec ps ns (PTy doc argdocs syn fc o n nfc ty)

10321032 = if n `elem` ns && (not rhsonly)

10331033 then -- trace (show (n, expandParams dec ps ns ty)) $

1034− PTy doc argdocs syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

1034+ PTy doc argdocs syn fc o (dec n) nfc (piBindp expl_param ps (expandParams dec ps ns [] ty))

10351035 else --trace (show (n, expandParams dec ps ns ty)) $

1036− PTy doc argdocs syn fc o n (expandParams dec ps ns [] ty)

1036+ PTy doc argdocs syn fc o n nfc (expandParams dec ps ns [] ty)

10371037expandParamsD rhsonly ist dec ps ns (PPostulate e doc syn fc o n ty)

10381038 = if n `elem` ns && (not rhsonly)

10391039 then -- trace (show (n, expandParams dec ps ns ty)) $

src/Idris/AbsSyntaxTree.hs+5−5

@@ -593,7 +593,7 @@ type ProvideWhat = ProvideWhat' PTerm

593593-- datatypes and typeclasses.

594594data PDecl' t

595595 = PFix FC Fixity [String] -- ^ Fixity declaration

596− | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

596+ | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)

597597 | PPostulate Bool -- external def if true

598598 (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

599599 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

@@ -728,7 +728,7 @@ type PClause = PClause' PTerm

728728

729729declared :: PDecl -> [Name]

730730declared (PFix _ _ _) = []

731−declared (PTy _ _ _ _ _ n t) = [n]

731+declared (PTy _ _ _ _ _ n fc t) = [n]

732732declared (PPostulate _ _ _ _ _ n t) = [n]

733733declared (PClauses _ _ n _) = [] -- not a declaration

734734declared (PCAF _ n _) = [n]

@@ -749,7 +749,7 @@ declared _ = []

749749-- get the names declared, not counting nested parameter blocks

750750tldeclared :: PDecl -> [Name]

751751tldeclared (PFix _ _ _) = []

752−tldeclared (PTy _ _ _ _ _ n t) = [n]

752+tldeclared (PTy _ _ _ _ _ n _ t) = [n]

753753tldeclared (PPostulate _ _ _ _ _ n t) = [n]

754754tldeclared (PClauses _ _ n _) = [] -- not a declaration

755755tldeclared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn

@@ -764,7 +764,7 @@ tldeclared _ = []

764764

765765defined :: PDecl -> [Name]

766766defined (PFix _ _ _) = []

767−defined (PTy _ _ _ _ _ n t) = []

767+defined (PTy _ _ _ _ _ n _ t) = []

768768defined (PPostulate _ _ _ _ _ n t) = []

769769defined (PClauses _ _ n _) = [n] -- not a declaration

770770defined (PCAF _ n _) = [n]

@@ -1780,7 +1780,7 @@ showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

17801780showDecls o ds = vsep (map (showDeclImp o) ds)

17811781

17821782showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1783−showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1783+showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

17841784showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

17851785 indent 2 (vsep (map (showCImp o) cs))

17861786showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

src/Idris/DeepSeq.hs+4−2

@@ -129,10 +129,12 @@ instance NFData DataOpt where

129129

130130instance (NFData t) => NFData (PDecl' t) where

131131 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

132− rnf (PTy x1 x2 x3 x4 x5 x6 x7)

132+ rnf (PTy x1 x2 x3 x4 x5 x6 x7 x8)

133133 = rnf x1 `seq`

134134 rnf x2 `seq`

135− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

135+ rnf x3 `seq`

136+ rnf x4 `seq`

137+ rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

136138 rnf (PPostulate x1 x2 x3 x4 x5 x6 x7)

137139 = rnf x1 `seq`

138140 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

src/Idris/Delaborate.hs+8−5

@@ -309,7 +309,7 @@ pprintErr' i (InvalidTCArg n t)

309309 <> annName n <$>

310310 text "(Type class arguments must be injective)"

311311pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

312− align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

312+ align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as)))

313313pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

314314pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

315315pprintErr' i (WithFnType ty) =

@@ -558,8 +558,9 @@ annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

558558annTm :: Term -> Doc OutputAnnotation -> Doc OutputAnnotation

559559annTm tm = annotate (AnnTerm [] tm)

560560

561−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

562−fancifyAnnots ist annot@(AnnName n _ _ _) =

561+-- | Add extra metadata to an output annotation, optionally marking metavariables.

562+fancifyAnnots :: IState -> Bool -> OutputAnnotation -> OutputAnnotation

563+fancifyAnnots ist meta annot@(AnnName n _ _ _) =

563564 do let ctxt = tt_ctxt ist

564565 docs = docOverview ist n

565566 ty = Just (getTy ist n)

@@ -567,7 +568,9 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

567568 _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

568569 _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

569570 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

570− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

571+ _ | isMetavarName n ist -> if meta

572+ then AnnName n (Just MetavarOutput) docs ty

573+ else AnnName n (Just FunOutput) docs ty

571574 _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

572575 _ | otherwise -> annot

573576 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

@@ -585,7 +588,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

585588 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

586589 delabTy ist n

587590 in (displayS . renderPretty 1.0 50 $ theTy) ""

588−fancifyAnnots _ annot = annot

591+fancifyAnnots _ _ annot = annot

589592

590593showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

591594showSc i [] = empty

src/Idris/Elab/Class.hs+6−6

@@ -140,8 +140,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

140140 conbind ((c, ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)

141141 conbind [] x = x

142142

143− getMName (PTy _ _ _ _ _ n _) = nsroot n

144− tdecl allmeths (PTy doc _ syn _ o n t)

143+ getMName (PTy _ _ _ _ _ n nfc _) = nsroot n

144+ tdecl allmeths (PTy doc _ syn _ o n nfc t)

145145 = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

146146 logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

147147 return ( (n, (toExp (map fst ps) Exp t')),

@@ -155,7 +155,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

155155 case lookup n mtys of

156156 Just (syn, o, ty) -> do let ty' = insertConstraint c ty

157157 let ds = map (decorateid defaultdec)

158− [PTy emptyDocstring [] syn fc [] n ty',

158+ [PTy emptyDocstring [] syn fc [] n NoFC ty',

159159 PClauses fc (o ++ opts) n cs]

160160 iLOG (show ds)

161161 return (n, ((defaultdec n, ds!!1), ds))

@@ -165,7 +165,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

165165 defaultdec (UN n) = sUN ("default#" ++ str n)

166166 defaultdec (NS n ns) = NS (defaultdec n) ns

167167

168− tydecl (PTy _ _ _ _ _ _ _) = True

168+ tydecl (PTy _ _ _ _ _ _ _ _) = True

169169 tydecl _ = False

170170 instdecl (PInstance _ _ _ _ _ _ _ _ _ _) = True

171171 instdecl _ = False

@@ -194,7 +194,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

194194 addInstance False conn' cfn

195195 addIBC (IBCInstance False conn' cfn)

196196-- iputStrLn ("Added " ++ show (conn, cfn, ty))

197− return [PTy emptyDocstring [] syn fc [] cfn ty,

197+ return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

198198 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

199199

200200 -- Generate a top level function which looks up a method in a given

@@ -210,7 +210,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

210210 logLvl 2 ("Top level type: " ++ showTmImpls ty')

211211 iLOG (show (m, ty', capp, margs))

212212 logLvl 2 ("Definition: " ++ showTmImpls lhs ++ " = " ++ showTmImpls rhs)

213− return [PTy doc [] syn fc o m ty',

213+ return [PTy doc [] syn fc o m NoFC ty',

214214 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

215215

216216 getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc

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

@@ -374,7 +374,7 @@ elabPE info fc caller r =

374374 logLvl 2 $ show n ++ " transformation rule: " ++

375375 show rhs ++ " ==> " ++ show lhs

376376

377− elabType info defaultSyntax emptyDocstring [] fc opts newnm specTy

377+ elabType info defaultSyntax emptyDocstring [] fc opts newnm NoFC specTy

378378 let def = map (\(lhs, rhs) ->

379379 PClause fc newnm lhs [] rhs [])

380380 (pe_clauses specdecl)

@@ -732,7 +732,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

732732-- = NS (UN ('#':show x)) [show cnum, show fname]

733733

734734 sepBlocks bs = sepBlocks' [] bs where

735− sepBlocks' ns (d@(PTy _ _ _ _ _ n t) : bs)

735+ sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)

736736 = let (bf, af) = sepBlocks' (n : ns) bs in

737737 (d : bf, af)

738738 sepBlocks' ns (d@(PClauses _ _ n _) : bs)

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

@@ -321,7 +321,7 @@ elabCaseFun ind paramPos n ty cons info = do

321321 let motiveConstr = [(motiveName, expl, motive)]

322322 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

323323 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

324− let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

324+ let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy

325325 let clauseConsElimArgs = map getPiName consTerms

326326 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

327327 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

src/Idris/Elab/Instance.hs+3−3

@@ -71,7 +71,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

7171 let iname = mkiname n (namespace info) ps expn

7272 let emptyclass = null (class_methods ci)

7373 when (what /= EDefns || (null ds && not emptyclass)) $ do

74− nty <- elabType' True info syn doc argDocs fc [] iname t

74+ nty <- elabType' True info syn doc argDocs fc [] iname NoFC t

7575 -- if the instance type matches any of the instances we have already,

7676 -- and it's not a named instance, then it's overlapping, so report an error

7777 case expn of

@@ -245,8 +245,8 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

245245 decorate ns iname (UN n) = NS (SN (MethodN (UN n))) ns

246246 decorate ns iname (NS (UN n) s) = NS (SN (MethodN (UN n))) ns

247247

248− mkTyDecl (n, op, t, _)

249− = PTy emptyDocstring [] syn fc op n

248+ mkTyDecl (n, op, t, _)

249+ = PTy emptyDocstring [] syn fc op n NoFC

250250 (mkUniqueNames [] t)

251251

252252 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

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

@@ -93,7 +93,7 @@ elabProvider doc info syn fc what n

9393 Provide tm

9494 | ProvTerm ty _ <- what ->

9595 do -- Finally add a top-level definition of the provided term

96− elabType info syn doc [] fc [] n ty

96+ elabType info syn doc [] fc [] n NoFC ty

9797 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

9898 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

9999 | ProvPostulate _ <- what ->

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

@@ -313,7 +313,8 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f

313313 where

314314 -- | The type of the projection function.

315315 generateTy :: PDecl

316− generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName NoFC targetTy projTy

316+ generateTy = PTy pdoc [] psyn fc [] pname NoFC $

317+ PPi expl recName NoFC targetTy projTy

317318

318319 -- | The left hand side of the projection function.

319320 generateLhs :: PTerm

@@ -375,7 +376,9 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

375376 where

376377 -- | The type of the update function.

377378 generateTy :: PDecl

378− generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) NoFC pty (PPi expl recName NoFC sty (substInput sty))

379+ generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

380+ PPi expl (nsroot pname) NoFC pty $

381+ PPi expl recName NoFC sty (substInput sty)

379382 where substInput = substMatches [(cname, PRef fc (nsroot pname))]

380383

381384 -- | The "_set" name.

src/Idris/Elab/Type.hs+8−5

@@ -120,14 +120,15 @@ buildType info syn fc opts n ty' = do

120120-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

121121elabType :: ElabInfo -> SyntaxInfo

122122 -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))]

123− -> FC -> FnOpts -> Name -> PTerm -> Idris Type

123+ -> FC -> FnOpts -> Name -> FC -- ^ The precise location of the name

124+ -> PTerm -> Idris Type

124125elabType = elabType' False

125126

126127elabType' :: Bool -> -- normalise it

127128 ElabInfo -> SyntaxInfo ->

128129 Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

129− FC -> FnOpts -> Name -> PTerm -> Idris Type

130−elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

130+ FC -> FnOpts -> Name -> FC -> PTerm -> Idris Type

131+elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (params info) ty_in

131132 n = liftname info n_in in -}

132133 do checkUndefined fc n

133134 (cty, _, ty, inacc) <- buildType info syn fc opts n ty'

@@ -192,6 +193,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

192193 addIBC (IBCErrorHandler n)

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

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

196+ -- Send highlighting information about the name being declared

197+ sendHighlighting [(nfc, AnnName n Nothing Nothing Nothing)]

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

196199 case (unApply usety) of

197200 (P _ ut _, _)

@@ -229,7 +232,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

229232elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

230233 FC -> FnOpts -> Name -> PTerm -> Idris ()

231234elabPostulate info syn doc fc opts n ty = do

232− elabType info syn doc [] fc opts n ty

235+ elabType info syn doc [] fc opts n NoFC ty

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

234237 addIBC (IBCPostulate n)

235238

@@ -239,7 +242,7 @@ elabPostulate info syn doc fc opts n ty = do

239242elabExtern :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

240243 FC -> FnOpts -> Name -> PTerm -> Idris ()

241244elabExtern info syn doc fc opts n ty = do

242− cty <- elabType info syn doc [] fc opts n ty

245+ cty <- elabType info syn doc [] fc opts n NoFC ty

243246 ist <- getIState

244247 let arity = length (getArgTys (normalise (tt_ctxt ist) [] cty))

245248

src/Idris/Elab/Utils.hs+3−3

@@ -124,7 +124,7 @@ checkDocs fc args tm = cd (Map.fromList args) tm

124124 ++ (concat . intersperse ", " . map show . Map.keys) as

125125 ++ " but they were not found."

126126

127−decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorate n) t

127+decorateid decorate (PTy doc argdocs s f o n nfc t) = PTy doc argdocs s f o (decorate n) nfc t

128128decorateid decorate (PClauses f o n cs)

129129 = PClauses f o (decorate n) (map dc cs)

130130 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

@@ -272,8 +272,8 @@ getStatics ns (Bind n (Pi _ _ _) t)

272272getStatics _ _ = []

273273

274274mkStatic :: [Name] -> PDecl -> PDecl

275−mkStatic ns (PTy doc argdocs syn fc o n ty)

276− = PTy doc argdocs syn fc o n (mkStaticTy ns ty)

275+mkStatic ns (PTy doc argdocs syn fc o n nfc ty)

276+ = PTy doc argdocs syn fc o n nfc (mkStaticTy ns ty)

277277mkStatic ns t = t

278278

279279mkStaticTy :: [Name] -> PTerm -> PTerm

src/Idris/ElabDecls.hs+2−2

@@ -156,10 +156,10 @@ elabDecl' _ info (PFix _ _ _)

156156 = return () -- nothing to elaborate

157157elabDecl' _ info (PSyntax _ p)

158158 = return () -- nothing to elaborate

159−elabDecl' what info (PTy doc argdocs s f o n ty)

159+elabDecl' what info (PTy doc argdocs s f o n nfc ty)

160160 | what /= EDefns

161161 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

162− elabType info s doc argdocs f o n ty

162+ elabType info s doc argdocs f o n nfc ty

163163 return ()

164164elabDecl' what info (PPostulate b doc s f o n ty)

165165 | what /= EDefns

src/Idris/IBC.hs+4−2

@@ -1144,7 +1144,7 @@ instance (Binary t) => Binary (PDecl' t) where

11441144 put x1

11451145 put x2

11461146 put x3

1147− PTy x1 x2 x3 x4 x5 x6 x7

1147+ PTy x1 x2 x3 x4 x5 x6 x7 x8

11481148 -> do putWord8 1

11491149 put x1

11501150 put x2

@@ -1153,6 +1153,7 @@ instance (Binary t) => Binary (PDecl' t) where

11531153 put x5

11541154 put x6

11551155 put x7

1156+ put x8

11561157 PClauses x1 x2 x3 x4 -> do putWord8 2

11571158 put x1

11581159 put x2

@@ -1258,7 +1259,8 @@ instance (Binary t) => Binary (PDecl' t) where

12581259 x5 <- get

12591260 x6 <- get

12601261 x7 <- get

1261− return (PTy x1 x2 x3 x4 x5 x6 x7)

1262+ x8 <- get

1263+ return (PTy x1 x2 x3 x4 x5 x6 x7 x8)

12621264 2 -> do x1 <- get

12631265 x2 <- get

12641266 x3 <- get

src/Idris/Output.hs+8−8

@@ -33,20 +33,20 @@ instance MonadException m => MonadException (ExceptT Err m) where

3333pshow :: IState -> Err -> String

3434pshow ist err = displayDecorated (consoleDecorate ist) .

3535 renderPretty 1.0 80 .

36− fmap (fancifyAnnots ist) $ pprintErr ist err

36+ fmap (fancifyAnnots ist True) $ pprintErr ist err

3737

3838iWarn :: FC -> Doc OutputAnnotation -> Idris ()

3939iWarn fc err =

4040 do i <- getIState

4141 case idris_outputmode i of

4242 RawOutput h ->

43− do err' <- iRender . fmap (fancifyAnnots i) $

43+ do err' <- iRender . fmap (fancifyAnnots i True) $

4444 case fc of

4545 FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err

4646 _ -> err

4747 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

4848 IdeMode n h ->

49− do err' <- iRender . fmap (fancifyAnnots i) $ err

49+ do err' <- iRender . fmap (fancifyAnnots i True) $ err

5050 let (str, spans) = displaySpans err'

5151 runIO . hPutStrLn h $

5252 convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

@@ -97,7 +97,7 @@ iRenderOutput doc =

9797 RawOutput h -> do out <- iRender doc

9898 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

9999 IdeMode n h ->

100− do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

100+ do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i True) $ doc

101101 let out = [toSExp str, toSExp spans]

102102 runIO . hPutStrLn h $ convSExp "write-decorated" out n

103103

@@ -112,7 +112,7 @@ ideModeReturnWithStatus status n h out = do

112112 ist <- getIState

113113 (str, spans) <- fmap displaySpans .

114114 iRender .

115− fmap (fancifyAnnots ist) $

115+ fmap (fancifyAnnots ist True) $

116116 out

117117 let good = [SymbolAtom status, toSExp str, toSExp spans]

118118 runIO . hPutStrLn h $ convSExp "return" good n

@@ -168,7 +168,7 @@ iputGoal g = do i <- getIState

168168 case idris_outputmode i of

169169 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)

170170 IdeMode n h ->

171− let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g

171+ let (str, spans) = displaySpans . fmap (fancifyAnnots i True) $ g

172172 goal = [toSExp str, toSExp spans]

173173 in runIO . hPutStrLn h $ convSExp "write-goal" goal n

174174

@@ -201,7 +201,7 @@ sendHighlighting highlights =

201201 case idris_outputmode ist of

202202 RawOutput _ -> return ()

203203 IdeMode n h ->

204− let fancier = [toSExp (fc, fancifyAnnots ist annot) | (fc, annot) <- highlights]

204+ let fancier = [toSExp (fc, fancifyAnnots ist False annot) | (fc, annot) <- highlights]

205205 in runIO . hPutStrLn h $

206206 convSExp "output"

207207 (SymbolAtom "ok",

@@ -217,7 +217,7 @@ renderExternal fmt width doc

217217 return . wrap fmt .

218218 displayDecorated (decorate fmt) .

219219 renderPretty 1.0 width .

220− fmap (fancifyAnnots ist) $

220+ fmap (fancifyAnnots ist True) $

221221 doc

222222 where

223223 decorate _ (AnnFC _) = id

src/Idris/Parser.hs+6−5

@@ -392,7 +392,7 @@ fnDecl syn = try (do notEndBlock

392392-}

393393fnDecl' :: SyntaxInfo -> IdrisParser PDecl

394394fnDecl' syn = checkFixity $

395− do (doc, argDocs, fc, opts', n, acc) <- try (do

395+ do (doc, argDocs, fc, opts', n, nfc, acc) <- try (do

396396 pushIndent

397397 (doc, argDocs) <- docstring syn

398398 ist <- get

@@ -402,15 +402,15 @@ fnDecl' syn = checkFixity $

402402 opts <- fnOpts initOpts

403403 acc <- optional accessibility

404404 opts' <- fnOpts opts

405− n_in <- fst <$> fnName

405+ (n_in, nfc) <- fnName

406406 let n = expandNS syn n_in

407407 fc <- getFC

408408 lchar ':'

409− return (doc, argDocs, fc, opts', n, acc))

409+ return (doc, argDocs, fc, opts', n, nfc, acc))

410410 ty <- typeExpr (allowImp syn)

411411 terminator

412412 addAcc n acc

413− return (PTy doc argDocs syn fc opts' n ty)

413+ return (PTy doc argDocs syn fc opts' n nfc ty)

414414 <|> postulate syn

415415 <|> caf syn

416416 <|> pattern syn

@@ -423,7 +423,7 @@ fnDecl' syn = checkFixity $

423423 unless fOk . fail $

424424 "Missing fixity declaration for " ++ show n

425425 return decl

426− getName (PTy _ _ _ _ _ n _) = Just n

426+ getName (PTy _ _ _ _ _ n _ _) = Just n

427427 getName _ = Nothing

428428 fixityOK (NS n _) = fixityOK n

429429 fixityOK (UN n) | all (flip elem opChars) (str n) =

@@ -437,6 +437,7 @@ fnDecl' syn = checkFixity $

437437@

438438FnOpts ::= 'total'

439439 | 'partial'

440+ | 'covering'

440441 | 'implicit'

441442 | '%' 'no_implicit'

442443 | '%' 'assert_total'

src/Idris/REPL.hs+11−11

@@ -438,7 +438,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

438438 in

439439 displaySpans .

440440 renderPretty 0.9 cols .

441− fmap (fancifyAnnots ist) .

441+ fmap (fancifyAnnots ist True) .

442442 annotate (AnnTerm (zip bnd (take (length bnd) (repeat False))) t) $

443443 prettyT

444444

@@ -463,7 +463,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =

463463 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

464464 where pn ist = displaySpans .

465465 renderPretty 0.9 1000 .

466− fmap (fancifyAnnots ist) .

466+ fmap (fancifyAnnots ist True) .

467467 prettyName True True []

468468

469469runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

@@ -476,7 +476,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

476476 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

477477 where pn ist = displaySpans .

478478 renderPretty 0.9 1000 .

479− fmap (fancifyAnnots ist) .

479+ fmap (fancifyAnnots ist True) .

480480 prettyName True True []

481481

482482runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =

@@ -491,7 +491,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.BrowseNS ns) =

491491 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

492492 where pn ist = displaySpans .

493493 renderPretty 0.9 1000 .

494− fmap (fancifyAnnots ist) .

494+ fmap (fancifyAnnots ist True) .

495495 prettyName True True []

496496runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

497497 do ctxt <- getContext

@@ -506,7 +506,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

506506 msg = (IdeMode.SymbolAtom "ok",

507507 displaySpans .

508508 renderPretty 0.9 80 .

509− fmap (fancifyAnnots ist) $ ptm)

509+ fmap (fancifyAnnots ist True) $ ptm)

510510 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

511511runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =

512512 ideModeForceTermImplicits h id bnd True tm

@@ -519,7 +519,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.TermElab bnd tm) =

519519 msg = (IdeMode.SymbolAtom "ok",

520520 displaySpans .

521521 renderPretty 0.9 70 .

522− fmap (fancifyAnnots ist) $ ptm)

522+ fmap (fancifyAnnots ist True) $ ptm)

523523 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

524524runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =

525525 case splitName name of

@@ -535,7 +535,7 @@ runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =

535535 let (out, spans) =

536536 displaySpans .

537537 renderPretty 0.9 80 .

538− fmap (fancifyAnnots ist) $ pprintErr ist e

538+ fmap (fancifyAnnots ist True) $ pprintErr ist e

539539 msg = (IdeMode.SymbolAtom "ok", out, spans)

540540 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

541541runIdeModeCommand h id orig fn modes IdeMode.GetIdrisVersion =

@@ -558,7 +558,7 @@ ideModeForceTermImplicits h id bnd impl tm =

558558 msg = (IdeMode.SymbolAtom "ok",

559559 displaySpans .

560560 renderPretty 0.9 80 .

561− fmap (fancifyAnnots ist) $ expl)

561+ fmap (fancifyAnnots ist True) $ expl)

562562 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

563563

564564splitName :: String -> Either String Name

@@ -788,7 +788,7 @@ process fn (NewDefn decls) = do

788788 mapM_ defineName namedGroups where

789789 namedGroups = groupBy (\d1 d2 -> getName d1 == getName d2) decls

790790 getName :: PDecl -> Maybe Name

791− getName (PTy docs argdocs syn fc opts name ty) = Just name

791+ getName (PTy docs argdocs syn fc opts name _ ty) = Just name

792792 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

793793 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

794794 getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

@@ -797,7 +797,7 @@ process fn (NewDefn decls) = do

797797 getClauseName (PClause fc name whole with rhs whereBlock) = name

798798 getClauseName (PWith fc name whole with rhs pn whereBlock) = name

799799 defineName :: [PDecl] -> Idris ()

800− defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

800+ defineName (tyDecl@(PTy docs argdocs syn fc opts name _ ty) : decls) = do

801801 elabDecl EAll recinfo tyDecl

802802 elabClauses recinfo fc opts name (concatMap getClauses decls)

803803 setReplDefined (Just name)

@@ -896,7 +896,7 @@ process fn (Check (PRef _ n))

896896 case lookupNames n ctxt of

897897 ts@(t:_) ->

898898 case lookup t (idris_metavars ist) of

899− Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist) $

899+ Just (_, i, _) -> iRenderResult . fmap (fancifyAnnots ist True) $

900900 showMetavarInfo ppo ist n i

901901 Nothing -> iPrintFunTypes [] n (map (\n -> (n, pprintDelabTy ist n)) ts)

902902 [] -> iPrintError $ "No such variable " ++ show n

src/Idris/TypeSearch.hs+1−1

@@ -47,7 +47,7 @@ searchByType pkgs pterm = do

4747 pterm' <- addUsingConstraints syn emptyFC pterm

4848 pterm'' <- implicit toplevel syn name pterm'

4949 let pterm''' = addImpl [] i pterm''

50− ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

50+ ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name NoFC pterm'

5151 let names = searchUsing searchPred i ty

5252 let names' = take numLimit names

5353 let docs =