From 0696537cc2d9a9e423de22bef48a4329163aff64 Mon Sep 17 00:00:00 2001
From: David Raymond Christiansen <david@davidchristiansen.dk>
Date: Mon, 18 May 2015 16:21:51 +0200
Subject: [PATCH 1/2] Fix display of output from :total

Now, the pretty-printer is used, which makes it look non-horrible in IDE
clients as well as get semantic highlighting.
---
 src/Idris/REPL.hs       | 51 ++++++++++++++++++++++++++---------------
 test/interactive005/run |  2 +-
 2 files changed, 33 insertions(+), 20 deletions(-)

diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
index 8a68fc844f..a4d28be437 100644
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -973,19 +973,22 @@ process fn Universes
                             OK _ -> iPrintResult "Universes OK"
 process fn (Defn n)
                     = do i <- getIState
-                         iputStrLn "Compiled patterns:\n"
-                         iputStrLn $ show (lookupDef n (tt_ctxt i))
-                         case lookupCtxt n (idris_patdefs i) of
-                            [] -> return ()
-                            [(d, _)] -> do iputStrLn "Original definiton:\n"
-                                           mapM_ (printCase i) d
-                         case lookupTotal n (tt_ctxt i) of
-                            [t] -> iputStrLn (showTotal t i)
-                            _ -> return ()
+                         let head = text "Compiled patterns:" <$>
+                                    text (show (lookupDef n (tt_ctxt i)))
+                         let defs =
+                              case lookupCtxt n (idris_patdefs i) of
+                                [] -> empty
+                                [(d, _)] -> text "Original definiton:" <$>
+                                            vsep (map (printCase i) d)
+                         let tot =
+                              case lookupTotal n (tt_ctxt i) of
+                                 [t] -> showTotal t i
+                                 _ -> empty
+                         iRenderResult $ vsep [head, defs, tot]
     where printCase i (_, lhs, rhs)
              = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
-               in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
-                             showTm i' (delab i rhs))
+               in text (showTm i' (delab i lhs)) <+> text "=" <+>
+                  text (showTm i' (delab i rhs))
 process fn (TotCheck n)
                         = do i <- getIState
                              case lookupNameTotal n (tt_ctxt i) of
@@ -993,10 +996,11 @@ process fn (TotCheck n)
                                 ts  -> do ist <- getIState
                                           c <- colourise
                                           let ppo =  ppOptionIst ist
-                                          let showN = showName (Just ist) [] ppo c
-                                          iPrintResult . concat . intersperse "\n" .
-                                            map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $
-                                            ts
+                                          let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
+                                                        showName (Just ist) [] ppo False n
+                                          iRenderResult . vsep .
+                                           map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $
+                                           ts
 
 process fn (DebugUnify l r)
    = do (ltm, _) <- elabVal recinfo ERHS l
@@ -1343,13 +1347,22 @@ process fn (PPrint fmt width t)
         iPrintResult =<< renderExternal fmt width (pprintDelab ist tm)
 
 
-showTotal :: Totality -> IState -> String
+showTotal :: Totality -> IState -> Doc OutputAnnotation
 showTotal t@(Partial (Other ns)) i
-   = show t ++ "\n\t" ++ showSep "\n\t" (map (showTotalN i) ns)
-showTotal t i = show t
+   = text "possibly not total due to:" <$>
+     vsep (map (showTotalN i) ns)
+showTotal t@(Partial (Mutual ns)) i
+   = text "possibly not total due to recursive path:" <$>
+     align (group (vsep (punctuate comma
+       (map (\n -> annotate (AnnName n Nothing Nothing Nothing) $
+                   text (show n))
+            ns))))
+showTotal t i = text (show t)
+
+showTotalN :: IState -> Name -> Doc OutputAnnotation
 showTotalN i n = case lookupTotal n (tt_ctxt i) of
                         [t] -> showTotal t i
-                        _ -> ""
+                        _ -> empty
 
 displayHelp = let vstr = showVersion version in
               "\nIdris version " ++ vstr ++ "\n" ++
diff --git a/test/interactive005/run b/test/interactive005/run
index 311fa1c520..5bd96feade 100755
--- a/test/interactive005/run
+++ b/test/interactive005/run
@@ -1,5 +1,5 @@
 #!/usr/bin/env bash
-idris --nocolour --quiet interactive005.idr < input
+idris --nocolour --quiet interactive005.idr --consolewidth 70 < input
 rm -f *.ibc
 rm -f hello.bytecode
 rm -f hello

From b643b7a9837a361f1c7aa1d7ad40cb5e1633a08c Mon Sep 17 00:00:00 2001
From: David Raymond Christiansen <david@davidchristiansen.dk>
Date: Mon, 18 May 2015 16:33:21 +0200
Subject: [PATCH 2/2] Indentation improvement

---
 src/Idris/REPL.hs | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
index a4d28be437..704bd94df7 100644
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -990,17 +990,17 @@ process fn (Defn n)
                in text (showTm i' (delab i lhs)) <+> text "=" <+>
                   text (showTm i' (delab i rhs))
 process fn (TotCheck n)
-                        = do i <- getIState
-                             case lookupNameTotal n (tt_ctxt i) of
-                                []  -> iPrintError $ "Unknown operator " ++ show n
-                                ts  -> do ist <- getIState
-                                          c <- colourise
-                                          let ppo =  ppOptionIst ist
-                                          let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
-                                                        showName (Just ist) [] ppo False n
-                                          iRenderResult . vsep .
-                                           map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $
-                                           ts
+   = do i <- getIState
+        case lookupNameTotal n (tt_ctxt i) of
+           []  -> iPrintError $ "Unknown operator " ++ show n
+           ts  -> do ist <- getIState
+                     c <- colourise
+                     let ppo =  ppOptionIst ist
+                     let showN n = annotate (AnnName n Nothing Nothing Nothing) . text $
+                                   showName (Just ist) [] ppo False n
+                     iRenderResult . vsep .
+                      map (\(n, t) -> hang 4 $ showN n <+> text "is" <+> showTotal t i) $
+                      ts
 
 process fn (DebugUnify l r)
    = do (ltm, _) <- elabVal recinfo ERHS l