0663f4d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1183 from pminten/ppopt

0663f4dEdwin Brady12 years ago

src/Idris/AbsSyntaxTree.hs+73−51

compare with master

unifiedsplit

@@ -95,6 +95,28 @@ defaultOpts = IOption { opt_logLevel = 0

95 , opt_autoSolve = True

96 }

98+data PPOption = PPOption {

99+ ppopt_impl :: Bool -- ^^ whether to show implicits

100+} deriving (Show)

101+

102+-- | Pretty printing options with default verbosity.

103+defaultPPOption :: PPOption

104+defaultPPOption = PPOption { ppopt_impl = False }

105+

106+-- | Pretty printing options with the most verbosity.

107+verbosePPOption :: PPOption

108+verbosePPOption = PPOption { ppopt_impl = True }

109+

110+-- | Get pretty printing options from the big options record.

111+ppOption :: IOption -> PPOption

112+ppOption opt = PPOption {

113+ ppopt_impl = opt_showimp opt

114+}

115+

116+-- | Get pretty printing options from an idris state record.

117+ppOptionIst :: IState -> PPOption

118+ppOptionIst = ppOption . idris_options

119+

98data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

121

100-- | The output mode in use

122-- | The output mode in use

@@ -1089,19 +1111,19 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

1089-- could interfere with interactive editing, which calls "show".

1111-- could interfere with interactive editing, which calls "show".

1090

1112

1091instance Show PTerm where

1113instance Show PTerm where

1092− showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm

1114+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm

1093

1115

1094instance Show PDecl where

1116instance Show PDecl where

1095− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d

1117+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d

1096

1118

1097instance Show PClause where

1119instance Show PClause where

1098− showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c

1120+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c

1099

1121

1100instance Show PData where

1122instance Show PData where

1101− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d

1123+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d

1102

1124

1103instance Pretty PTerm OutputAnnotation where

1125instance Pretty PTerm OutputAnnotation where

1104− pretty = prettyImp False

1126+ pretty = prettyImp defaultPPOption

1105

1127

1106-- | Colourise annotations according to an Idris state. It ignores the names

1128-- | Colourise annotations according to an Idris state. It ignores the names

1107-- in the annotation, as there's no good way to show extended information on a

1129-- in the annotation, as there's no good way to show extended information on a

@@ -1129,23 +1151,23 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1129 colour ItalicText = IdrisColour Nothing True False False True

1151 colour ItalicText = IdrisColour Nothing True False False True

1130

1152

1131-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1153-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1132−prettyImp :: Bool -- ^^ whether to show implicits

1154+prettyImp :: PPOption -- ^^ pretty printing options

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

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

1134 -> Doc OutputAnnotation

1156 -> Doc OutputAnnotation

1135prettyImp impl = pprintPTerm impl [] [] []

1157prettyImp impl = pprintPTerm impl [] [] []

1136

1158

1137-- | Do the right thing for rendering a term in an IState

1159-- | Do the right thing for rendering a term in an IState

1138prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1160prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1139−prettyIst ist = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist)

1161+prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

1140

1162

1141-- | Pretty-print a high-level Idris term in some bindings context with infix info

1163-- | Pretty-print a high-level Idris term in some bindings context with infix info

1142−pprintPTerm :: Bool -- ^^ whether to show implicits

1164+pprintPTerm :: PPOption -- ^^ pretty printing options

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

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

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

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

1145 -> [FixDecl] -- ^^ Fixity declarations

1167 -> [FixDecl] -- ^^ Fixity declarations

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

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

1147 -> Doc OutputAnnotation

1169 -> Doc OutputAnnotation

1148−pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1170+pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1149 where

1171 where

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

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

1151 prettySe p bnd (PQuote r) =

1173 prettySe p bnd (PQuote r) =

@@ -1154,7 +1176,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1154 prettySe p bnd e

1176 prettySe p bnd e

1155 | Just str <- slist p bnd e = str

1177 | Just str <- slist p bnd e = str

1156 | Just n <- snat p e = annotate AnnConstData (text (show n))

1178 | Just n <- snat p e = annotate AnnConstData (text (show n))

1157− prettySe p bnd (PRef fc n) = prettyName impl bnd n

