git.iko.soy/Idris-dev
on master help sign in
Only show documented arguments in :doc

This reduces redundancy, avoids showing internal names like __pi_arg, and takes up less space. New output: Idris> :doc foldl foldl : Foldable t => (acc -> elt -> acc) -> acc -> (t elt) -> acc Idris> :doc id id : a -> a Identity function. Idris> :doc the the : (a : Type) -> (x : a) -> a Manually assign a type to an expression. Arguments: a : Type -- the type to assign x : a -- the element to get the type

commitd1e12d5774ad42ccb6cf0ccfb0f88ead12952223 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 25 Mar 2014, 08:34 (13 years ago) parent04e2cd8
1 file changed+6−7
compare with master
unifiedsplit
src/Idris/Docs.hs+6−7
src/Idris/Docs.hs+6−7
@@ -44,23 +44,22 @@ pprintFD imp (FD n doc args ty f)
4444 then nest 4 $ text "Arguments:" <$> vsep argshow
4545 else empty)
4646
47− where showArgs ((n, ty, Exp {}, d):args) bnd
47+ where showArgs ((n, ty, Exp {}, Just d):args) bnd
4848 = bindingOf n False <+> colon <+>
4949 pprintPTerm imp bnd [] ty <>
50− showDoc (maybe emptyDocstring id d) <> line
50+ showDoc d <> line
5151 :
5252 showArgs args ((n, False):bnd)
53− showArgs ((n, ty, Constraint {}, d):args) bnd
53+ showArgs ((n, ty, Constraint {}, Just d):args) bnd
5454 = text "Class constraint" <+>
55− pprintPTerm imp bnd [] ty <> showDoc (maybe emptyDocstring id d) <> line
55+ pprintPTerm imp bnd [] ty <> showDoc d <> line
5656 :
5757 showArgs args ((n, True):bnd)
58− showArgs ((n, ty, Imp {}, d):args) bnd
59− | Just d' <- d
58+ showArgs ((n, ty, Imp {}, Just d):args) bnd
6059 = text "(implicit)" <+>
6160 bindingOf n True <+> colon <+>
6261 pprintPTerm imp bnd [] ty <>
63− showDoc d' <> line
62+ showDoc d <> line
6463 :
6564 showArgs args ((n, True):bnd)
6665 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)