a724531 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -567,7 +567,7 @@ ihPrintFunTypes h bnd n overloads = do imp <- impShow

567 RawOutput -> consoleDisplayAnnotated h output

568 IdeSlave n -> ideSlaveReturnAnnotated n h output

569 where fullName n = prettyName True bnd n

570− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd tm)

570+ ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

571

572ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

573ihRenderResult h d = do ist <- getIState

src/Idris/AbsSyntaxTree.hs+4−3

@@ -1085,14 +1085,15 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

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

1086 -> PTerm -- ^^ the term to pretty-print

1087 -> Doc OutputAnnotation

1088−prettyImp impl = pprintPTerm impl []

1088+prettyImp impl = pprintPTerm impl [] []

1089

1090-- | Pretty-print a high-level Idris term in some bindings context

1091pprintPTerm :: Bool -- ^^ whether to show implicits

1092 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

1093+ -> [Name] -- ^^ names to always show in pi, even if not used

1093 -> PTerm -- ^^ the term to pretty-print

1094 -> PTerm -- ^^ the term to pretty-print

1094 -> Doc OutputAnnotation

1095 -> Doc OutputAnnotation

1095−pprintPTerm impl bnd = prettySe 10 bnd

1096+pprintPTerm impl bnd docArgs = prettySe 10 bnd

1096 where

1097 where

1097 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1098 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1098 prettySe p bnd (PQuote r) =

1099 prettySe p bnd (PQuote r) =

@@ -1112,7 +1113,7 @@ pprintPTerm impl bnd = prettySe 10 bnd

1112 prettySe 10 bnd v <+> kwd "in" </>

1113 prettySe 10 bnd v <+> kwd "in" </>

1113 prettySe 10 ((n, False):bnd) sc

1114 prettySe 10 ((n, False):bnd) sc

1114 prettySe p bnd (PPi (Exp l s _) n ty sc)

1115 prettySe p bnd (PPi (Exp l s _) n ty sc)

1115− | n `elem` allNamesIn sc || impl =

1116+ | n `elem` allNamesIn sc || impl || n `elem` docArgs =

1116 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1117 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1117 bracket p 2 . group $

1118 bracket p 2 . group $

1118 enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1119 enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

src/Idris/Delaborate.hs+1−1

@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

138pprintTerm ist = pprintTerm' ist []

139

140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141−pprintTerm' ist = pprintPTerm (opt_showimp (idris_options ist))

141+pprintTerm' ist bnd tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm

142

143pshow :: IState -> Err -> String

144pshow ist err = displayDecorated (consoleDecorate ist) .

src/Idris/Docs.hs+13−10

@@ -12,6 +12,7 @@ import Util.Pretty

12

13import Data.Maybe

14import Data.List

15+import qualified Data.Text as T

15

16

16-- TODO: Only include names with public/abstract accessibility

17-- TODO: Only include names with public/abstract accessibility

17

18

@@ -33,30 +34,32 @@ showDoc d | nullDocstring d = empty

33

34

34pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

35pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

35pprintFD imp (FD n doc args ty f)

36pprintFD imp (FD n doc args ty f)

36− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>

37+ = nest 4 (prettyName imp [] n <+> colon <+>

38+ pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args

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

40+ renderDocstring doc <$>

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

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

38 let argshow = showArgs args [] in

42 let argshow = showArgs args [] in

39 if not (null argshow)

43 if not (null argshow)

40 then nest 4 $ text "Arguments:" <$> vsep argshow

44 then nest 4 $ text "Arguments:" <$> vsep argshow

41 else empty)

45 else empty)

42

46

43− where showArgs ((n, ty, Exp {}, d):args) bnd

47+ where showArgs ((n, ty, Exp {}, Just d):args) bnd

44 = bindingOf n False <+> colon <+>

48 = bindingOf n False <+> colon <+>

45− pprintPTerm imp bnd ty <>

49+ pprintPTerm imp bnd [] ty <>

46− showDoc (maybe emptyDocstring id d) <> line

50+ showDoc d <> line

47 :

51 :

48 showArgs args ((n, False):bnd)

52 showArgs args ((n, False):bnd)

49− showArgs ((n, ty, Constraint {}, d):args) bnd

53+ showArgs ((n, ty, Constraint {}, Just d):args) bnd

50 = text "Class constraint" <+>

54 = text "Class constraint" <+>

51− pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line

55+ pprintPTerm imp bnd [] ty <> showDoc d <> line

52 :

56 :

53 showArgs args ((n, True):bnd)

57 showArgs args ((n, True):bnd)

54− showArgs ((n, ty, Imp {}, d):args) bnd

58+ showArgs ((n, ty, Imp {}, Just d):args) bnd

55− | Just d' <- d

56 = text "(implicit)" <+>

59 = text "(implicit)" <+>

57 bindingOf n True <+> colon <+>

60 bindingOf n True <+> colon <+>

58− pprintPTerm imp bnd ty <>

61+ pprintPTerm imp bnd [] ty <>

59− showDoc d' <> line

62+ showDoc d <> line

60 :

63 :

61 showArgs args ((n, True):bnd)

64 showArgs args ((n, True):bnd)

62 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

65 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)

src/Idris/Prover.hs+5−5

@@ -104,7 +104,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

104 where

105 showImplicits = opt_showimp (idris_options ist)

106

107− tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t

107+ tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t

108

109 assumptionNames :: Env -> [Name]

110 assumptionNames = map fst

@@ -236,8 +236,8 @@ ploop fn d prompt prf e h

236 TType _ ->

237 ihPrintTermWithType h (prettyImp imp PType) type1Doc

238 _ -> let bnd = map (\x -> (fst x, False)) env in

239− ihPrintTermWithType h (pprintPTerm imp bnd (delab ist tm))

239+ ihPrintTermWithType h (pprintPTerm imp bnd [] (delab ist tm))

240− (pprintPTerm imp bnd (delab ist ty))

240+ (pprintPTerm imp bnd [] (delab ist ty))

241 putIState ist

242 return (False, e, False, prf))

243 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -254,8 +254,8 @@ ploop fn d prompt prf e h

254 let tm' = force (normaliseAll ctxt' env tm)

255 ty' = force (normaliseAll ctxt' env ty)

256 imp = opt_showimp (idris_options ist')

257− tmDoc = pprintPTerm imp bnd (delab ist' tm')

257+ tmDoc = pprintPTerm imp bnd [] (delab ist' tm')

258− tyDoc = pprintPTerm imp bnd (delab ist' ty')

258+ tyDoc = pprintPTerm imp bnd [] (delab ist' ty')

259 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

260 putIState ist

261 return (False, e, False, prf))

src/Idris/REPL.hs+1−1

@@ -518,7 +518,7 @@ process h fn (Check (PRef _ n))

518 annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>

519 align (tPretty bnd ist g)

520

521− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t

521+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

522

523

524process h fn (Check t)