git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1012 from david-christiansen/issue/949
1569aa9Edwin Brady
src/Idris/AbsSyntax.hs+11−4
compare with master
unifiedsplit
@@ -490,6 +490,12 @@ getUndefined :: Idris [Name]
490getUndefined = do i <- getIState
490getUndefined = do i <- getIState
491 return (map fst (idris_metavars i) \\ primDefs)
491 return (map fst (idris_metavars i) \\ primDefs)
492
492
493+isMetavarName :: Name -> IState -> Bool
494+isMetavarName n ist
495+ = case lookupNames n (tt_ctxt ist) of
496+ (t:_) -> isJust $ lookup t (idris_metavars ist)
497+ _ -> False
498+
493getWidth :: Idris ConsoleWidth
499getWidth :: Idris ConsoleWidth
494getWidth = fmap idris_consolewidth getIState
500getWidth = fmap idris_consolewidth getIState
495
501
@@ -579,10 +585,11 @@ fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
579fancifyAnnots ist annot@(AnnName n _ _) =
585fancifyAnnots ist annot@(AnnName n _ _) =
580 do let ctxt = tt_ctxt ist
586 do let ctxt = tt_ctxt ist
581 case () of
587 case () of
582− _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
588+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
583− _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
589+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
584− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
590+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
591+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) Nothing
585− _ | otherwise -> annot
592+ _ | otherwise -> annot
586fancifyAnnots _ annot = annot
593fancifyAnnots _ annot = annot
587
594
588type1Doc :: Doc OutputAnnotation
595type1Doc :: Doc OutputAnnotation
src/Idris/Core/TT.hs+1−1
@@ -82,7 +82,7 @@ instance Show FC where
82 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
82 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
83
83
84-- | Output annotation for pretty-printed name - decides colour
84-- | Output annotation for pretty-printed name - decides colour
85−data NameOutput = TypeOutput | FunOutput | DataOutput
85+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput
86
86
87-- | Text formatting output
87-- | Text formatting output
88data TextFormatting = BoldText | ItalicText | UnderlineText
88data TextFormatting = BoldText | ItalicText | UnderlineText
src/Idris/IdeSlave.hs+4−3
@@ -74,9 +74,10 @@ instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>
74 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
74 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
75
75
76instance SExpable NameOutput where
76instance SExpable NameOutput where
77− toSExp TypeOutput = SymbolAtom "type"
77+ toSExp TypeOutput = SymbolAtom "type"
78− toSExp FunOutput = SymbolAtom "function"
78+ toSExp FunOutput = SymbolAtom "function"
79− toSExp DataOutput = SymbolAtom "data"
79+ toSExp DataOutput = SymbolAtom "data"
80+ toSExp MetavarOutput = SymbolAtom "metavar"
80
81
81instance SExpable OutputAnnotation where
82instance SExpable OutputAnnotation where
82 toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
83 toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),