e9ef380 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Support text formatting in docstrings

Now, Markdown text formatting is no-longer a no-op. Needed to make the stern warning on Vect.length look reasonable.

commite9ef380339669c529bf13d6a75cfad55e30edde0 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 18 Mar 2014, 15:33 (13 years ago) parente7c5cb2

7 files changed+23−9

compare with master

unifiedsplit

libs/prelude/Prelude/Vect.idr+1−1 src/Idris/AbsSyntaxTree.hs+4 src/Idris/Colours.hs+3−3 src/Idris/Core/TT.hs+4 src/Idris/Docstrings.hs+5−4 src/Idris/IdeSlave.hs+5 src/Idris/REPL.hs+1−1

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

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

2626

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

2828|||

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

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

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

3232||| @ xs the vector

src/Idris/AbsSyntaxTree.hs+4

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

10761076 _ | isTConName n ctxt -> colouriseType theme

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

10781078consoleDecorate 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

10791083

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

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

src/Idris/Colours.hs+3−3

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

44 defaultTheme,

55 colouriseKwd, colouriseBound, colouriseImplicit,

66 colouriseType, colouriseFun, colouriseData, colouriseKeyword,

7− colourisePrompt,

8− ColourType(..)) where

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

109import System.Console.ANSI

1110

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

3029 }

3130 deriving (Eq, Show)

3231

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

3333defaultTheme :: ColourTheme

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

3535 , boundVarColour = mkColour Magenta

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

4040 , promptColour = IdrisColour Nothing True False True False

4141 }

4242

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

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

4444colourise :: IdrisColour -> String -> String

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

4646 where sgr = fg c ++

src/Idris/Core/TT.hs+4

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

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

8585data NameOutput = TypeOutput | FunOutput | DataOutput

8686

87+-- | Text formatting output

88+data TextFormatting = BoldText | ItalicText | UnderlineText

89+

8790-- | Output annotations for pretty-printing

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

8992 | AnnBoundName Name Bool

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

9194 | AnnConstType

9295 | AnnKeyword

9396 | AnnFC FC

97+ | AnnTextFmt TextFormatting

9498

9599-- | Used for error reflection

96100data ErrorReportPart = TextPart String

src/Idris/Docstrings.hs+5−4

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

1010import Util.Pretty

1111

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

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

1313

1414import qualified Data.Text as T

1515import qualified Data.Foldable as F

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

7171renderInline CT.Space = space

7272renderInline CT.SoftBreak = softline

7373renderInline CT.LineBreak = line

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

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

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

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

7676renderInline (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)

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

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

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

src/Idris/IdeSlave.hs+5

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

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

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

9696 (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"

97102

98103escape :: String -> String

99104escape = concatMap escapeChar

src/Idris/REPL.hs+1−1

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

2323import qualified Idris.IdeSlave as IdeSlave

2424import Idris.Chaser

2525import Idris.Imports

26−import Idris.Colours

26+import Idris.Colours hiding (colourise)

2727import Idris.Inliner

2828import Idris.CaseSplit

2929import Idris.DeepSeq