1179+ prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n

1158 prettySe p bnd (PLam n ty sc) =

1180 prettySe p bnd (PLam n ty sc) =

1159 bracket p 2 . group . align . hang 2 $

1181 bracket p 2 . group . align . hang 2 $

1160 text "\\" <> bindingOf n False <+> text "=>" <$>

1182 text "\\" <> bindingOf n False <+> text "=>" <$>

@@ -1165,7 +1187,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

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

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

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

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

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

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

1168− | n `elem` allNamesIn sc || impl || n `elem` docArgs =

1190+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1169 bracket p 2 . group $

1191 bracket p 2 . group $

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

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

1171 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

@@ -1178,7 +1200,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1178 Static -> text "[static]" <> space

1200 Static -> text "[static]" <> space

1179 _ -> empty

1201 _ -> empty

1180 prettySe p bnd (PPi (Imp l s _) n ty sc)

1202 prettySe p bnd (PPi (Imp l s _) n ty sc)

1181− | impl =

1203+ | ppopt_impl ppo =

1182 bracket p 2 $

1204 bracket p 2 $

1183 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1205 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1184 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1206 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1197,16 +1219,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1197 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1219 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1198 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1220 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1199 | UN nm <- basename f

1221 | UN nm <- basename f

1222+ , not (ppopt_impl ppo) && null (getExps args) =

1200− , not impl && null (getExps args) = if isAlpha (thead nm)

1223+ if isAlpha (thead nm)

1201− then prettyName impl bnd f

1224+ then prettyName (ppopt_impl ppo) bnd f

1202− else enclose lparen rparen $

1225+ else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f

1203− prettyName impl bnd f

1204 prettySe p bnd (PAppBind _ (PRef _ f) [])

1226 prettySe p bnd (PAppBind _ (PRef _ f) [])

1205− | not impl = text "!" <> prettyName impl bnd f

1227+ | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f

1206 prettySe p bnd (PApp _ (PRef _ op) args)

1228 prettySe p bnd (PApp _ (PRef _ op) args)

1207 | UN nm <- basename op

1229 | UN nm <- basename op

1208 , not (tnull nm) &&

1230 , not (tnull nm) &&

1209− (not impl) && (not $ isAlpha (thead nm)) =

1231+ (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1210 case getExps args of

1232 case getExps args of

1211 [] -> enclose lparen rparen opName

1233 [] -> enclose lparen rparen opName

1212 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

1234 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

@@ -1215,7 +1237,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1215 (l:r:rest) -> bracket p 1 $

1237 (l:r:rest) -> bracket p 1 $

1216 enclose lparen rparen (inFix l r) <+>

1238 enclose lparen rparen (inFix l r) <+>

1217 align (group (vsep (map (prettyArgSe bnd) rest)))

1239 align (group (vsep (map (prettyArgSe bnd) rest)))

1218− where opName = prettyName impl bnd op

1240+ where opName = prettyName (ppopt_impl ppo) bnd op

1219 f = getFixity (opStr op)

1241 f = getFixity (opStr op)

1220 left l = case f of

1242 left l = case f of

1221 Nothing -> prettySe (-1) bnd l

1243 Nothing -> prettySe (-1) bnd l

@@ -1235,7 +1257,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1235 fp = prettySe 1 bnd f

1257 fp = prettySe 1 bnd f

1236 in

1258 in

1237 bracket p 1 . group $

1259 bracket p 1 . group $

1238− if impl

1260+ if ppopt_impl ppo

1239 then if null as

1261 then if null as

1240 then fp

1262 then fp

1241 else fp <+> align (vsep (map (prettyArgS bnd) as))

1263 else fp <+> align (vsep (map (prettyArgS bnd) as))

@@ -1340,9 +1362,9 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1340 basename n = n

1362 basename n = n

1341

1363

1342 slist' p bnd (PApp _ (PRef _ nil) _)

1364 slist' p bnd (PApp _ (PRef _ nil) _)

1343− | not impl && nsroot nil == sUN "Nil" = Just []

1365+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1344 slist' p bnd (PRef _ nil)

1366 slist' p bnd (PRef _ nil)

1345− | not impl && nsroot nil == sUN "Nil" = Just []

1367+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1346 slist' p bnd (PApp _ (PRef _ cons) args)

1368 slist' p bnd (PApp _ (PRef _ cons) args)

1347 | nsroot cons == sUN "::",

1369 | nsroot cons == sUN "::",

1348 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

1370 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

@@ -1415,43 +1437,43 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

1415 strName other = show other

1437 strName other = show other

1416

1438

1417

1439

1418−showCImp :: Bool -> PClause -> Doc OutputAnnotation

1440+showCImp :: PPOption -> PClause -> Doc OutputAnnotation

1419−showCImp impl (PClause _ n l ws r w)

1441+showCImp ppo (PClause _ n l ws r w)

1420− = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

1442+ = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r

1421 <+> text "where" <+> text (show w)

1443 <+> text "where" <+> text (show w)

1422 where

1444 where

1423 showWs [] = empty

1445 showWs [] = empty

1424− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1446+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1425−showCImp impl (PWith _ n l ws r w)

1447+showCImp ppo (PWith _ n l ws r w)

1426− = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

1448+ = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

1427 <+> braces (text (show w))

1449 <+> braces (text (show w))

1428 where

1450 where

1429 showWs [] = empty

1451 showWs [] = empty

1430− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1452+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1431

1453

1432

1454

1433−showDImp :: Bool -> PData -> Doc OutputAnnotation

1455+showDImp :: PPOption -> PData -> Doc OutputAnnotation

1434−showDImp impl (PDatadecl n ty cons)

1456+showDImp ppo (PDatadecl n ty cons)

1435− = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1457+ = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>

1436− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1458+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))

