dfba993 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Experimental support for console colours on Windows

dfba993David Raymond Christiansen11 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -30,6 +30,7 @@ New in 0.9.19:

30* Major improvements to reflected elaboration scripts, including the ability to run

31 them in a declaration context and many bug fixes.

32* "decl syntax" rules to allow syntax extensions at the declaration level

33+* Experimental Windows support for console colours

34New in 0.9.18:

35New in 0.9.18:

35--------------

36--------------

idris.cabal+1−1

@@ -894,7 +894,7 @@ Library

894 , Tools_idris

895

896 Build-depends: base >=4 && <5

897− , annotated-wl-pprint >= 0.5.3 && < 0.7

897+ , annotated-wl-pprint >= 0.7 && < 0.8

898 , ansi-terminal < 0.7

899 , ansi-wl-pprint < 0.7

900 , base64-bytestring < 1.1

src/Idris/AbsSyntaxTree.hs+32−27

@@ -1576,36 +1576,41 @@ instance Pretty PTerm OutputAnnotation where

1576-- | Colourise annotations according to an Idris state. It ignores the names

1577-- in the annotation, as there's no good way to show extended information on a

1578-- terminal.

1579−consoleDecorate :: IState -> OutputAnnotation -> String -> String

1579+annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour

1580−consoleDecorate ist _ | not (idris_colourRepl ist) = id

1580+annotationColour ist _ | not (idris_colourRepl ist) = Nothing

1581+annotationColour ist (AnnConst c) =

1581−consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist

1582+ let theme = idris_colourTheme ist

1582− in if constIsType c

1583+ in Just $ if constIsType c

1583− then colouriseType theme

1584+ then typeColour theme

1584− else colouriseData theme

1585+ else dataColour theme

1585−consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)

1586+annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)

1586−consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)

1587+annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)

1587−consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1588+annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)

1588−consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1589+annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)

1589−consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1590+annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)

1591+annotationColour ist (AnnName n _ _ _) =

1590−consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist

1592+ let ctxt = tt_ctxt ist

1591− theme = idris_colourTheme ist

1593+ theme = idris_colourTheme ist

1592− in case () of

1594+ in case () of

1593− _ | isDConName n ctxt -> colouriseData theme

1595+ _ | isDConName n ctxt -> Just $ dataColour theme

1594− _ | isFnName n ctxt -> colouriseFun theme

1596+ _ | isFnName n ctxt -> Just $ functionColour theme

1595− _ | isTConName n ctxt -> colouriseType theme

1597+ _ | isTConName n ctxt -> Just $ typeColour theme

1596− _ | isPostulateName n ist -> colourisePostulate theme

1598+ _ | isPostulateName n ist -> Just $ postulateColour theme

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

1599+ _ | otherwise -> Nothing -- don't colourise unknown names

1598−consoleDecorate ist (AnnFC _) = id

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

1600+annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)

1600 where colour BoldText = IdrisColour Nothing True False True False

1601 where colour BoldText = IdrisColour Nothing True False True False

1601 colour UnderlineText = IdrisColour Nothing True True False False

1602 colour UnderlineText = IdrisColour Nothing True True False False

1602 colour ItalicText = IdrisColour Nothing True False False True

1603 colour ItalicText = IdrisColour Nothing True False False True

1603−consoleDecorate ist (AnnTerm _ _) = id

1604+annotationColour ist _ = Nothing

1604−consoleDecorate ist (AnnSearchResult _) = id

1605+

1605−consoleDecorate ist (AnnErr _) = id

1606+

1606−consoleDecorate ist (AnnNamespace _ _) = id

1607+-- | Colourise annotations according to an Idris state. It ignores the names

1607−consoleDecorate ist (AnnLink url) =

1608+-- in the annotation, as there's no good way to show extended

1608− \txt -> Idris.Colours.colourise (IdrisColour Nothing True True False False) txt ++ " (" ++ url ++ ")"

1609+-- information on a terminal. Note that strings produced this way will

1610+-- not be coloured on Windows, so the use of the colour rendering

