e9ef380 · Idris-dev · git.iko.soy

libs/prelude/Prelude/Vect.idr+1−1

compare with master

unifiedsplit

@@ -26,7 +26,7 @@ infixr 7 ::

26

27||| Calculate the length of a `Vect`.

28|||

29−||| *Note*: this is only useful if you don't already statically know the length

29+||| **Note**: this is only useful if you don't already statically know the length

30||| and you want to avoid matching the implicit argument for erasure reasons.

31||| @ n the length (provably equal to the return value)

32||| @ xs the vector

src/Idris/AbsSyntaxTree.hs+4

@@ -1076,6 +1076,10 @@ consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1076 _ | isTConName n ctxt -> colouriseType theme

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

1078consoleDecorate ist (AnnFC _) = id

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

1080+ where colour BoldText = IdrisColour Nothing True False True False

1081+ colour UnderlineText = IdrisColour Nothing True True False False

1082+ colour ItalicText = IdrisColour Nothing True False False True

1079

1083

1080-- | Pretty-print a high-level closed Idris term

1084-- | Pretty-print a high-level closed Idris term

1081prettyImp :: Bool -- ^^ whether to show implicits

1085prettyImp :: Bool -- ^^ whether to show implicits

src/Idris/Colours.hs+3−3

@@ -4,8 +4,7 @@ module Idris.Colours (

4 defaultTheme,

5 colouriseKwd, colouriseBound, colouriseImplicit,

6 colouriseType, colouriseFun, colouriseData, colouriseKeyword,

7− colourisePrompt,

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

8− ColourType(..)) where

9

8

10import System.Console.ANSI

9import System.Console.ANSI

11

10

@@ -30,6 +29,7 @@ data ColourTheme = ColourTheme { keywordColour :: IdrisColour

30 }

29 }

31 deriving (Eq, Show)

30 deriving (Eq, Show)

32

31

32+-- | Idris's default console colour theme

33defaultTheme :: ColourTheme

34defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True False

35 , boundVarColour = mkColour Magenta

@@ -40,7 +40,7 @@ defaultTheme = ColourTheme { keywordColour = IdrisColour Nothing True False True

40 , promptColour = IdrisColour Nothing True False True False

41 }

42

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

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

44colourise :: IdrisColour -> String -> String

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

46 where sgr = fg c ++

src/Idris/Core/TT.hs+4

@@ -84,6 +84,9 @@ instance Show FC where

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

85data NameOutput = TypeOutput | FunOutput | DataOutput

86

87+-- | Text formatting output

88+data TextFormatting = BoldText | ItalicText | UnderlineText

89+

87-- | Output annotations for pretty-printing

90-- | Output annotations for pretty-printing

88data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

91data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

89 | AnnBoundName Name Bool

92 | AnnBoundName Name Bool

@@ -91,6 +94,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

91 | AnnConstType

94 | AnnConstType

92 | AnnKeyword

95 | AnnKeyword

93 | AnnFC FC

96 | AnnFC FC

97+ | AnnTextFmt TextFormatting

94

98

95-- | Used for error reflection

99-- | Used for error reflection

96data ErrorReportPart = TextPart String

100data ErrorReportPart = TextPart String

src/Idris/Docstrings.hs+5−4

@@ -9,7 +9,7 @@ import qualified Cheapskate.Types as CT

9

10import Util.Pretty

11

12−import Idris.Core.TT (OutputAnnotation, Name)

12+import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name)

13

14import qualified Data.Text as T

15import qualified Data.Foldable as F

@@ -71,10 +71,11 @@ renderInline (CT.Str s) = text $ T.unpack s

71renderInline CT.Space = space

72renderInline CT.SoftBreak = softline

73renderInline CT.LineBreak = line

74−renderInline (CT.Emph txt) = renderInlines txt -- TODO

74+renderInline (CT.Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines txt -- TODO

75−renderInline (CT.Strong txt) = renderInlines txt -- TODO

75+renderInline (CT.Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines txt -- TODO

76renderInline (CT.Code txt) = text $ T.unpack txt

77−renderInline (CT.Link body url title) = renderInlines body <+> parens (text $ T.unpack url)

77+renderInline (CT.Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines body) <+>

78+ parens (text $ T.unpack url)

78renderInline (CT.Image body url title) = text "<image>" -- TODO

79renderInline (CT.Image body url title) = text "<image>" -- TODO

79renderInline (CT.Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO

80renderInline (CT.Entity a) = text $ "<entity " ++ T.unpack a ++ ">" -- TODO

80renderInline (CT.RawHtml txt) = text "<html content>" --TODO

81renderInline (CT.RawHtml txt) = text "<html content>" --TODO

src/Idris/IdeSlave.hs+5

@@ -94,6 +94,11 @@ instance SExpable OutputAnnotation where

94 ((SymbolAtom "filename", StringAtom f),

95 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

96 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec))))]

97+ toSExp (AnnTextFmt fmt) = toSExp [(SymbolAtom "text-formatting", SymbolAtom format)]

98+ where format = case fmt of

99+ BoldText -> "bold"

100+ ItalicText -> "italic"

101+ UnderlineText -> "underline"

97

102

98escape :: String -> String

103escape :: String -> String

99escape = concatMap escapeChar

104escape = concatMap escapeChar

src/Idris/REPL.hs+1−1

@@ -23,7 +23,7 @@ import Idris.Completion

23import qualified Idris.IdeSlave as IdeSlave

24import Idris.Chaser

25import Idris.Imports

26−import Idris.Colours

26+import Idris.Colours hiding (colourise)

27import Idris.Inliner

28import Idris.CaseSplit

29import Idris.DeepSeq