1437

1459

1438−showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1460+showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

1439−showDecls i ds = vsep (map (showDeclImp i) ds)

1461+showDecls o ds = vsep (map (showDeclImp o) ds)

1440

1462

1441showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1463showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1442−showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1464+showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1443−showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1465+showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1444− indent 2 (vsep (map (showCImp i) cs))

1466+ indent 2 (vsep (map (showCImp o) cs))

1445−showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1467+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

1446−showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1468+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1447−showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1469+showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

1448showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1470showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1449−showDeclImp i (PClass _ _ _ cs n ps _ ds)

1471+showDeclImp o (PClass _ _ _ cs n ps _ ds)

1450− = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

1472+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1451−showDeclImp i (PInstance _ _ cs n _ t _ ds)

1473+showDeclImp o (PInstance _ _ cs n _ t _ ds)

1452− = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

1474+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

1453showDeclImp _ _ = text "..."

1475showDeclImp _ _ = text "..."

1454−-- showDeclImp (PImport i) = "import " ++ i

1476+-- showDeclImp (PImport o) = "import " ++ o

1455

1477

1456instance Show (Doc OutputAnnotation) where

1478instance Show (Doc OutputAnnotation) where

1457 show = flip (displayS . renderCompact) ""

1479 show = flip (displayS . renderCompact) ""

@@ -1478,14 +1500,14 @@ getAll = map getTm

1478-- | Show Idris name

1500-- | Show Idris name

1479showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1501showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1480 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1502 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1481− -> Bool -- ^^ whether to show implicits

1503+ -> PPOption -- ^^ pretty printing options

1482 -> Bool -- ^^ whether to colourise

1504 -> Bool -- ^^ whether to colourise

1483 -> Name -- ^^ the term to show

1505 -> Name -- ^^ the term to show

1484 -> String

1506 -> String

1485−showName ist bnd impl colour n = case ist of

1507+showName ist bnd ppo colour n = case ist of

1486 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1508 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

1487 Nothing -> showbasic n

1509 Nothing -> showbasic n

1488− where name = if impl then show n else showbasic n

1510+ where name = if ppopt_impl ppo then show n else showbasic n

1489 showbasic n@(UN _) = showCG n

1511 showbasic n@(UN _) = showCG n

1490 showbasic (MN _ s) = str s

1512 showbasic (MN _ s) = str s

1491 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

1513 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

@@ -1509,11 +1531,11 @@ showTm :: IState -- ^^ the Idris state, for information about identifiers and co

1509 -> String

