@@ -973,30 +973,34 @@ process fn Universes
973 OK _ -> iPrintResult "Universes OK"
973 OK _ -> iPrintResult "Universes OK"
974process fn (Defn n)
974process fn (Defn n)
975 = do i <- getIState
975 = do i <- getIState
976− iputStrLn "Compiled patterns:\n"
976+ let head = text "Compiled patterns:" <$>
977− iputStrLn $ show (lookupDef n (tt_ctxt i))
977+ text (show (lookupDef n (tt_ctxt i)))
978− case lookupCtxt n (idris_patdefs i) of
979+ case lookupCtxt n (idris_patdefs i) of
979− [] -> return ()
980+ [] -> empty
980− [(d, _)] -> do iputStrLn "Original definiton:\n"
981+ [(d, _)] -> text "Original definiton:" <$>
981− mapM_ (printCase i) d
982+ vsep (map (printCase i) d)
982− case lookupTotal n (tt_ctxt i) of
984+ case lookupTotal n (tt_ctxt i) of
983− [t] -> iputStrLn (showTotal t i)
985+ [t] -> showTotal t i
984− _ -> return ()
986+ _ -> empty
987+ iRenderResult $ vsep [head, defs, tot]
985 where printCase i (_, lhs, rhs)
988 where printCase i (_, lhs, rhs)
986 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
989 = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
987− in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
990+ in text (showTm i' (delab i lhs)) <+> text "=" <+>
988− showTm i' (delab i rhs))
991+ text (showTm i' (delab i rhs))
989process fn (TotCheck n)
992process fn (TotCheck n)
990− = do i <- getIState
993+ = do i <- getIState
991− case lookupNameTotal n (tt_ctxt i) of
994+ case lookupNameTotal n (tt_ctxt i) of
992− [] -> iPrintError $ "Unknown operator " ++ show n
995+ [] -> iPrintError $ "Unknown operator " ++ show n
993− ts -> do ist <- getIState
996+ ts -> do ist <- getIState
994− c <- colourise
997+ c <- colourise
995− let ppo = ppOptionIst ist
998+ let ppo = ppOptionIst ist
999+ let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
996− let showN = showName (Just ist) [] ppo c
1000+ showName (Just ist) [] ppo False n
997− iPrintResult . concat . intersperse "\n" .
1001+ iRenderResult . vsep .
998− map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
1002+ map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $
1001process fn (DebugUnify l r)
1005process fn (DebugUnify l r)
1002 = do (ltm, _) <- elabVal recinfo ERHS l
1006 = do (ltm, _) <- elabVal recinfo ERHS l
@@ -1343,13 +1347,22 @@ process fn (PPrint fmt width t)
1343 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
1347 iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
1346−showTotal :: Totality -> IState -> String
1350+showTotal :: Totality -> IState -> Doc OutputAnnotation
1347showTotal t@(Partial (Other ns)) i
1351showTotal t@(Partial (Other ns)) i
1348− = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
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) $
1349−showTotal t i = show t
1360+showTotal t i = text (show t)
1362+showTotalN :: IState -> Name -> Doc OutputAnnotation
1350showTotalN i n = case lookupTotal n (tt_ctxt i) of
1363showTotalN i n = case lookupTotal n (tt_ctxt i) of
1351 [t] -> showTotal t i
1364 [t] -> showTotal t i
1352− _ -> ""
1365+ _ -> empty
1354displayHelp = let vstr = showVersion version in
1367displayHelp = let vstr = showVersion version in
1355 "\nIdris version " ++ vstr ++ "\n" ++
1368 "\nIdris version " ++ vstr ++ "\n" ++