1c155de · Idris-dev · git.iko.soy

src/Idris/Docs.hs+9−8

compare with master

unifiedsplit

@@ -148,6 +148,11 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

148 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

149 <> line <$>

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

151+

152+ <> (if null constraints

153+ then empty

154+ else line <$> nest 4 (text "Constraints:" <$> prettyConstraints))

155+

151 <> line <$>

156 <> line <$>

152 nest 4 (text "Methods:" <$>

157 nest 4 (text "Methods:" <$>

153 vsep (map (pprintFDWithTotality ist False) meths))

158 vsep (map (pprintFDWithTotality ist False) meths))

@@ -234,17 +239,13 @@ pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_

234 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

239 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

235 isSubInterface _ = False

240 isSubInterface _ = False

236

241

237− prettyConstraints separateLine =

242+ prettyConstraints =

238− let separator = if separateLine then line else empty

239− in case constraints of

240− [] -> empty

241− [pt] -> pprintPTerm ppo params' [] infixes pt <+> text "=>" <> separator

242− _ -> parens (cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))) <+> text "=>" <> separator

243+ cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))

243

244

244 prettyParameters =

245 prettyParameters =

245 if any (isJust . snd) params

246 if any (isJust . snd) params

246− then prettyConstraints True <> vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

247+ then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

247− else prettyConstraints False <+> hsep (punctuate comma (map (prettyName True False params' . fst) params))

248+ else hsep (punctuate comma (map (prettyName True False params' . fst) params))

248

249

249pprintDocs ist (RecordDoc n doc ctor projs params)

250pprintDocs ist (RecordDoc n doc ctor projs params)

250 = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>

251 = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>

test/TestData.hs+2−1

@@ -91,7 +91,8 @@ testFamiliesData = [

91 ( 2, ANY ),

92 ( 3, ANY ),

93 ( 4, ANY ),

94− ( 5, ANY )]),

94+ ( 5, ANY ),

95+ ( 6, ANY )]),

95 ("dsl", "DSL",

96 ("dsl", "DSL",

96 [ ( 1, ANY ),

97 [ ( 1, ANY ),

97 ( 2, C_CG ),

98 ( 2, C_CG ),

test/docs006/docs006.idrnew file+7

@@ -0,0 +1,7 @@

1+module docs006

2+

3+||| interface

4+||| @ t some parameter

5+interface Eq t => Foo t where

6+ ||| member of interface

7+ m : t

test/docs006/expectednew file+16

@@ -0,0 +1,16 @@

1+Interface Foo

2+ interface

3+

4+Parameters:

5+ t -- some parameter

6+

7+Constraints:

8+ Eq t

9+

10+Methods:

11+ m : Foo t => t

12+ member of interface

13+

14+ The function is Total

15+Implementations:

16+ <no implementations>

test/docs006/inputnew file+1

@@ -0,0 +1 @@

1+:doc Foo

test/docs006/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none --nocolor docs006.idr < input

3+rm *.ibc