1611+-- functions in Idris.Output is to be preferred.

1612+consoleDecorate :: IState -> OutputAnnotation -> String -> String

1613+consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)

1609

1614

1610isPostulateName :: Name -> IState -> Bool

1615isPostulateName :: Name -> IState -> Bool

1611isPostulateName n ist = S.member n (idris_postulates ist)

1616isPostulateName n ist = S.member n (idris_postulates ist)

src/Idris/Colours.hs+22−8

@@ -4,9 +4,10 @@ module Idris.Colours (

4 defaultTheme,

5 colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,

6 colouriseType, colouriseFun, colouriseData, colouriseKeyword,

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

7+ colourisePrompt, colourise, ColourType(..), hStartColourise, hEndColourise) where

9import System.Console.ANSI

10+import System.IO (Handle)

11data IdrisColour = IdrisColour { colour :: Maybe Color

12data IdrisColour = IdrisColour { colour :: Maybe Color

12 , vivid :: Bool

13 , vivid :: Bool

@@ -42,15 +43,28 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True

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

43 , postulateColour = IdrisColour (Just Green) True False True False

43 }

44 }

46+-- | Compute the ANSI colours corresponding to an Idris colour

47+mkSGR :: IdrisColour -> [SGR]

48+mkSGR (IdrisColour c v u b i) =

49+ fg c ++

50+ (if u then [SetUnderlining SingleUnderline] else []) ++

51+ (if b then [SetConsoleIntensity BoldIntensity] else []) ++

52+ (if i then [SetItalicized True] else [])

53+ where

54+ fg Nothing = []

55+ fg (Just c) = [SetColor Foreground (if v then Vivid else Dull) c]

56+

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

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

46colourise :: IdrisColour -> String -> String

58colourise :: IdrisColour -> String -> String

47−colourise (IdrisColour c v u b i) str = setSGRCode sgr ++ str ++ setSGRCode [Reset]

59+colourise c str = setSGRCode (mkSGR c) ++ str ++ setSGRCode [Reset]

48− where sgr = fg c ++

60+

49− (if u then [SetUnderlining SingleUnderline] else []) ++

61+-- | Start a colour on a handle, to support colour output on Windows

50− (if b then [SetConsoleIntensity BoldIntensity] else []) ++

62+hStartColourise :: Handle -> IdrisColour -> IO ()

51− (if i then [SetItalicized True] else [])

63+hStartColourise h c = hSetSGR h (mkSGR c)

52− fg Nothing = []

64+

53− fg (Just c) = [SetColor Foreground (if v then Vivid else Dull) c]

65+-- | End a colour region on a handle

66+hEndColourise :: Handle -> IdrisColour -> IO ()

67+hEndColourise h _ = hSetSGR h [Reset]

55-- | Set the colour of a string using POSIX escape codes, with trailing '\STX' denoting the end

69-- | Set the colour of a string using POSIX escape codes, with trailing '\STX' denoting the end

56-- (required by Haskeline in the prompt string)

70-- (required by Haskeline in the prompt string)

src/Idris/Output.hs+21−9

@@ -6,6 +6,7 @@ import Idris.Core.TT

6import Idris.Core.Evaluate (isDConName, isTConName, isFnName, normaliseAll)

8import Idris.AbsSyntax

9+import Idris.Colours (hStartColourise, hEndColourise)

9import Idris.Delaborate

10import Idris.Delaborate

10import Idris.Docstrings

11import Idris.Docstrings

11import Idris.IdeMode

12import Idris.IdeMode

@@ -17,7 +18,7 @@ import Control.Monad.Trans.Except (ExceptT (ExceptT), runExceptT)

18import System.Console.Haskeline.MonadException

19import System.Console.Haskeline.MonadException

19 (MonadException (controlIO), RunIO (RunIO))

20 (MonadException (controlIO), RunIO (RunIO))

20−import System.IO (stdout, Handle, hPutStrLn)

21+import System.IO (stdout, Handle, hPutStrLn, hPutStr)

21import System.FilePath (replaceExtension)

