@@ -973,30 +973,34 @@ process fn Universes
973973 OK _ -> iPrintResult "Universes OK"
974974process fn (Defn n)
975975 = do i <- getIState
976− iputStrLn "Compiled patterns:\n"
977− iputStrLn $ show (lookupDef n (tt_ctxt i))
978− case lookupCtxt n (idris_patdefs i) of
979− [] -> return ()
980− [(d, _)] -> do iputStrLn "Original definiton:\n"
981− mapM_ (printCase i) d
982− case lookupTotal n (tt_ctxt i) of
983− [t] -> iputStrLn (showTotal t i)
984− _ -> return ()
976+ let head = text "Compiled patterns:" <$>
977+ text (show (lookupDef n (tt_ctxt i)))
978+ let defs =
979+ case lookupCtxt n (idris_patdefs i) of
980+ [] -> empty
981+ [(d, _)] -> text "Original definiton:" <$>
982+ vsep (map (printCase i) d)
983+ let tot =
984+ case lookupTotal n (tt_ctxt i) of
985+ [t] -> showTotal t i
986+ _ -> empty
987+ iRenderResult $ vsep [head, defs, tot]
985988 where printCase i (_, lhs, rhs)
986989 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
987− in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
988− showTm i' (delab i rhs))
990+ in text (showTm i' (delab i lhs)) <+> text "=" <+>
991+ text (showTm i' (delab i rhs))
989992process fn (TotCheck n)
990− = do i <- getIState
991− case lookupNameTotal n (tt_ctxt i) of
992− [] -> iPrintError $ "Unknown operator " ++ show n
993− ts -> do ist <- getIState
994− c <- colourise
995− let ppo = ppOptionIst ist
996− let showN = showName (Just ist) [] ppo c
997− iPrintResult . concat . intersperse "\n" .
998− map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
999− ts
993+ = do i <- getIState
994+ case lookupNameTotal n (tt_ctxt i) of
995+ [] -> iPrintError $ "Unknown operator " ++ show n
996+ ts -> do ist <- getIState
997+ c <- colourise
998+ let ppo = ppOptionIst ist
999+ let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
1000+ showName (Just ist) [] ppo False n
1001+ iRenderResult . vsep .
1002+ map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $
1003+ ts
10001004
10011005process fn (DebugUnify l r)
10021006 = do (ltm, _) <- elabVal recinfo ERHS l
@@ -1343,13 +1347,22 @@ process fn (PPrint fmt width t)
13431347 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
13441348
13451349
1346−showTotal :: Totality -> IState -> String
1350+showTotal :: Totality -> IState -> Doc OutputAnnotation
13471351showTotal t@(Partial (Other ns)) i
1348− = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
1349−showTotal t i = show t
1352+ = text "possibly not total due to:" <$>
1353+ vsep (map (showTotalN i) ns)
1354+showTotal t@(Partial (Mutual ns)) i
1355+ = text "possibly not total due to recursive path:" <$>
1356+ align (group (vsep (punctuate comma
1357+ (map (\n -> annotate (AnnName n Nothing Nothing Nothing) $
1358+ text (show n))
1359+ ns))))
1360+showTotal t i = text (show t)
1361+
1362+showTotalN :: IState -> Name -> Doc OutputAnnotation
13501363showTotalN i n = case lookupTotal n (tt_ctxt i) of
13511364 [t] -> showTotal t i
1352− _ -> ""
1365+ _ -> empty
13531366
13541367displayHelp = let vstr = showVersion version in
13551368 "\nIdris version " ++ vstr ++ "\n" ++