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

Add semantic highlighting for postulates

commitbaaea97ff7546cd935b0936dfeb9833decd07e59 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 6 Jun 2014, 10:30 (12 years ago) parent9c59a19d6c5b2b
7 files changed+43−29
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+8−7 src/Idris/AbsSyntaxTree.hs+8−4 src/Idris/Colours.hs+15−8 src/Idris/Core/TT.hs+1−1 src/Idris/Delaborate.hs+5−4 src/Idris/IdeSlave.hs+5−4 src/Idris/REPLParser.hs+1−1
src/Idris/AbsSyntax.hs+8−7
@@ -778,13 +778,14 @@ setColour :: ColourType -> IdrisColour -> Idris ()
778778setColour ct c = do i <- getIState
779779 let newTheme = setColour' ct c (idris_colourTheme i)
780780 putIState $ i { idris_colourTheme = newTheme }
781− where setColour' KeywordColour c t = t { keywordColour = c }
782− setColour' BoundVarColour c t = t { boundVarColour = c }
783− setColour' ImplicitColour c t = t { implicitColour = c }
784− setColour' FunctionColour c t = t { functionColour = c }
785− setColour' TypeColour c t = t { typeColour = c }
786− setColour' DataColour c t = t { dataColour = c }
787− setColour' PromptColour c t = t { promptColour = c }
781+ where setColour' KeywordColour c t = t { keywordColour = c }
782+ setColour' BoundVarColour c t = t { boundVarColour = c }
783+ setColour' ImplicitColour c t = t { implicitColour = c }
784+ setColour' FunctionColour c t = t { functionColour = c }
785+ setColour' TypeColour c t = t { typeColour = c }
786+ setColour' DataColour c t = t { dataColour = c }
787+ setColour' PromptColour c t = t { promptColour = c }
788+ setColour' PostulateColour c t = t { postulateColour = c }
788789
789790logLvl :: Int -> String -> Idris ()
790791logLvl l str = do i <- getIState
src/Idris/AbsSyntaxTree.hs+8−4
@@ -1150,16 +1150,20 @@ consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
11501150consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
11511151 theme = idris_colourTheme ist
11521152 in case () of
1153− _ | isDConName n ctxt -> colouriseData theme
1154− _ | isFnName n ctxt -> colouriseFun theme
1155− _ | isTConName n ctxt -> colouriseType theme
1156− _ | otherwise -> id -- don't colourise unknown names
1153+ _ | isDConName n ctxt -> colouriseData theme
1154+ _ | isFnName n ctxt -> colouriseFun theme
1155+ _ | isTConName n ctxt -> colouriseType theme
1156+ _ | isPostulateName n ist -> colourisePostulate theme
1157+ _ | otherwise -> id -- don't colourise unknown names
11571158consoleDecorate ist (AnnFC _) = id
11581159consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
11591160 where colour BoldText = IdrisColour Nothing True False True False
11601161 colour UnderlineText = IdrisColour Nothing True True False False
11611162 colour ItalicText = IdrisColour Nothing True False False True
11621163
1164+isPostulateName :: Name -> IState -> Bool
1165+isPostulateName n ist = S.member n (idris_postulates ist)
1166+
11631167-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
11641168prettyImp :: PPOption -- ^^ pretty printing options
11651169 -> PTerm -- ^^ the term to pretty-print
src/Idris/Colours.hs+15−8
@@ -2,7 +2,7 @@ module Idris.Colours (
22 IdrisColour(..),
33 ColourTheme(..),
44 defaultTheme,
5− colouriseKwd, colouriseBound, colouriseImplicit,
5+ colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,
66 colouriseType, colouriseFun, colouriseData, colouriseKeyword,
77 colourisePrompt, colourise, ColourType(..)) where
88
@@ -19,13 +19,14 @@ data IdrisColour = IdrisColour { colour :: Maybe Color
1919mkColour :: Color -> IdrisColour
2020mkColour c = IdrisColour (Just c) True False False False
2121
22−data ColourTheme = ColourTheme { keywordColour :: IdrisColour
23− , boundVarColour :: IdrisColour
24− , implicitColour :: IdrisColour
25− , functionColour :: IdrisColour
26− , typeColour :: IdrisColour
27− , dataColour :: IdrisColour
28− , promptColour :: IdrisColour
22+data ColourTheme = ColourTheme { keywordColour :: IdrisColour
23+ , boundVarColour :: IdrisColour
24+ , implicitColour :: IdrisColour
25+ , functionColour :: IdrisColour
26+ , typeColour :: IdrisColour
27+ , dataColour :: IdrisColour
28+ , promptColour :: IdrisColour
29+ , postulateColour :: IdrisColour
2930 }
3031 deriving (Eq, Show)
3132
@@ -38,6 +39,7 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True
3839 , typeColour = mkColour Blue
3940 , dataColour = mkColour Red
4041 , promptColour = IdrisColour Nothing True False True False
42+ , postulateColour = IdrisColour (Just Green) True False True False
4143 }
4244
4345-- | Set the colour of a string using POSIX escape codes
@@ -74,6 +76,10 @@ colourisePrompt t = colourise (promptColour t)
7476colouriseKeyword :: ColourTheme -> String -> String
7577colouriseKeyword t = colourise (keywordColour t)
7678
79+colourisePostulate :: ColourTheme -> String -> String
80+colourisePostulate t = colourise (postulateColour t)
81+
82+
7783data ColourType = KeywordColour
7884 | BoundVarColour
7985 | ImplicitColour
@@ -81,4 +87,5 @@ data ColourType = KeywordColour
8187 | TypeColour
8288 | DataColour
8389 | PromptColour
90+ | PostulateColour
8491 deriving (Eq, Show, Bounded, Enum)
src/Idris/Core/TT.hs+1−1
@@ -83,7 +83,7 @@ instance Show FC where
8383 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
8484
8585-- | Output annotation for pretty-printed name - decides colour
86−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput
86+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput
8787
8888-- | Text formatting output
8989data TextFormatting = BoldText | ItalicText | UnderlineText
src/Idris/Delaborate.hs+5−4
@@ -265,10 +265,11 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =
265265 docs = docOverview ist n
266266 ty = Just (getTy ist n)
267267 case () of
268− _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
269− _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
270− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
271− _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
268+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty
269+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty
270+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty
271+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty
272+ _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty
272273 _ | otherwise -> annot
273274 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs
274275 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)
src/Idris/IdeSlave.hs+5−4
@@ -74,10 +74,11 @@ 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"
80− toSExp MetavarOutput = SymbolAtom "metavar"
77+ toSExp TypeOutput = SymbolAtom "type"
78+ toSExp FunOutput = SymbolAtom "function"
79+ toSExp DataOutput = SymbolAtom "data"
80+ toSExp MetavarOutput = SymbolAtom "metavar"
81+ toSExp PostulateOutput = SymbolAtom "postulate"
8182
8283maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]
8384maybeProps [] = []
src/Idris/REPLParser.hs+1−1
@@ -184,7 +184,7 @@ pColourMod = try (P.symbol "vivid" >> return doVivid)
184184 doNoItalic i = i { italic = False }
185185 doSetColour c i = i { colour = c }
186186
187−
187+-- | Generate the colour type names using the default Show instance.
188188colourTypes :: [(String, ColourType)]
189189colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
190190 enumFromTo minBound maxBound