1531 -> String

1510showTm ist = displayDecorated (consoleDecorate ist) .

1532showTm ist = displayDecorated (consoleDecorate ist) .

1511 renderPretty 0.8 100000 .

1533 renderPretty 0.8 100000 .

1512− prettyImp (opt_showimp (idris_options ist))

1534+ prettyImp (ppOptionIst ist)

1513

1535

1514-- | Show a term with implicits, no colours

1536-- | Show a term with implicits, no colours

1515showTmImpls :: PTerm -> String

1537showTmImpls :: PTerm -> String

1516−showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

1538+showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

1517

1539

1518

1540

1519instance Sized PTerm where

1541instance Sized PTerm where

src/Idris/Delaborate.hs+2−2

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

138pprintTerm ist = pprintTerm' ist []

139

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

141−pprintTerm' ist bnd = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist)

141+pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

142

143pprintErr :: IState -> Err -> Doc OutputAnnotation

144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>

269

270

271showqual :: IState -> Name -> String

272−showqual i n = showName (Just i) [] False False (dens n)

272+showqual i n = showName (Just i) [] (ppOptionIst i) { ppopt_impl = False } False (dens n)

273 where

274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of

275 [_] -> n -- just one thing

src/Idris/Docs.hs+9−9

@@ -36,8 +36,8 @@ showDoc d | nullDocstring d = empty

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

38pprintFD ist (FD n doc args ty f)

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

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

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

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

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

42 renderDocstring doc <$>

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

@@ -46,23 +46,23 @@ pprintFD ist (FD n doc args ty f)

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

47 else empty)

49− where imp = opt_showimp (idris_options ist)

49+ where ppo = ppOptionIst ist

50 infixes = idris_infixes ist

51 showArgs ((n, ty, Exp {}, Just d):args) bnd

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

53− pprintPTerm imp bnd [] infixes ty <>

53+ pprintPTerm ppo bnd [] infixes ty <>

54 showDoc d <> line

55 :

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

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

58 = text "Class constraint" <+>

59− pprintPTerm imp bnd [] infixes ty <> showDoc d <> line

59+ pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line

60 :

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

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

63 = text "(implicit)" <+>

64 bindingOf n True <+> colon <+>

65− pprintPTerm imp bnd [] infixes ty <>

65+ pprintPTerm ppo bnd [] infixes ty <>

66 showDoc d <> line

67 :

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

@@ -77,7 +77,7 @@ pprintDocs ist (DataDoc t args)

77 nest 4 (text "Constructors:" <> line <>

78 vsep (map (pprintFD ist) args))

79pprintDocs ist (ClassDoc n doc meths params instances)

80− = nest 4 (text "Type class" <+> prettyName imp [] n <>

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

81 if nullDocstring doc then empty else line <> renderDocstring doc)

82 <> line <$>

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

@@ -97,11 +97,11 @@ pprintDocs ist (ClassDoc n doc meths params instances)

98 pNames = map fst params

100− imp = opt_showimp (idris_options ist)

100+ ppo = ppOptionIst ist

101 infixes = idris_infixes ist

102

103 dumpInstance :: PTerm -> Doc OutputAnnotation

104− dumpInstance = pprintPTerm imp params' [] infixes

104+ dumpInstance = pprintPTerm ppo params' [] infixes

105

106 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

107 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

src/Idris/ElabDecls.hs+3−3

@@ -393,7 +393,7 @@ elabEliminator paramPos n ty cons info = do

393 elimLog elimSig

394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

396− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

396+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

398 -- Do not elaborate clauses if there aren't any

399 case eliminatorClauses of

@@ -1863,7 +1863,7 @@ elabClass info syn doc fc constraints tn ps pDocs ds

1863 constraint

1864 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

1865 let ddecl = PDatadecl tn tty cons

1866− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1866+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

1867 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

1868 -- for each constraint, build a top level function to chase it

1869 logLvl 5 $ "Building functions"

@@ -2059,7 +2059,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

2059 let wbTys = map mkTyDecl mtys

2060 let wbVals = map (decorateid (decorate ns iname)) ds'

2061 let wb = wbTys ++ wbVals

2062− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

2062+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

2063 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

