git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1012 from david-christiansen/issue/949

Add semantic highlighting info for metavariables

commit1569aa9e45c001f8cdbdf84ba4c12e5e2d0f15b1 authorEdwin Brady <edwin.brady@gmail.com> dateTue 1 Apr 2014, 14:11 (13 years ago) parent8f5e40fdd20fac
3 files changed+16−8
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+11−4 src/Idris/Core/TT.hs+1−1 src/Idris/IdeSlave.hs+4−3
src/Idris/AbsSyntax.hs+11−4
@@ -490,6 +490,12 @@ getUndefined :: Idris [Name]
490490getUndefined = do i <- getIState
491491 return (map fst (idris_metavars i) \\ primDefs)
492492
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+
493499getWidth :: Idris ConsoleWidth
494500getWidth = fmap idris_consolewidth getIState
495501
@@ -579,10 +585,11 @@ fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
579585fancifyAnnots ist annot@(AnnName n _ _) =
580586 do let ctxt = tt_ctxt ist
581587 case () of
582− _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
583− _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
584− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
585− _ | otherwise -> annot
588+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
589+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
590+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
591+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) Nothing
592+ _ | otherwise -> annot
586593fancifyAnnots _ annot = annot
587594
588595type1Doc :: Doc OutputAnnotation
src/Idris/Core/TT.hs+1−1
@@ -82,7 +82,7 @@ instance Show FC where
8282 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
8383
8484-- | Output annotation for pretty-printed name - decides colour
85−data NameOutput = TypeOutput | FunOutput | DataOutput
85+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput
8686
8787-- | Text formatting output
8888data 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) =>
7474 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]
7575
7676instance SExpable NameOutput where
77− toSExp TypeOutput = SymbolAtom "type"
78− toSExp FunOutput = SymbolAtom "function"
79− toSExp DataOutput = SymbolAtom "data"
77+ toSExp TypeOutput = SymbolAtom "type"
78+ toSExp FunOutput = SymbolAtom "function"
79+ toSExp DataOutput = SymbolAtom "data"
80+ toSExp MetavarOutput = SymbolAtom "metavar"
8081
8182instance SExpable OutputAnnotation where
8283 toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),