16ff91f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add syntax for example code to docs

16ff91fDavid Raymond Christiansen12 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -22,6 +22,7 @@ New in 0.9.15:

22* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting

23* Naming of data and type constructors is made consistent across the standard library (see #1516)

24* Terms in `code blocks` inside of documentation strings are now parsed and type checked. If this succeeds, they are rendered in full color in documentation lookups, and with semantic highlighting for IDEs.

25+* Fenced code blocks in docs defined with the "example" attribute are rendered as code examples.

26New in 0.9.14:

27New in 0.9.14:

27--------------

28--------------

src/Idris/Delaborate.hs+1−1

@@ -441,7 +441,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

441 -- Issue #1588 on the Issue Tracker

442 -- https://github.com/idris-lang/Idris-dev/issues/1588

443 out = displayS . renderPretty 1.0 50 $

444− renderDocstring (pprintDelab ist) o

444+ renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) o

445 return (out "")

446 getTy :: IState -> Name -> String -- fails if name not already extant!

447 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

src/Idris/Docs.hs+3−3

@@ -35,14 +35,14 @@ data Docs = FunDoc FunDoc

35 deriving Show

37showDoc ist d | nullDocstring d = empty

38− | otherwise = text " -- " <> renderDocstring (pprintDelab ist) d

38+ | otherwise = text " -- " <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) d

40pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

41pprintFD ist (FD n doc args ty f)

42 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

43 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

44 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

45− renderDocstring (pprintDelab ist) doc <$>

45+ renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc <$>

46 maybe empty (\f -> text (show f) <> line) f <>

47 let argshow = showArgs args [] in

48 if not (null argshow)

@@ -84,7 +84,7 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

84 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

85 if nullDocstring doc

86 then empty

87− else line <> renderDocstring (pprintDelab ist) doc)

87+ else line <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc)

88 <> line <$>

89 nest 4 (text "Parameters:" <$> prettyParameters)

90 <> line <$>

src/Idris/Docstrings.hs+28−20

@@ -94,36 +94,44 @@ options = CT.Options { CT.sanitize = True

94 }

96-- | Convert a docstring to be shown by the pretty-printer

97−renderDocstring :: (a -> Doc OutputAnnotation) -> Docstring (Maybe a) -> Doc OutputAnnotation

97+renderDocstring :: (a -> Doc OutputAnnotation) -> (a -> a) -> Docstring (Maybe a) -> Doc OutputAnnotation

98−renderDocstring pp (DocString _ blocks) = renderBlocks pp blocks

98+renderDocstring pp norm (DocString _ blocks) = renderBlocks pp norm blocks

100-- | Construct a docstring consisting of the first block-level element of the

101-- argument docstring, for use in summaries.

102overview :: Docstring a -> Docstring a

103overview (DocString opts blocks) = DocString opts (S.take 1 blocks)

104

105−renderBlocks :: (a -> Doc OutputAnnotation) -> Blocks (Maybe a) -> Doc OutputAnnotation

105+renderBlocks :: (a -> Doc OutputAnnotation) -> (a -> a)

106+ -> Blocks (Maybe a) -> Doc OutputAnnotation

106−renderBlocks pp blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

107+renderBlocks pp norm blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

107− fmap (renderBlock pp) blocks

108+ fmap (renderBlock pp norm) blocks

108− | S.length blocks == 1 = renderBlock pp (S.index blocks 0)

109+ | S.length blocks == 1 = renderBlock pp norm (S.index blocks 0)

109 | otherwise = empty

110 | otherwise = empty

110

111

111−renderBlock :: (a -> Doc OutputAnnotation) -> Block (Maybe a) -> Doc OutputAnnotation

112+renderBlock :: (a -> Doc OutputAnnotation) -> (a -> a)

113+ -> Block (Maybe a) -> Doc OutputAnnotation

112−renderBlock pp (Para inlines) = renderInlines pp inlines

114+renderBlock pp norm (Para inlines) = renderInlines pp inlines

113−renderBlock pp (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

115+renderBlock pp norm (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

114−renderBlock pp (Blockquote blocks) = indent 8 $ renderBlocks pp blocks

116+renderBlock pp norm (Blockquote blocks) = indent 8 $ renderBlocks pp norm blocks

115−renderBlock pp (List b ty blockss) = renderList pp b ty blockss

117+renderBlock pp norm (List b ty blockss) = renderList pp norm b ty blockss

116−renderBlock pp (CodeBlock attr src Nothing) = indent 8 $ text (T.unpack src)

118+renderBlock pp norm (CodeBlock attr src Nothing) = indent 8 $ text (T.unpack src)

117−renderBlock pp (CodeBlock attr src (Just tm)) = indent 8 $ pp tm

119+renderBlock pp norm (CodeBlock attr src (Just tm))

120+ | isExample attr = indent 4 $

121+ text ">" <+> align (group (pp tm)) <$>

122+ align (group (pp (norm tm)))

123+ | otherwise = indent 4 $ pp tm

124+ where isExample (CT.CodeAttr lang info) = T.pack "example" `elem` lang : T.words info

118−renderBlock pp (HtmlBlock txt) = text "<html block>" -- TODO

125+renderBlock pp norm (HtmlBlock txt) = text "<html block>" -- TODO

119−renderBlock pp HRule = text "----------------------"

126+renderBlock pp norm HRule = text "----------------------"

120−

127+

128+renderList :: (a -> Doc OutputAnnotation) -> (a -> a)

121−renderList :: (a -> Doc OutputAnnotation) -> Bool -> CT.ListType -> [Blocks (Maybe a)] -> Doc OutputAnnotation

129+ -> Bool -> CT.ListType -> [Blocks (Maybe a)] -> Doc OutputAnnotation

122−renderList pp b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp) blockss

130+renderList pp norm b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp norm) blockss

123−renderList pp b (CT.Numbered nw i) blockss =

131+renderList pp norm b (CT.Numbered nw i) blockss =

124 vsep $

132 vsep $

125 zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

133 zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

126− [i..] (repeat punc) (map (renderBlocks pp) blockss)

134+ [i..] (repeat punc) (map (renderBlocks pp norm) blockss)

127 where punc = case nw of

135 where punc = case nw of

128 CT.PeriodFollowing -> char '.'

136 CT.PeriodFollowing -> char '.'

129 CT.ParenFollowing -> char '('

137 CT.ParenFollowing -> char '('

src/Idris/Output.hs+2−2

@@ -3,7 +3,7 @@

3module Idris.Output where

5import Idris.Core.TT

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

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

8import Idris.AbsSyntax

9import Idris.Delaborate

@@ -181,7 +181,7 @@ prettyDocumentedIst :: IState

181 -> Doc OutputAnnotation

182prettyDocumentedIst ist (name, ty, docs) =

183 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

184− fromMaybe empty (fmap (\d -> renderDocstring ppTm d <> line) docs)

184+ fromMaybe empty (fmap (\d -> renderDocstring ppTm (normaliseAll (tt_ctxt ist) []) d <> line) docs)

185 where ppTm = pprintDelab ist

186

187