2064 show (concat (nub wparams))

2065

src/Idris/IdrisDoc.hs+1−1

@@ -457,7 +457,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

457

458 where

459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names (idris_infixes ist) ftype

460+ signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype

461 names = [ n | (n@(UN n'), _, _, _) <- args,

462 not (T.isPrefixOf (txt "__") n') ]

463

src/Idris/Output.hs+6−6

@@ -88,16 +88,16 @@ ihPrintTermWithType h tm ty = do ist <- getIState

88-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

89ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

90ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

91−ihPrintFunTypes h bnd n overloads = do imp <- impShow

91+ihPrintFunTypes h bnd n overloads = do ist <- getIState

92− ist <- getIState

92+ let ppo = ppOptionIst ist

93 let infixes = idris_infixes ist

94− let output = vsep (map (uncurry (ppOverload imp infixes)) overloads)

94+ let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

95 case idris_outputmode ist of

96 RawOutput -> consoleDisplayAnnotated h output

97 IdeSlave n -> ideSlaveReturnAnnotated n h output

98 where fullName n = prettyName True bnd n

99− ppOverload imp infixes n tm =

99+ ppOverload ppo infixes n tm =

100− fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)

100+ fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

101

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

103ihRenderResult h d = do ist <- getIState

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

123 out = displayS . renderPretty 1.0 50 $ renderDocstring o

124 return (out "")

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

126− getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist) $

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

127 delabTy ist n

128 in (displayS . renderPretty 1.0 50 $ theTy) ""

129fancifyAnnots _ annot = annot

src/Idris/Parser.hs+1−1

@@ -1248,7 +1248,7 @@ loadSource h lidr f

1248 -- Parsing done, now process declarations

1249

1250 let ds = namespaces mname ds'

1251− logLvl 3 (show $ showDecls True ds)

1251+ logLvl 3 (show $ showDecls verbosePPOption ds)

1252 i <- getIState

1253 logLvl 10 (show (toAlist (idris_implicits i)))

1254 logLvl 3 (show (idris_infixes i))

src/Idris/Prover.hs+9−9

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

110 iputGoal rendered

111

112 where

113− showImplicits = opt_showimp (idris_options ist)

113+ ppo = ppOptionIst ist

114

115− tPretty bnd t = pprintPTerm showImplicits bnd [] (idris_infixes ist) $ delab ist t

115+ tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t

116

117 assumptionNames :: Env -> [Name]

118 assumptionNames = map fst

@@ -237,16 +237,16 @@ ploop fn d prompt prf e h

237 ctxt' = envCtxt env ctxt

238 putIState ist { tt_ctxt = ctxt' }

239 (tm, ty) <- elabVal toplevel False t

240− let imp = opt_showimp (idris_options ist)

240+ let ppo = ppOptionIst ist

241 ty' = normaliseC ctxt [] ty

242 h = idris_outh ist

243 infixes = idris_infixes ist

244 case tm of

245 TType _ ->

246− ihPrintTermWithType h (prettyImp imp PType) type1Doc

246+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

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

248− ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))

248+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

249− (pprintPTerm imp bnd [] infixes (delab ist ty))

249+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

250 putIState ist

251 return (False, e, False, prf))

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

@@ -262,10 +262,10 @@ ploop fn d prompt prf e h

262 (tm, ty) <- elabVal toplevel False t

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

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

265− imp = opt_showimp (idris_options ist')

265+ ppo = ppOption (idris_options ist')

266 infixes = idris_infixes ist

267− tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')

267+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

268− tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')

268+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

270 putIState ist

271 return (False, e, False, prf))

src/Idris/REPL.hs+23−24

@@ -312,34 +312,34 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

313 do ist <- getIState

314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

315− imp <- impShow

315+ let ppo = ppOptionIst ist

316 let mvarTys = map (delabTy ist) mvs

317 let res = (IdeSlave.SymbolAtom "ok",

318 zipWith (\ n (prems, concl) -> (n, prems, concl))

319 (map (IdeSlave.StringAtom . show) mvs)

320− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

320+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))

321 runIO . putStrLn $ IdeSlave.convSExp "return" res id

322 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

323 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

324 in ((n, t):prems, conc)

