baaea97 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+8−7

compare with master

unifiedsplit

@@ -778,13 +778,14 @@ setColour :: ColourType -> IdrisColour -> Idris ()

778setColour ct c = do i <- getIState

779 let newTheme = setColour' ct c (idris_colourTheme i)

780 putIState $ i { idris_colourTheme = newTheme }

781− where setColour' KeywordColour c t = t { keywordColour = c }

781+ where setColour' KeywordColour c t = t { keywordColour = c }

782− setColour' BoundVarColour c t = t { boundVarColour = c }

782+ setColour' BoundVarColour c t = t { boundVarColour = c }

783− setColour' ImplicitColour c t = t { implicitColour = c }

783+ setColour' ImplicitColour c t = t { implicitColour = c }

784− setColour' FunctionColour c t = t { functionColour = c }

784+ setColour' FunctionColour c t = t { functionColour = c }

785− setColour' TypeColour c t = t { typeColour = c }

785+ setColour' TypeColour c t = t { typeColour = c }

786− setColour' DataColour c t = t { dataColour = c }

786+ setColour' DataColour c t = t { dataColour = c }

787− setColour' PromptColour c t = t { promptColour = c }

787+ setColour' PromptColour c t = t { promptColour = c }

788+ setColour' PostulateColour c t = t { postulateColour = c }

788

789

789logLvl :: Int -> String -> Idris ()

790logLvl :: Int -> String -> Idris ()

790logLvl l str = do i <- getIState

791logLvl l str = do i <- getIState

src/Idris/AbsSyntaxTree.hs+8−4

@@ -1150,16 +1150,20 @@ consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1150consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist

1151 theme = idris_colourTheme ist

1152 in case () of

1153− _ | isDConName n ctxt -> colouriseData theme

1153+ _ | isDConName n ctxt -> colouriseData theme

1154− _ | isFnName n ctxt -> colouriseFun theme

1154+ _ | isFnName n ctxt -> colouriseFun theme

1155− _ | isTConName n ctxt -> colouriseType theme

1155+ _ | isTConName n ctxt -> colouriseType theme

1156+ _ | isPostulateName n ist -> colourisePostulate theme

1156− _ | otherwise -> id -- don't colourise unknown names

1157+ _ | otherwise -> id -- don't colourise unknown names

1157consoleDecorate ist (AnnFC _) = id

1158consoleDecorate ist (AnnFC _) = id

1158consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1159consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1159 where colour BoldText = IdrisColour Nothing True False True False

1160 where colour BoldText = IdrisColour Nothing True False True False

1160 colour UnderlineText = IdrisColour Nothing True True False False

1161 colour UnderlineText = IdrisColour Nothing True True False False

1161 colour ItalicText = IdrisColour Nothing True False False True

1162 colour ItalicText = IdrisColour Nothing True False False True

1162

1163

1164+isPostulateName :: Name -> IState -> Bool

1165+isPostulateName n ist = S.member n (idris_postulates ist)

1166+

1163-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1167-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1164prettyImp :: PPOption -- ^^ pretty printing options

1168prettyImp :: PPOption -- ^^ pretty printing options

1165 -> PTerm -- ^^ the term to pretty-print

1169 -> PTerm -- ^^ the term to pretty-print

src/Idris/Colours.hs+15−8

@@ -2,7 +2,7 @@ module Idris.Colours (

2 IdrisColour(..),

3 ColourTheme(..),

4 defaultTheme,

5− colouriseKwd, colouriseBound, colouriseImplicit,

5+ colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,

6 colouriseType, colouriseFun, colouriseData, colouriseKeyword,

7 colourisePrompt, colourise, ColourType(..)) where

8

@@ -19,13 +19,14 @@ data IdrisColour = IdrisColour { colour :: Maybe Color

19mkColour :: Color -> IdrisColour

20mkColour c = IdrisColour (Just c) True False False False

21

22−data ColourTheme = ColourTheme { keywordColour :: IdrisColour

22+data ColourTheme = ColourTheme { keywordColour :: IdrisColour

23− , boundVarColour :: IdrisColour

23+ , boundVarColour :: IdrisColour

24− , implicitColour :: IdrisColour

24+ , implicitColour :: IdrisColour

25− , functionColour :: IdrisColour

25+ , functionColour :: IdrisColour

26− , typeColour :: IdrisColour

26+ , typeColour :: IdrisColour

27− , dataColour :: IdrisColour

27+ , dataColour :: IdrisColour

28− , promptColour :: IdrisColour

28+ , promptColour :: IdrisColour

29+ , postulateColour :: IdrisColour

29 }

30 }

30 deriving (Eq, Show)

31 deriving (Eq, Show)

31

32

@@ -38,6 +39,7 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True

38 , typeColour = mkColour Blue

39 , typeColour = mkColour Blue

39 , dataColour = mkColour Red

40 , dataColour = mkColour Red

40 , promptColour = IdrisColour Nothing True False True False

41 , promptColour = IdrisColour Nothing True False True False

42+ , postulateColour = IdrisColour (Just Green) True False True False

41 }

43 }

42

44

43-- | Set the colour of a string using POSIX escape codes

45-- | Set the colour of a string using POSIX escape codes

@@ -74,6 +76,10 @@ colourisePrompt t = colourise (promptColour t)

74colouriseKeyword :: ColourTheme -> String -> String

76colouriseKeyword :: ColourTheme -> String -> String

75colouriseKeyword t = colourise (keywordColour t)

77colouriseKeyword t = colourise (keywordColour t)

76

78

79+colourisePostulate :: ColourTheme -> String -> String

80+colourisePostulate t = colourise (postulateColour t)

81+

82+

77data ColourType = KeywordColour

83data ColourType = KeywordColour

78 | BoundVarColour

84 | BoundVarColour

79 | ImplicitColour

85 | ImplicitColour

@@ -81,4 +87,5 @@ data ColourType = KeywordColour

81 | TypeColour

87 | TypeColour

82 | DataColour

88 | DataColour

83 | PromptColour

89 | PromptColour

90+ | PostulateColour

84 deriving (Eq, Show, Bounded, Enum)

91 deriving (Eq, Show, Bounded, Enum)

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

@@ -83,7 +83,7 @@ instance Show FC where

83 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec

84

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

86−data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput

86+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput

87

88-- | Text formatting output

89data TextFormatting = BoldText | ItalicText | UnderlineText

src/Idris/Delaborate.hs+5−4

@@ -265,10 +265,11 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

265 docs = docOverview ist n

266 ty = Just (getTy ist n)

267 case () of

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

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

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

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

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

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

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

271+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

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

272 _ | otherwise -> annot

273 _ | otherwise -> annot

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

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

274 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

275 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) =>

74 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]

75

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+ toSExp MetavarOutput = SymbolAtom "metavar"

81+ toSExp PostulateOutput = SymbolAtom "postulate"

81

82

82maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

83maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

83maybeProps [] = []

84maybeProps [] = []

src/Idris/REPLParser.hs+1−1

@@ -184,7 +184,7 @@ pColourMod = try (P.symbol "vivid" >> return doVivid)

184 doNoItalic i = i { italic = False }

185 doSetColour c i = i { colour = c }

186

187−

187+-- | Generate the colour type names using the default Show instance.

188colourTypes :: [(String, ColourType)]

189colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $

190 enumFromTo minBound maxBound