22import System.FilePath (replaceExtension)

23import Prelude hiding ((<$>))

24import Prelude hiding ((<$>))

@@ -45,7 +46,7 @@ iWarn fc err =

45 case fc of

46 case fc of

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

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

47 _ -> err

48 _ -> err

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

49+ hWriteDoc h i err'

49 IdeMode n h ->

50 IdeMode n h ->

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

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

51 let (str, spans) = displaySpans err'

52 let (str, spans) = displaySpans err'

@@ -68,13 +69,23 @@ iRender d = do w <- getWidth

68 | otherwise -> do width <- runIO getScreenWidth

69 | otherwise -> do width <- runIO getScreenWidth

69 return $ renderPretty 0.8 width d

70 return $ renderPretty 0.8 width d

72+hWriteDoc :: Handle -> IState -> SimpleDoc OutputAnnotation -> Idris ()

73+hWriteDoc h ist rendered =

74+ do runIO $ displayDecoratedA

75+ (hPutStr h)

76+ (maybe (return ()) (hStartColourise h))

77+ (maybe (return ()) (hEndColourise h))

78+ (fmap (annotationColour ist) rendered)

79+ runIO $ hPutStr h "\n" -- newline translation on the output

80+ -- stream should take care of this for

81+ -- Windows

82+

71-- | Write a pretty-printed term to the console with semantic coloring

83-- | Write a pretty-printed term to the console with semantic coloring

72consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

84consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

73−consoleDisplayAnnotated h output = do ist <- getIState

85+consoleDisplayAnnotated h output =

86+ do ist <- getIState

74− rendered <- iRender $ output

87+ rendered <- iRender output

75− runIO . hPutStrLn h .

76− displayDecorated (consoleDecorate ist) $

77− rendered

88+ hWriteDoc h ist rendered

79iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

90iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

80iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

91iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

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

97 do i <- getIState

108 do i <- getIState

98 case idris_outputmode i of

109 case idris_outputmode i of

99 RawOutput h -> do out <- iRender doc

110 RawOutput h -> do out <- iRender doc

100− runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

111+ hWriteDoc h i out

112+

101 IdeMode n h ->

113 IdeMode n h ->

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

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

103 let out = [toSExp str, toSExp spans]

115 let out = [toSExp str, toSExp spans]

@@ -168,7 +180,7 @@ idemodePutSExp cmd info = do i <- getIState

168iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

180iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

169iputGoal g = do i <- getIState

181iputGoal g = do i <- getIState

170 case idris_outputmode i of

182 case idris_outputmode i of

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

183+ RawOutput h -> hWriteDoc h i g

172 IdeMode n h ->

184 IdeMode n h ->

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

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

174 goal = [toSExp str, toSExp spans]

186 goal = [toSExp str, toSExp spans]

src/Idris/REPL.hs+5−3

@@ -114,7 +114,9 @@ repl orig mods efile

114 then ""

115 else showMVs colour theme mvs ++

116 let str = mkPrompt mods ++ ">" in

117+ (if colour && not isWindows

117− (if colour then colourisePrompt theme str else str) ++ " "

118+ then colourisePrompt theme str

119+ else str) ++ " "

118 x <- H.catch (getInputLine prompt)

120 x <- H.catch (getInputLine prompt)

119 (ctrlC (return Nothing))

121 (ctrlC (return Nothing))

120 case x of

122 case x of

@@ -1624,8 +1626,8 @@ idrisMain opts =

1624

1626

1625 when (DefaultTotal `elem` opts) $ do i <- getIState

1627 when (DefaultTotal `elem` opts) $ do i <- getIState

1626 putIState (i { default_total = True })

1628 putIState (i { default_total = True })

1627− setColourise $ not quiet && last ((not isWindows) : opt getColour opts)

1629+ setColourise $ not quiet && last (True : opt getColour opts)

1628−

1630+

1629

1631

1630

1632

1631 mapM_ addLangExt (opt getLanguageExt opts)

1633 mapM_ addLangExt (opt getLanguageExt opts)