325 getGoal tm = ([], tm)

326− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

326+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)

327 -> ([(String, String, SpanList OutputAnnotation)],

328 (String, SpanList OutputAnnotation))

329− sexpGoal ist cols imp ns ([], concl) =

329+ sexpGoal ist cols ppo ns ([], concl) =

330 let infixes = idris_infixes ist

331 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

332− pprintPTerm imp (zip ns (repeat False)) [] infixes concl

332+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl

333 in ([], concl')

334− sexpGoal ist cols imp ns ((n, t):ps, concl) =

334+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =

335 let n' = case n of

336 NS (UN nm) ns -> str nm

337 UN nm | ('_':'_':_) <- str nm -> "_"

338 | otherwise -> str nm

339 _ -> "_"

340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

341− pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t

341+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t

342− rest = sexpGoal ist cols imp (n:ns) (ps, concl)

342+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)

343 in ((n', t', spans) : fst rest, snd rest)

344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

345 case splitName n of

@@ -581,21 +581,21 @@ process h fn (ExecVal t)

581process h fn (Check (PRef _ n))

582 = do ctxt <- getContext

583 ist <- getIState

584− imp <- impShow

584+ let ppo = ppOptionIst ist

585 case lookupNames n ctxt of

586 ts@(t:_) ->

587 case lookup t (idris_metavars ist) of

588 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

589− showMetavarInfo imp ist n i

589+ showMetavarInfo ppo ist n i

590 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

591 [] -> ihPrintError h $ "No such variable " ++ show n

592 where

593− showMetavarInfo imp ist n i

593+ showMetavarInfo ppo ist n i

594 = case lookupTy n (tt_ctxt ist) of

595− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))

595+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

596− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

596+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

597− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

597+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

598− putTy imp ist i bnd (PPi _ n t sc)

598+ putTy ppo ist i bnd (PPi _ n t sc)

599 = let current = text " " <>

600 (case n of

601 MN _ _ -> text "_"

@@ -603,21 +603,21 @@ process h fn (Check (PRef _ n))

603 _ -> bindingOf n False) <+>

604 colon <+> align (tPretty bnd ist t) <> line

605 in

606− current <> putTy imp ist (i-1) ((n,False):bnd) sc

606+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc

607− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

607+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc

608− putGoal imp ist bnd g

608+ putGoal ppo ist bnd g

609 = text "--------------------------------------" <$>

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

611 align (tPretty bnd ist g)

612

613− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t

613+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

614

615

616process h fn (Check t)

617 = do (tm, ty) <- elabVal toplevel False t

618 ctxt <- getContext

619 ist <- getIState

620− let imp = opt_showimp (idris_options ist)

620+ let ppo = ppOptionIst ist

621 ty' = normaliseC ctxt [] ty

622 case tm of

623 TType _ ->

@@ -664,8 +664,8 @@ process h fn (TotCheck n)

664 [] -> ihPrintError h $ "Unknown operator " ++ show n

665 ts -> do ist <- getIState

666 c <- colourise

667− imp <- impShow

667+ let ppo = ppOptionIst ist

668− let showN = showName (Just ist) [] imp c

668+ let showN = showName (Just ist) [] ppo c

669 ihPrintResult h . concat . intersperse "\n" .

670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

671 ts

@@ -825,7 +825,7 @@ process h fn (DoProofSearch updatefile rec l n hints)

825 ctxt <- getContext

826 i <- getIState

827 return . flip displayS "" . renderPretty 1.0 80 $

828− pprintPTerm False [] [] (idris_infixes i)

828+ pprintPTerm defaultPPOption [] [] (idris_infixes i)

829 (stripNS

830 (dropCtxt envlen

831 (delab i (specialise ctxt [] [(mn, 1)] tm)))))

@@ -958,7 +958,6 @@ process h fn (TestInline t)

958 ctxt <- getContext

959 ist <- getIState

960 let tm' = inlineTerm ist tm

961− imp <- impShow

962 c <- colourise

961 c <- colourise

963 iPrintResult (showTm ist (delab ist tm'))

962 iPrintResult (showTm ist (delab ist tm'))

964process h fn Execute

963process h fn Execute