dfba993 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Experimental support for console colours on Windows

commitdfba993f4c7009bd02b737dbceaf89c2a531165d authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 27 Aug 2015, 13:31 (11 years ago) parentffb50e2

6 files changed+82−48

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+1−1 src/Idris/AbsSyntaxTree.hs+32−27 src/Idris/Colours.hs+22−8 src/Idris/Output.hs+21−9 src/Idris/REPL.hs+5−3

CHANGELOG+1

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

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

3131 them in a declaration context and many bug fixes.

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

33+* Experimental Windows support for console colours

3334

3435New in 0.9.18:

3536--------------

idris.cabal+1−1

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

894894 , Tools_idris

895895

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

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

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

898898 , ansi-terminal < 0.7

899899 , ansi-wl-pprint < 0.7

900900 , base64-bytestring < 1.1

src/Idris/AbsSyntaxTree.hs+32−27

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

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

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

15781578-- terminal.

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

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

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

1582− in if constIsType c

1583− then colouriseType theme

1584− else colouriseData theme

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

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

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

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

1589−consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

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

1591− theme = idris_colourTheme ist

1592− in case () of

1593− _ | isDConName n ctxt -> colouriseData theme

1594− _ | isFnName n ctxt -> colouriseFun theme

1595− _ | isTConName n ctxt -> colouriseType theme

1596− _ | isPostulateName n ist -> colourisePostulate theme

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

1598−consoleDecorate ist (AnnFC _) = id

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

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

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

1581+annotationColour ist (AnnConst c) =

1582+ let theme = idris_colourTheme ist

1583+ in Just $ if constIsType c

1584+ then typeColour theme

1585+ else dataColour theme

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

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

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

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

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

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

1592+ let ctxt = tt_ctxt ist

1593+ theme = idris_colourTheme ist

1594+ in case () of

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

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

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

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

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

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

16001601 where colour BoldText = IdrisColour Nothing True False True False

16011602 colour UnderlineText = IdrisColour Nothing True True False False

16021603 colour ItalicText = IdrisColour Nothing True False False True

1603−consoleDecorate ist (AnnTerm _ _) = id

1604−consoleDecorate ist (AnnSearchResult _) = id

1605−consoleDecorate ist (AnnErr _) = id

1606−consoleDecorate ist (AnnNamespace _ _) = id

1607−consoleDecorate ist (AnnLink url) =

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

1604+annotationColour ist _ = Nothing

1605+

1606+

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

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

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)

16091614

16101615isPostulateName :: Name -> IState -> Bool

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

src/Idris/Colours.hs+22−8

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

44 defaultTheme,

55 colouriseKwd, colouriseBound, colouriseImplicit, colourisePostulate,

66 colouriseType, colouriseFun, colouriseData, colouriseKeyword,

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

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

99import System.Console.ANSI

10+import System.IO (Handle)

1011

1112data IdrisColour = IdrisColour { colour :: Maybe Color

1213 , vivid :: Bool

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

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

4344 }

4445

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+

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

4658colourise :: IdrisColour -> String -> String

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

48− where sgr = fg c ++

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

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

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

52− fg Nothing = []

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

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

60+

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

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

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

64+

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

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

67+hEndColourise h _ = hSetSGR h [Reset]

5468

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

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

src/Idris/Output.hs+21−9

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

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

88import Idris.AbsSyntax

9+import Idris.Colours (hStartColourise, hEndColourise)

910import Idris.Delaborate

1011import Idris.Docstrings

1112import Idris.IdeMode

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

1718

1819import System.Console.Haskeline.MonadException

1920 (MonadException (controlIO), RunIO (RunIO))

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

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

2122import System.FilePath (replaceExtension)

2223

2324import Prelude hiding ((<$>))

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

4546 case fc of

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

4748 _ -> err

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

49+ hWriteDoc h i err'

4950 IdeMode n h ->

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

5152 let (str, spans) = displaySpans err'

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

6869 | otherwise -> do width <- runIO getScreenWidth

6970 return $ renderPretty 0.8 width d

7071

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+

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

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

73−consoleDisplayAnnotated h output = do ist <- getIState

74− rendered <- iRender $ output

75− runIO . hPutStrLn h .

76− displayDecorated (consoleDecorate ist) $

77− rendered

85+consoleDisplayAnnotated h output =

86+ do ist <- getIState

87+ rendered <- iRender output

88+ hWriteDoc h ist rendered

7889

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

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

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

97108 do i <- getIState

98109 case idris_outputmode i of

99110 RawOutput h -> do out <- iRender doc

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

111+ hWriteDoc h i out

112+

101113 IdeMode n h ->

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

103115 let out = [toSExp str, toSExp spans]

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

168180iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

169181iputGoal g = do i <- getIState

170182 case idris_outputmode i of

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

183+ RawOutput h -> hWriteDoc h i g

172184 IdeMode n h ->

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

174186 goal = [toSExp str, toSExp spans]

src/Idris/REPL.hs+5−3

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

114114 then ""

115115 else showMVs colour theme mvs ++

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

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

117+ (if colour && not isWindows

118+ then colourisePrompt theme str

119+ else str) ++ " "

118120 x <- H.catch (getInputLine prompt)

119121 (ctrlC (return Nothing))

120122 case x of

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

16241626

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

16261628 putIState (i { default_total = True })

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

1628−

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

1630+

16291631

16301632

16311633 mapM_ addLangExt (opt getLanguageExt opts)