git.iko.soy/Idris-dev
on master help sign in
Some playing around with widths to make everything look nicer.
368fdf6Dominic Mulligan
src/Idris/AbsSyntax.hs+4−4
compare with master
unifiedsplit
@@ -912,13 +912,13 @@ prettyImp impl = prettySe 10
912 where
912 where
913 fS l r =
913 fS l r =
914 if size r > breakingSize then
914 if size r > breakingSize then
915− l $+$ prettyArgS r
915+ l $+$ nest nestingSize (prettyArgS r)
916 else
916 else
917 l <+> prettyArgS r
917 l <+> prettyArgS r
918
918
919 fSe l r =
919 fSe l r =
920 if size r > breakingSize then
920 if size r > breakingSize then
921− l $+$ prettyArgSe r
921+ l $+$ nest nestingSize (prettyArgSe r)
922 else
922 else
923 l <+> prettyArgSe r
923 l <+> prettyArgSe r
924 prettySe p (PCase _ scr opts) =
924 prettySe p (PCase _ scr opts) =
@@ -935,9 +935,9 @@ prettyImp impl = prettySe 10
935 prettySe p (PEq _ l r) =
935 prettySe p (PEq _ l r) =
936 bracket p 2 $
936 bracket p 2 $
937 if size r > breakingSize then
937 if size r > breakingSize then
938− prettySe 10 l <+> text "=" $+$ prettySe 10 r
938+ prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
939 else
939 else
940− hang (prettySe 10 l <+> text "=") nestingSize $ prettySe 10 r
940+ prettySe 10 l <+> text "=" <+> prettySe 10 r
941 prettySe p (PTyped l r) =
941 prettySe p (PTyped l r) =
942 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
942 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
943 prettySe p (PPair _ l r) =
943 prettySe p (PPair _ l r) =
src/Idris/Prover.hs+1−30
@@ -84,8 +84,7 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
84 prettyG b = tPretty $ binderTy b
84 prettyG b = tPretty $ binderTy b
85
85
86 prettyGoal ty =
86 prettyGoal ty =
87− text "----------" <+> text "Metavariable currently in focus" <> colon
87+ text "---------- Goal: ----------" $$
88− <+> pretty nm <+> text "----------" $$
89 pretty h <> colon $$ nest nestingSize (prettyG ty)
88 pretty h <> colon $$ nest nestingSize (prettyG ty)
90
89
91 prettyAssumptions env =
90 prettyAssumptions env =
@@ -102,34 +101,6 @@ dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
102 text "---------- Other goals: ----------" $$
101 text "---------- Other goals: ----------" $$
103 pretty hs
102 pretty hs
104
103
105−
106−{-
107−dumpState :: IState -> ProofState -> IO ()
108−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
109−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
110− = do let OK ty = goalAtFocus ps
111− let OK env = envAtFocus ps
112−-- putStrLn $ "Other goals: " ++ show hs ++ "\n"
113− putStr $ "\n" ++ showPs (reverse env)
114− putStrLn $ "---------------------------------- (" ++ show nm
115− ++ ") --------"
116− putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
117− where
118− tshow t = show (delab ist t)
119−
120− showPs [] = ""
121− showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs
122− showPs ((n, Let t v) : bs)
123− = " " ++ show n ++ " = " ++ tshow v ++ " : " ++
124− tshow t ++ "\n" ++ showPs bs
125− showPs ((n, b) : bs)
126− = " " ++ show n ++ " : " ++
127− tshow (binderTy b) ++ "\n" ++ showPs bs
128−
129− showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
130− showG b = tshow (binderTy b)
131−-}
132−
133lifte :: ElabState [PDecl] -> ElabD a -> Idris a
104lifte :: ElabState [PDecl] -> ElabD a -> Idris a
134lifte st e = do (v, _) <- elabStep st e
105lifte st e = do (v, _) <- elabStep st e
135 return v
106 return v
src/Util/Pretty.hs+2−2
@@ -18,10 +18,10 @@ instance Sized a => Sized [a] where
18
18
19-- The maximum size before we break on to another line.
19-- The maximum size before we break on to another line.
20breakingSize :: Int
20breakingSize :: Int
21−breakingSize = 14
21+breakingSize = 15
22
22
23nestingSize :: Int
23nestingSize :: Int
24−nestingSize = 2
24+nestingSize = 1
25
25
26class Pretty a where
26class Pretty a where
27 pretty :: a -> Doc
27 pretty :: a -> Doc