@@ -81,7 +81,7 @@ import Control.Concurrent.MVar
81import Network
81import Network
82import Control.Concurrent
82import Control.Concurrent
83import Data.Maybe
83import Data.Maybe
84−import Data.List
84+import Data.List hiding (group)
85import Data.Char
85import Data.Char
86import Data.Version
86import Data.Version
87import Data.Word (Word)
87import Data.Word (Word)
@@ -1180,16 +1180,18 @@ process fn (PrintDef n) =
1180 where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1180 where ppDef :: IState -> (Name, ([([Name], Term, Term)], [PTerm])) -> Doc OutputAnnotation
1181 ppDef ist (n, (clauses, missing)) =
1181 ppDef ist (n, (clauses, missing)) =
1182 prettyName True True [] n <+> colon <+>
1182 prettyName True True [] n <+> colon <+>
1183− pprintPTerm (ppOptionIst ist) [] [] [] (delabTy ist n) <$>
1183+ align (pprintDelabTy ist n) <$>
1184 indent 2 (ppClauses ist clauses <> ppMissing missing)
1184 indent 2 (ppClauses ist clauses <> ppMissing missing)
1185 ppClauses ist [] = text "No clauses."
1185 ppClauses ist [] = text "No clauses."
1186 ppClauses ist cs = vsep (map pp cs)
1186 ppClauses ist cs = vsep (map pp cs)
1187 where pp (vars, lhs, rhs) =
1187 where pp (vars, lhs, rhs) =
1188+ let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .
1188− let ppTm = pprintPTerm (ppOptionIst ist)
1189+ pprintPTerm (ppOptionIst ist)
1189− (zip vars (repeat False))
1190+ (zip vars (repeat False))
1190− [] [] .
1191+ [] [] .
1191− delab ist
1192+ delab ist $
1192− in ppTm lhs <+> text "=" <+> ppTm rhs
1194+ in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)
1193 ppMissing _ = empty
1195 ppMissing _ = empty