Merge pull request #801 from david-christiansen/semantic-pprint

Colour support in the prover + refactoring of pretty-printing vs show

idris.cabal

@@ -434,6 +434,7 @@ Library
 
   Build-depends:  base >=4 && <5
                 , Cabal
+                , annotated-wl-pprint >= 0.5.3
                 , ansi-terminal
                 , ansi-wl-pprint
                 , binary
@@ -463,6 +464,7 @@ Library
                 , zlib
   Extensions:     MultiParamTypeClasses
                 , FunctionalDependencies
+                , FlexibleContexts
                 , FlexibleInstances
                 , TemplateHaskell
 

src/Idris/AbsSyntax.hs

@@ -397,6 +397,55 @@ ihPrintResult h s = do i <- getIState
                              let good = SexpList [SymbolAtom "ok", toSExp s] in
                              runIO $ hPutStrLn h $ convSExp "return" good n
 
+-- | Write a pretty-printed term to the console with semantic coloring
+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
+consoleDisplayAnnotated h output = do ist <- getIState
+                                      runIO . hPutStrLn h .
+                                        displayDecorated (consoleDecorate ist) .
+                                        renderCompact $ output
+
+-- | Write pretty-printed output to IDESlave with semantic annotations
+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
+ideSlaveReturnAnnotated n h out = do ist <- getIState
+                                     let (str, spans) = displaySpans .
+                                                        renderCompact .
+                                                        fmap (fancifyAnnots ist) $
+                                                        out
+                                         good = [SymbolAtom "ok", toSExp str, toSExp spans]
+                                     runIO . hPutStrLn h $ convSExp "return" good n
+
+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
+ihPrintTermWithType h tm ty = do ist <- getIState
+                                 let output = tm <+> colon <+> ty
+                                 case idris_outputmode ist of
+                                   RawOutput -> consoleDisplayAnnotated h output
+                                   IdeSlave n -> ideSlaveReturnAnnotated n h output
+
+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
+ihPrintFunTypes :: Handle -> Name -> [(Name, PTerm)] -> Idris ()
+ihPrintFunTypes h n []        = ihPrintError h $ "No such variable " ++ show n
+ihPrintFunTypes h n overloads = do imp <- impShow
+                                   ist <- getIState
+                                   let output = vsep (map (uncurry (ppOverload imp)) overloads)
+                                   case idris_outputmode ist of
+                                     RawOutput -> consoleDisplayAnnotated h output
+                                     IdeSlave n -> ideSlaveReturnAnnotated n h output
+  where fullName n = annotate (AnnName n Nothing Nothing) $ text (show n)
+        ppOverload imp n tm = fullName n <+> colon <+> prettyImp imp tm
+
+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
+fancifyAnnots ist annot@(AnnName n _ _) =
+  do let ctxt = tt_ctxt ist
+     case () of
+       _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
+       _ | isFnName   n ctxt -> AnnName n (Just FunOutput) Nothing
+       _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
+       _ | otherwise         -> annot
+fancifyAnnots _ annot = annot
+
+type1Doc :: Doc OutputAnnotation
+type1Doc = (annotate AnnConstType $ text "Type 1")
+
 ihPrintError :: Handle -> String -> Idris ()
 ihPrintError h s = do i <- getIState
                       case idris_outputmode i of
@@ -425,11 +474,12 @@ ideslavePutSExp cmd info = do i <- getIState
                                    _ -> return ()
 
 -- this needs some typing magic and more structured output towards emacs
-iputGoal :: String -> Idris ()
-iputGoal s = do i <- getIState
+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
+iputGoal g = do i <- getIState
                 case idris_outputmode i of
-                  RawOutput -> runIO $ putStrLn s
-                  IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
+                  RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
+                  IdeSlave n -> runIO . putStrLn $
+                                convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
 
 isetPrompt :: String -> Idris ()
 isetPrompt p = do i <- getIState
@@ -692,90 +742,6 @@ setTypeCase t = do i <- getIState
                    putIState $ i { idris_options = opt' }
 
 
--- For inferring types of things
-
-bi = fileFC "builtin"
-
-inferTy   = sMN 0 "__Infer"
-inferCon  = sMN 0 "__infer"
-inferDecl = PDatadecl inferTy
-                      PType
-                      [("", inferCon, PPi impl (sMN 0 "iType") PType (
-                                  PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
-                                  (PRef bi inferTy)), bi, [])]
-inferOpts = []
-
-infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
-infP = P (TCon 6 0) inferTy (TType (UVal 0))
-
-getInferTerm, getInferType :: Term -> Term
-getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
-getInferTerm (App (App _ _) tm) = tm
-getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
-
-getInferType (Bind n b sc) = Bind n b $ getInferType sc
-getInferType (App (App _ ty) _) = ty
-
--- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
-
-primNames = [unitTy, unitCon,
-             falseTy, pairTy, pairCon,
-             eqTy, eqCon, inferTy, inferCon]
-
-unitTy   = sMN 0 "__Unit"
-unitCon  = sMN 0 "__II"
-unitDecl = PDatadecl unitTy PType
-                     [("", unitCon, PRef bi unitTy, bi, [])]
-unitOpts = [DefaultEliminator]
-
-falseTy   = sMN 0 "__False"
-falseDecl = PDatadecl falseTy PType []
-falseOpts = []
-
-pairTy    = sMN 0 "__Pair"
-pairCon   = sMN 0 "__MkPair"
-pairDecl  = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
-            [("", pairCon, PPi impl (n "A") PType (
-                       PPi impl (n "B") PType (
-                       PPi expl (n "a") (PRef bi (n "A")) (
-                       PPi expl (n "b") (PRef bi (n "B"))
-                           (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
-                                                pexp (PRef bi (n "B"))])))), bi, [])]
-    where n a = sMN 0 a
-pairOpts = []
-
-eqTy = sUN "="
-eqCon = sUN "refl"
-eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
-                                 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
-                                 PType)
-                [("", eqCon, PPi impl (n "A") PType (
-                         PPi impl (n "x") (PRef bi (n "A"))
-                           (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
-                                                    pimp (n "B") Placeholder False,
-                                                    pexp (PRef bi (n "x")),
-                                                    pexp (PRef bi (n "x"))])), bi, [])]
-    where n a = sMN 0 a
-eqOpts = []
-
-elimName       = sUN "__Elim"
-elimMethElimTy = sUN "__elimTy"
-elimMethElim   = sUN "elim"
-elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] 
-                     [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
-                      PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
-
--- Defined in builtins.idr
-sigmaTy   = sUN "Exists"
-existsCon = sUN "Ex_intro"
-
-piBind :: [(Name, PTerm)] -> PTerm -> PTerm
-piBind = piBindp expl
-
-piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
-piBindp p [] t = t
-piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
-
 -- Dealing with parameters
 
 expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
@@ -1442,7 +1408,7 @@ mkPApp fc a f as = let rest = drop a as in
 -- FIXME: It's possible that this really has to happen after elaboration
 
 findStatics :: IState -> PTerm -> (PTerm, [Bool])
-findStatics ist tm = trace (showImp Nothing True False tm) $
+findStatics ist tm = trace (show tm) $
                       let (ns, ss) = fs tm in
                          runState (pos ns ss tm) []
   where fs (PPi p n t sc)
@@ -1726,3 +1692,4 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
   mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
   mkUniq t = return t
 
+

src/Idris/AbsSyntaxTree.hs

@@ -30,6 +30,8 @@ import Data.Word (Word)
 
 import Debug.Trace
 
+import Text.PrettyPrint.Annotated.Leijen
+
 data IOption = IOption { opt_logLevel   :: Int,
                          opt_typecase   :: Bool,
                          opt_typeintype :: Bool,
@@ -908,62 +910,420 @@ expandNS syn n = case syn_namespace syn of
                         xs -> sNS n xs
 
 
---- Pretty printing declarations and terms
+-- For inferring types of things
+
+bi = fileFC "builtin"
+
+inferTy   = sMN 0 "__Infer"
+inferCon  = sMN 0 "__infer"
+inferDecl = PDatadecl inferTy
+                      PType
+                      [("", inferCon, PPi impl (sMN 0 "iType") PType (
+                                  PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
+                                  (PRef bi inferTy)), bi, [])]
+inferOpts = []
+
+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
+infP = P (TCon 6 0) inferTy (TType (UVal 0))
+
+getInferTerm, getInferType :: Term -> Term
+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
+getInferTerm (App (App _ _) tm) = tm
+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
+
+getInferType (Bind n b sc) = Bind n b $ getInferType sc
+getInferType (App (App _ ty) _) = ty
+
+
+
+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
+
+primNames = [unitTy, unitCon,
+             falseTy, pairTy, pairCon,
+             eqTy, eqCon, inferTy, inferCon]
+
+unitTy   = sMN 0 "__Unit"
+unitCon  = sMN 0 "__II"
+unitDecl = PDatadecl unitTy PType
+                     [("", unitCon, PRef bi unitTy, bi, [])]
+unitOpts = [DefaultEliminator]
+
+falseTy   = sMN 0 "__False"
+falseDecl = PDatadecl falseTy PType []
+falseOpts = []
+
+pairTy    = sMN 0 "__Pair"
+pairCon   = sMN 0 "__MkPair"
+pairDecl  = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
+            [("", pairCon, PPi impl (n "A") PType (
+                       PPi impl (n "B") PType (
+                       PPi expl (n "a") (PRef bi (n "A")) (
+                       PPi expl (n "b") (PRef bi (n "B"))
+                           (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
+                                                pexp (PRef bi (n "B"))])))), bi, [])]
+    where n a = sMN 0 a
+pairOpts = []
+
+eqTy = sUN "="
+eqCon = sUN "refl"
+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
+                                 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
+                                 PType)
+                [("", eqCon, PPi impl (n "A") PType (
+                         PPi impl (n "x") (PRef bi (n "A"))
+                           (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
+                                                    pimp (n "B") Placeholder False,
+                                                    pexp (PRef bi (n "x")),
+                                                    pexp (PRef bi (n "x"))])), bi, [])]
+    where n a = sMN 0 a
+eqOpts = []
+
+elimName       = sUN "__Elim"
+elimMethElimTy = sUN "__elimTy"
+elimMethElim   = sUN "elim"
+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
+                     [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
+                      PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
+
+-- Defined in builtins.idr
+sigmaTy   = sUN "Exists"
+existsCon = sUN "Ex_intro"
+
+piBind :: [(Name, PTerm)] -> PTerm -> PTerm
+piBind = piBindp expl
+
+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
+piBindp p [] t = t
+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
+
+
+-- Pretty-printing declarations and terms
 
 instance Show PTerm where
-    show tm = showImp Nothing False False tm
-
-instance Pretty PTerm where
-  pretty = prettyImp False
+  showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm
 
 instance Show PDecl where
-    show d = showDeclImp False d
+  showsPrec _ d = (displayS . renderCompact . showDeclImp False) d
 
 instance Show PClause where
-    show c = showCImp True c
+  showsPrec _ c = (displayS . renderCompact . showCImp True) c
 
 instance Show PData where
-    show d = showDImp False d
+  showsPrec _ d = (displayS . renderCompact . showDImp False) d
 
-showDecls :: Bool -> [PDecl] -> String
-showDecls _ [] = ""
-showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds
+instance Pretty PTerm OutputAnnotation where
+  pretty = prettyImp False
 
-showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
-showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t
-showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)
+-- | Colourise annotations according to an Idris state. It ignores the names
+-- in the annotation, as there's no good way to show extended information on a
+-- terminal.
+consoleDecorate :: IState -> OutputAnnotation -> String -> String
+consoleDecorate ist _ | not (idris_colourRepl ist) = id
+consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist
+                                   in colouriseData theme
+consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
+                                   in colouriseType theme
+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
+consoleDecorate ist (AnnName n _ _) = let ctxt  = tt_ctxt ist
+                                          theme = idris_colourTheme ist
+                                      in case () of
+                                           _ | isDConName n ctxt -> colouriseData theme
+                                           _ | isFnName n ctxt   -> colouriseFun theme
+                                           _ | isTConName n ctxt -> colouriseType theme
+                                           _ | otherwise         -> id -- don't colourise unknown names
+consoleDecorate ist (AnnFC _) = id
+
+-- | Pretty-print a high-level closed Idris term
+prettyImp :: Bool -- ^^ whether to show implicits
+          -> PTerm -- ^^ the term to pretty-print
+          -> Doc OutputAnnotation
+prettyImp impl = pprintPTerm impl []
+
+-- | Pretty-print a high-level Idris term in some bindings context
+pprintPTerm :: Bool -- ^^ whether to show implicits
+            -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
+            -> PTerm -- ^^ the term to pretty-print
+            -> Doc OutputAnnotation
+pprintPTerm impl bnd = prettySe 10 bnd
+  where
+    prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
+    prettySe p bnd (PQuote r) =
+      if size r > breakingSize then
+        text "![" <> line <> pretty r <> text "]"
+      else
+        text "![" <> pretty r <> text "]"
+    prettySe p bnd (PPatvar fc n) = pretty n
+    prettySe p bnd e
+      | Just str <- slist p bnd e = str
+      | Just n <- snat p e = annotate AnnConstData (text (show n))
+    prettySe p bnd (PRef fc n) = prettyName impl bnd n
+    prettySe p bnd (PLam n ty sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc
+        else
+          text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc
+    prettySe p bnd (PLet n ty v sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>
+            nest nestingSize (prettySe 10 ((n, False):bnd) sc)
+        else
+          text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>
+            prettySe 10 ((n, False):bnd) sc
+    prettySe p bnd (PPi (Exp l s _ _) n ty sc)
+      | n `elem` allNamesIn sc || impl =
+          let open = if Lazy `elem` l then text "|" <> lparen else lparen in
+            bracket p 2 $
+              if size sc > breakingSize then
+                enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
+                  st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
+              else
+                enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
+                 st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
+      | otherwise                      =
+          bracket p 2 $
+            if size sc > breakingSize then
+              prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
+            else
+              prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
+      where
+        st =
+          case s of
+            Static -> text "[static]" <> space
+            _      -> empty
+    prettySe p bnd (PPi (Imp l s _ _) n ty sc)
+      | impl =
+          let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
+            bracket p 2 $
+              if size sc > breakingSize then
+                open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
+                  st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
+              else
+                open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
+                  st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
+      | otherwise = prettySe 10 ((n, True):bnd) sc
+      where
+        st =
+          case s of
+            Static -> text "[static]" <> space
+            _      -> empty
+    prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc
+        else
+          prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc
+    prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =
+      bracket p 2 $
+        if size sc > breakingSize then
+          lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>
+            rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc
+        else
+          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
+            rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc
+    prettySe p bnd (PApp _ (PRef _ f) [])
+      | not impl = prettyName impl bnd f
+    prettySe p bnd (PAppBind _ (PRef _ f) [])
+      | not impl = text "!" <> prettyName impl bnd f
+    prettySe p bnd (PApp _ (PRef _ op) args)
+      | UN nm <- basename op
+      , not (tnull nm) &&
+        length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
+          let [l, r] = getExps args in
+            bracket p 1 $
+              if size r > breakingSize then
+                prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r
+              else
+                prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r
+    prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
+      | PConstant (Idris.Core.TT.Str str) <- getTm tm,
+        f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
+    prettySe p bnd (PApp _ f as) =
+      let args = getExps as
+          fp   = prettySe 1 bnd f
+      in
+        bracket p 1 $
+          hsep (if impl
+                  then fp : map (prettyArgS bnd) as
+                  else fp : map (prettyArgSe bnd) args)
+    prettySe p bnd (PCase _ scr opts) =
+      text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
+      where
+        prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
+
+        sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
+    prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
+    prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
+    prettySe p bnd (PResolveTC _) = text "resolvetc"
+    prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
+    prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
+    prettySe p bnd (PEq _ l r) =
+      bracket p 2 $
+        if size r > breakingSize then
+          prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)
+        else
+          prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r
+      where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
+    prettySe p bnd (PRewrite _ l r _) =
+      bracket p 2 $
+        if size r > breakingSize then
+          text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)
+        else
+          text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
+    prettySe p bnd (PTyped l r) =
+      lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
+    prettySe p bnd (PPair _ l r) =
+      if size r > breakingSize then
+        lparen <> prettySe 10 bnd l <> text "," <>
+          line <> prettySe 10 bnd r <> rparen
+      else
+        lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
+    prettySe p bnd (PDPair _ l t r) =
+      if size r > breakingSize then
+        lparen <> prettySe 10 bnd l <+> text "**" <>
+          line <> prettySe 10 bnd r <> rparen
+      else
+        lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
+    prettySe p bnd (PAlternative a as) =
+      lparen <> text "|" <> prettyAs <> text "|" <> rparen
+        where
+          prettyAs =
+            foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
+    prettySe p bnd PType = annotate AnnConstType $ text "Type"
+    prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))
+      where annot (AType _) = AnnConstType
+            annot StrType   = AnnConstType
+            annot PtrType   = AnnConstType
+            annot VoidType  = AnnConstType
+            annot _         = AnnConstData
+    -- XXX: add pretty for tactics
+    prettySe p bnd (PProof ts) =
+      text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
+    prettySe p bnd (PTactics ts) =
+      text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
+    prettySe p bnd (PMetavar n) = text "?" <> pretty n
+    prettySe p bnd (PReturn f) = text "return"
+    prettySe p bnd PImpossible = text "impossible"
+    prettySe p bnd Placeholder = text "_"
+    prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
+    prettySe p bnd (PElabError s) = pretty s
+
+    prettySe p bnd _ = text "test"
+
+    prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)
+    prettyArgS bnd (PExp _ _ tm _)   = prettyArgSe bnd tm
+    prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm
+    prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)
+
+    prettyArgSe bnd arg = prettySe 0 bnd arg
+    prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
+    prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
+    prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
+
+    basename :: Name -> Name
+    basename (NS n _) = basename n
+    basename n = n
+
+    slist' p bnd (PApp _ (PRef _ nil) _)
+      | not impl && nsroot nil == sUN "Nil" = Just []
+    slist' p bnd (PApp _ (PRef _ cons) args)
+      | nsroot cons == sUN "::",
+        (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
+        all isImp imps,
+        Just tl' <- slist' p bnd tl
+      = Just (hd:tl')
+      where
+        isImp (PImp {}) = True
+        isImp _ = False
+    slist' _ _ _ = Nothing
+
+    slist p bnd e | Just es <- slist' p bnd e = Just $
+      case es of [] -> annotate AnnConstData $ text "[]"
+                 [x] -> enclose left
+                                right
+                                (prettySe p bnd x)
+                 xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs
+      where left  = (annotate AnnConstData (text "["))
+            right = (annotate AnnConstData (text "]"))
+            comma = (annotate AnnConstData (text ","))
+    slist _ _ _ = Nothing
+
+    natns = "Prelude.Nat."
+
+    snat p (PRef _ z)
+      | show z == (natns++"Z") || show z == "Z" = Just 0
+    snat p (PApp _ s [PExp {getTm=n}])
+      | show s == (natns++"S") || show s == "S",
+        Just n' <- snat p n
+      = Just $ 1 + n'
+    snat _ _ = Nothing
+
+    bracket outer inner doc
+      | inner > outer = lparen <> doc <> rparen
+      | otherwise     = doc
+
+-- | Pretty-printer helper for the binding site of a name
+bindingOf :: Name -- ^^ the bound name
+          -> Bool -- ^^ whether the name is implicit
+          -> Doc OutputAnnotation
+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
+
+-- | Pretty-printer helper for names that attaches the correct annotations
+prettyName :: Bool -- ^^ whether to show namespaces
+           -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
+           -> Name -- ^^ the name to pprint
+           -> Doc OutputAnnotation
+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
+                        | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))
+  where strName (UN n) = T.unpack n
+        strName (NS n ns) | showNS    = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
+                          | otherwise = strName n
+        strName (MN i s) = T.unpack s
+        strName other = show other
+
+
+showCImp :: Bool -> PClause -> Doc OutputAnnotation
+showCImp impl (PClause _ n l ws r w)
+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r
+             <+> text "where" <+> text (show w)
+  where
+    showWs [] = empty
+    showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
+showCImp impl (PWith _ n l ws r w)
+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r
+                 <+> braces (text (show w))
+  where
+    showWs [] = empty
+    showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
+
+
+showDImp :: Bool -> PData -> Doc OutputAnnotation
+showDImp impl (PDatadecl n ty cons)
+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>
+    (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))
+
+showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
+showDecls i ds = vsep (map (showDeclImp i) ds)
+
+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
+showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t
+showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
+                                      indent 2 (vsep (map (showCImp i) cs))
 showDeclImp _ (PData _ _ _ _ d) = showDImp True d
-showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"
-showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"
-showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn
+showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)
+showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)
+showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
 showDeclImp i (PClass _ _ _ cs n ps ds)
-    = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds
+   = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds
 showDeclImp i (PInstance _ _ cs n _ t _ ds)
-    = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds
-showDeclImp _ _ = "..."
+   = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds
+showDeclImp _ _ = text "..."
 -- showDeclImp (PImport i) = "import " ++ i
 
-
-showCImp :: Bool -> PClause -> String
-showCImp impl (PClause _ n l ws r w)
-   = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r
-             ++ " where " ++ show w
-  where
-    showWs [] = ""
-    showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
-showCImp impl (PWith _ n l ws r w)
-   = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r
-             ++ " { " ++ show w ++ " } "
-  where
-    showWs [] = ""
-    showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
-
-
-showDImp :: Bool -> PData -> String
-showDImp impl (PDatadecl n ty cons)
-   = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"
-     ++ showSep "\n\t| "
-            (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)
+instance Show (Doc OutputAnnotation) where
+  show = flip (displayS . renderCompact) ""
 
 getImps :: [PArg] -> [(Name, PTerm)]
 getImps [] = []
@@ -983,199 +1343,6 @@ getConsts (_ : xs) = getConsts xs
 getAll :: [PArg] -> [PTerm]
 getAll = map getTm
 
--- | Pretty-print a high-level Idris term
-prettyImp :: Bool -- ^^ whether to show implicits
-          -> PTerm -- ^^ the term to pretty-print
-          -> Doc
-prettyImp impl = prettySe 10
-  where
-    prettySe p (PQuote r) =
-      if size r > breakingSize then
-        text "![" $$ pretty r <> text "]"
-      else
-        text "![" <> pretty r <> text "]"
-    prettySe p (PPatvar fc n) = pretty n
-    prettySe p (PRef fc n) =
-      if impl then
-        pretty n
-      else
-        prettyBasic n
-      where
-        prettyBasic n@(UN _) = pretty n
-        prettyBasic (MN _ s) = text (str s)
-        prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n
-        prettyBasic (SN sn) = text (show sn)
-    prettySe p (PLam n ty sc) =
-      bracket p 2 $
-        if size sc > breakingSize then
-          text "λ" <> pretty n <+> text "=>" $+$ pretty sc
-        else
-          text "λ" <> pretty n <+> text "=>" <+> pretty sc
-    prettySe p (PLet n ty v sc) =
-      bracket p 2 $
-        if size sc > breakingSize then
-          text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
-            nest nestingSize (prettySe 10 sc)
-        else
-          text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
-            prettySe 10 sc
-    prettySe p (PPi (Exp l s _ _) n ty sc)
-      | n `elem` allNamesIn sc || impl =
-          let open = if Lazy `elem` l then text "|" <> lparen else lparen in
-            bracket p 2 $
-              if size sc > breakingSize then
-                open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
-                  st <+> text "->" $+$ prettySe 10 sc
-              else
-                open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
-                  st <+> text "->" <+> prettySe 10 sc
-      | otherwise                      =
-          bracket p 2 $
-            if size sc > breakingSize then
-              prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
-            else
-              prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
-      where
-        st =
-          case s of
-            Static -> text "[static]"
-            _      -> empty
-    prettySe p (PPi (Imp l s _ _) n ty sc)
-      | impl =
-          let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
-            bracket p 2 $
-              if size sc > breakingSize then
-                open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
-                  st <+> text "->" <+> prettySe 10 sc
-              else
-                open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
-                  st <+> text "->" <+> prettySe 10 sc
-      | otherwise = prettySe 10 sc
-      where
-        st =
-          case s of
-            Static -> text $ "[static]"
-            _      -> empty
-    prettySe p (PPi (Constraint _ _ _) n ty sc) =
-      bracket p 2 $
-        if size sc > breakingSize then
-          prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
-        else
-          prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
-    prettySe p (PPi (TacImp _ _ s _) n ty sc) =
-      bracket p 2 $
-        if size sc > breakingSize then
-          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
-            rbrace <+> text "->" $+$ prettySe 10 sc
-        else
-          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
-            rbrace <+> text "->" <+> prettySe 10 sc
-    prettySe p (PApp _ (PRef _ f) [])
-      | not impl = pretty f
-    prettySe p (PAppBind _ (PRef _ f) [])
-      | not impl = text "!" <+> pretty f
-    prettySe p (PApp _ (PRef _ op@(UN nm)) args)
-      | not (tnull nm) &&
-        length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
-          let [l, r] = getExps args in
-            bracket p 1 $
-              if size r > breakingSize then
-                prettySe 1 l <+> pretty op $+$ prettySe 0 r
-              else
-                prettySe 1 l <+> pretty op <+> prettySe 0 r
-    prettySe p (PApp _ f as) =
-      let args = getExps as in
-        bracket p 1 $
-          prettySe 1 f <+>
-            if impl then
-              foldl' fS empty as
-              -- foldr (<+>) empty $ map prettyArgS as
-            else
-              foldl' fSe empty args
-              -- foldr (<+>) empty $ map prettyArgSe args
-      where
-        fS l r =
-          if size r > breakingSize then
-            l $+$ nest nestingSize (prettyArgS r)
-          else
-            l <+> prettyArgS r
-
-        fSe l r =
-          if size r > breakingSize then
-            l $+$ nest nestingSize (prettyArgSe r)
-          else
-            l <+> prettyArgSe r
-    prettySe p (PCase _ scr opts) =
-      text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
-      where
-        prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
-
-        sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
-    prettySe p (PHidden tm) = text "." <> prettySe 0 tm
-    prettySe p (PRefl _ _) = text "refl"
-    prettySe p (PResolveTC _) = text "resolvetc"
-    prettySe p (PTrue _) = text "()"
-    prettySe p (PFalse _) = text "_|_"
-    prettySe p (PEq _ l r) =
-      bracket p 2 $
-        if size r > breakingSize then
-          prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
-        else
-          prettySe 10 l <+> text "=" <+> prettySe 10 r
-    prettySe p (PRewrite _ l r _) =
-      bracket p 2 $
-        if size r > breakingSize then
-          text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)
-        else
-          text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r
-    prettySe p (PTyped l r) =
-      lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
-    prettySe p (PPair _ l r) =
-      if size r > breakingSize then
-        lparen <> prettySe 10 l <> text "," $+$
-          prettySe 10 r <> rparen
-      else
-        lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
-    prettySe p (PDPair _ l t r) =
-      if size r > breakingSize then
-        lparen <> prettySe 10 l <+> text "**" $+$
-          prettySe 10 r <> rparen
-      else
-        lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
-    prettySe p (PAlternative a as) =
-      lparen <> text "|" <> prettyAs <> text "|" <> rparen
-        where
-          prettyAs =
-            foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
-    prettySe p PType = text "Type"
-    prettySe p (PConstant c) = pretty c
-    -- XXX: add pretty for tactics
-    prettySe p (PProof ts) =
-      text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
-    prettySe p (PTactics ts) =
-      text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
-    prettySe p (PMetavar n) = text "?" <> pretty n
-    prettySe p (PReturn f) = text "return"
-    prettySe p PImpossible = text "impossible"
-    prettySe p Placeholder = text "_"
-    prettySe p (PDoBlock _) = text "do block pretty not implemented"
-    prettySe p (PElabError s) = pretty s
-
-    prettySe p _ = text "test"
-
-    prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)
-    prettyArgS (PExp _ _ tm _)   = prettyArgSe tm
-    prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
-    prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
-
-    prettyArgSe arg = prettySe 0 arg
-    prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
-    prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
-    prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
-
-    bracket outer inner doc
-      | inner > outer = lparen <> doc <> rparen
-      | otherwise     = doc
 
 -- | Show Idris name
 showName :: Maybe IState   -- ^^ the Idris state, for information about names and colours
@@ -1206,171 +1373,14 @@ showName ist bnd impl colour n = case ist of
                                       -- (like error messages). Thus, unknown vars are colourised as implicits.
                                       | otherwise         -> colouriseImplicit t name
 
--- | Show Idris term
-showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours
-        -> Bool  -- ^^ whether to show implicits
-        -> Bool  -- ^^ whether to colourise
-        -> PTerm -- ^^ the term to show
-        -> String
-showImp ist impl colour tm = se 10 [] tm where
-    perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
-    perhapsColourise col str = case ist of
-                                 Just i -> if colour then col (idris_colourTheme i) str else str
-                                 Nothing -> str
+showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
+       -> PTerm  -- ^^ the term to show
+       -> String
+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))
 
-    se :: Int -> [(Name, Bool)] -> PTerm -> String
-    se p bnd (PQuote r) = "![" ++ show r ++ "]"
-    se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
-    se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
-    se p bnd e
-        | Just str <- slist p bnd e = str
-        | Just num <- snat p e  = perhapsColourise colouriseData (show num)
-    se p bnd (PRef fc n) = showName ist bnd impl colour n
-    se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
-                              (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
-                              ++ se 10 ((n, False):bnd) sc
-    se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
-                                " = " ++ se 10 bnd v ++
-                                " in " ++ se 10 ((n, False):bnd) sc
-    se p bnd (PPi (Exp l s _ param) n ty sc)
-        | n `elem` allNamesIn sc || impl
-                                  = bracket p 2 $
-                                    (if Lazy `elem` l then "|(" else "(") ++
-                                    perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
-                                    ") " ++
-                                    (if (impl && param) then "P" else "") ++
-                                    st ++
-                                    "-> " ++ se 10 ((n, False):bnd) sc
-        | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
-      where st = case s of
-                    Static -> "[static] "
-                    _ -> ""
-    se p bnd (PPi (Imp l s _ _) n ty sc)
-        | impl = bracket p 2 $ (if Lazy `elem` l then "|{" else "{") ++
-                               perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
-                               "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
-        | otherwise = se 10 ((n, True):bnd) sc
-      where st = case s of
-                    Static -> "[static] "
-                    _ -> ""
-    se p bnd (PPi (Constraint _ _ _) n ty sc)
-        = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
-    se p bnd (PPi (TacImp _ _ s _) n ty sc)
-        = bracket p 2 $
-          "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
-          se 10 ((n, False):bnd) sc
-    se p bnd (PMatchApp _ f) = "match " ++ show f
-    se p bnd (PApp _ hd@(PRef fc f) [tm])
-        | PConstant (Idris.Core.TT.Str str) <- getTm tm,
-          f == sUN "Symbol_" = "'" ++ se 10 bnd (PRef fc (sUN str))
-    se p bnd (PApp _ hd@(PRef _ f) [])
-        | not impl = se p bnd hd
-    se p bnd (PAppBind _ hd@(PRef _ f) [])
-        | not impl = "!" ++ se p bnd hd
-    se p bnd (PApp _ op@(PRef _ (UN nm)) args)
-        | not (tnull nm) &&
-          length (getExps args) == 2 && not impl && not (isAlpha (thead nm))
-            = let [l, r] = getExps args in
-              bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r
-    se p bnd (PApp _ f as)
-        = -- let args = getExps as in
-              bracket p 1 $ se 1 bnd f ++
-                  if impl then concatMap (sArg bnd) as
-                          else concatMap (suiArg impl bnd) as
-    se p bnd (PAppBind _ f as)
-        = let args = getExps as in
-              "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
-                                                         else concatMap (seArg bnd) args)
-    se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
-       where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
-    se p bnd (PHidden tm) = "." ++ se 0 bnd tm
-    se p bnd (PRefl _ t)
-        | not impl = perhapsColourise colouriseData "refl"
-        | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
-    se p bnd (PResolveTC _) = "resolvetc"
-    se p bnd (PTrue _) = perhapsColourise colouriseType "()"
-    se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"
-    se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r
-    se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
-    se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
-    se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
-    se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
-    se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
-    se p bnd PType = perhapsColourise colouriseType "Type"
-    se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)
-        where cfun (AType _) = colouriseType
-              cfun StrType   = colouriseType
-              cfun PtrType   = colouriseType
-              cfun VoidType  = colouriseType
-              cfun _         = colouriseData
-    se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
-    se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
-    se p bnd (PMetavar n) = "?" ++ show n
-    se p bnd (PReturn f) = "return"
-    se p bnd PImpossible = "impossible"
-    se p bnd Placeholder = "_"
-    se p bnd (PDoBlock _) = "do block show not implemented"
-    se p bnd (PElabError s) = show s
-    se p bnd (PCoerced t) = se p bnd t
-    se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
-    se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t
-    se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t
---     se p bnd x = "Not implemented"
-
-    slist' p bnd (PApp _ (PRef _ nil) _)
-      | not impl && nsroot nil == sUN "Nil" = Just []
-    slist' p bnd (PApp _ (PRef _ cons) args)
-      | nsroot cons == sUN "::",
-        (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
-        all isImp imps,
-        Just tl' <- slist' p bnd tl
-      = Just (hd:tl')
-      where
-        isImp (PImp {}) = True
-        isImp _         = False
-    slist' _ _ _ = Nothing
-
-    slist p bnd e | Just es <- slist' p bnd e = Just $
-      case es of []  -> "[]"
-                 [x] -> "[" ++ se p bnd x ++ "]"
-                 xs  -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
-    slist _ _ _ = Nothing
-
-    -- since Prelude is always imported, S & Z are unqualified iff they're the
-    -- Nat ones.
-    snat p (PRef _ o)
-      | show o == (natns++"Z") || show o == "Z" = Just 0
-    snat p (PApp _ s [PExp {getTm=n}])
-      | show s == (natns++"S") || show s == "S",
-        Just n' <- snat p n
-      = Just $ 1 + n'
-    snat _ _ = Nothing
-
-    natns = "Prelude.Nat."
-
-    sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)
-    sArg bnd (PExp _ _ tm _) = seArg bnd tm
-    sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
-    sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
-
-    -- show argument, implicits given by the user also shown
-    suiArg impl bnd (PImp _ mi _ n tm _)
-        | impl || not mi = siArg bnd (n, tm)
-    suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm
-    suiArg impl bnd _ = ""
-
-    seArg bnd arg      = " " ++ se 0 bnd arg
-    siArg bnd (n, val) =
-        let n' = show n
-            val' = se 10 bnd val in
-            if (n' == val')
-               then " {" ++ n' ++ "}"
-               else " {" ++ n' ++ " = " ++ val' ++ "}"
-    scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
-    stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
-
-    bracket outer inner str | inner > outer = "(" ++ str ++ ")"
-                            | otherwise = str
+-- | Show a term with implicits, no colours
+showTmImpls :: PTerm -> String
+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""
 
 
 instance Sized PTerm where

src/Idris/CaseSplit.hs

@@ -62,11 +62,11 @@ split n t'
              Just ty ->
                 do let splits = findPats ist ty
                    iLOG ("New patterns " ++ showSep ", "  
-                         (map (showImp Nothing True False) splits))
+                         (map showTmImpls splits))
                    let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
                    logLvl 4 ("Working from " ++ show t)
                    logLvl 4 ("Trying " ++ showSep "\n" 
-                               (map (showImp Nothing True False) newPats_in))
+                               (map (showTmImpls) newPats_in))
                    newPats <- mapM elabNewPat newPats_in
                    logLvl 3 ("Original:\n" ++ show t)
                    logLvl 3 ("Split:\n" ++
@@ -237,7 +237,7 @@ splitOnLine l n fn = do
 --     let (before, later) = splitAt (l-1) (lines inp)
 --     i <- getIState
     cl <- getInternalApp fn l
-    logLvl 3 ("Working with " ++ showImp Nothing True False cl)
+    logLvl 3 ("Working with " ++ showTmImpls cl)
     tms <- split n cl
 --     iputStrLn (showSep "\n" (map show tms))
     return tms -- "" -- not yet done...

src/Idris/Core/Elaborate.hs

@@ -24,7 +24,7 @@ import Data.Char
 import Data.List
 import Debug.Trace
 
-import Util.Pretty
+import Util.Pretty hiding (fill)
 
 -- I don't really want this here, but it's useful for the test shell
 data Command = Theorem Name Raw

src/Idris/Core/ProofState.hs

@@ -18,7 +18,7 @@ import Control.Applicative hiding (empty)
 import Data.List
 import Debug.Trace
 
-import Util.Pretty
+import Util.Pretty hiding (fill)
 
 data ProofState = PS { thname   :: Name,
                        holes    :: [Name], -- holes still to be solved
@@ -113,23 +113,23 @@ instance Show ProofState where
                                          " =?= " ++ showEnv ps v
                showG ps b = showEnv ps (binderTy b)
 
-instance Pretty ProofState where
+instance Pretty ProofState OutputAnnotation where
   pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
     if size nm > breakingSize then
-      pretty nm <> colon $$ nest nestingSize (text " no more goals.")
+      pretty nm <+> colon <+> nest nestingSize (text " no more goals.")
     else
-      pretty nm <> colon <+> text " no more goals."
+      pretty nm <+> colon <+> text " no more goals."
   pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =
     let OK g  = goal (Just h) tm in
     let wkEnv = premises g in
-      text "Other goals" <+> colon <+> pretty hs $$
-      prettyPs wkEnv (reverse wkEnv) $$
-      text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
+      text "Other goals" <+> colon <+> pretty hs <+>
+      prettyPs wkEnv (reverse wkEnv) <+>
+      text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
       pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
     where
       prettyGoal ps (Guess t v) =
         if size v > breakingSize then
-          prettyEnv ps t <+> text "=?=" $$
+          prettyEnv ps t <+> text "=?=" <+>
             nest nestingSize (prettyEnv ps v)
         else
           prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
@@ -139,17 +139,17 @@ instance Pretty ProofState where
       prettyPs env ((n, Let t v):bs) =
         nest nestingSize (pretty n <+> colon <+>
           if size v > breakingSize then
-            prettyEnv env t <+> text "=" $$
-              nest nestingSize (prettyEnv env v) $$
+            prettyEnv env t <+> text "=" <+>
+              nest nestingSize (prettyEnv env v) <+>
                 nest nestingSize (prettyPs env bs)
           else
-            prettyEnv env t <+> text "=" <+> prettyEnv env v $$
+            prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
               nest nestingSize (prettyPs env bs))
       prettyPs env ((n, b):bs) =
         if size (binderTy b) > breakingSize then
           nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
         else
-          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
             nest nestingSize (prettyPs env bs))
 
 same Nothing n  = True

src/Idris/Core/TT.hs

@@ -77,6 +77,16 @@ instance Sized FC where
 instance Show FC where
     show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
 
+-- | Output annotation for pretty-printed name - decides colour
+data NameOutput = TypeOutput | FunOutput | DataOutput
+
+-- | Output annotations for pretty-printing
+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)
+                      | AnnBoundName Name Bool
+                      | AnnConstData
+                      | AnnConstType
+                      | AnnFC FC
+
 -- | Used for error reflection
 data ErrorReportPart = TextPart String
                      | NamePart Name
@@ -177,15 +187,15 @@ instance Show Err where
     show (At f e) = show f ++ ":" ++ show e
     show _ = "Error"
 
-instance Pretty Err where
+instance Pretty Err OutputAnnotation where
   pretty (Msg m) = text m
   pretty (CantUnify _ l r e _ i) =
     if size l + size r > breakingSize then
-      text "Cannot unify" <+> colon $$
-        nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
+      text "Cannot unify" <+> colon <+>
+        nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>
         nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
     else
-      text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
+      text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
         nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
   pretty (ProviderError msg) = text msg
   pretty err@(LoadingFailed _ _) = text (show err)
@@ -196,11 +206,11 @@ instance Error Err where
 
 type TC = TC' Err
 
-instance (Pretty a) => Pretty (TC a) where
+instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
   pretty (OK ok) = pretty ok
   pretty (Error err) =
     if size err > breakingSize then
-      text "Error" <+> colon $$ (nest nestingSize $ pretty err)
+      text "Error" <+> colon <+> (nest nestingSize $ pretty err)
     else
       text "Error" <+> colon <+> pretty err
 
@@ -294,11 +304,15 @@ instance Sized Name where
   size (MN i n) = 1
   size _ = 1
 
-instance Pretty Name where
-  pretty (UN n) = text (T.unpack n)
-  pretty (NS n s) = pretty n
-  pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
-  pretty (SN s) = text (show s)
+instance Pretty Name OutputAnnotation where
+  pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')
+  pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un
+  pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $
+                      lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
+  pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)
+
+instance Pretty [Name] OutputAnnotation where
+  pretty = encloseSep empty empty comma . map pretty
 
 instance Show Name where
     show (UN n) = str n
@@ -417,7 +431,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
 data NativeTy = IT8 | IT16 | IT32 | IT64
     deriving (Show, Eq, Ord, Enum)
 
-instance Pretty NativeTy where
+instance Pretty NativeTy OutputAnnotation where
     pretty IT8  = text "Bits8"
     pretty IT16 = text "Bits16"
     pretty IT32 = text "Bits32"
@@ -435,7 +449,7 @@ deriving instance NFData NativeTy
 deriving instance NFData ArithTy
 !-}
 
-instance Pretty ArithTy where
+instance Pretty ArithTy OutputAnnotation where
     pretty (ATInt ITNative) = text "Int"
     pretty (ATInt ITBig) = text "BigInt"
     pretty (ATInt ITChar) = text "Char"
@@ -471,7 +485,7 @@ deriving instance NFData Const
 instance Sized Const where
   size _ = 1
 
-instance Pretty Const where
+instance Pretty Const OutputAnnotation where
   pretty (I i) = text . show $ i
   pretty (BI i) = text . show $ i
   pretty (Fl f) = text . show $ f
@@ -503,7 +517,7 @@ instance Sized Raw where
   size (RForce raw) = 1 + size raw
   size (RConstant const) = size const
 
-instance Pretty Raw where
+instance Pretty Raw OutputAnnotation where
   pretty = text . show
 
 {-!
@@ -621,7 +635,7 @@ deriving instance NFData NameType
 instance Sized NameType where
   size _ = 1
 
-instance Pretty NameType where
+instance Pretty NameType OutputAnnotation where
   pretty = text . show
 
 instance Eq NameType where
@@ -687,7 +701,7 @@ instance Sized a => Sized (TT a) where
   size Erased = 1
   size (TType u) = 1 + size u
 
-instance Pretty a => Pretty (TT a) where
+instance Pretty a o => Pretty (TT a) o where
   pretty _ = text "test"
 
 type EnvTT n = [(n, Binder (TT n))]
@@ -1042,7 +1056,7 @@ prettyEnv env t = prettyEnv' env t False
     prettySe p env (P nt n t) debug =
       pretty n <+>
         if debug then
-          lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
+          lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket
         else
           empty
     prettySe p env (V i) debug
@@ -1050,7 +1064,7 @@ prettyEnv env t = prettyEnv' env t False
         if debug then
           text . show . fst $ env!!i
         else
-          lbrack <+> text (show i) <+> rbrack
+          lbracket <+> text (show i) <+> rbracket
       | otherwise      = text "unbound" <+> text (show i) <+> text "!"
     prettySe p env (Bind n b@(Pi t) sc) debug
       | noOccurrence n sc && not debug =

src/Idris/Coverage.hs

@@ -50,7 +50,7 @@ genClauses fc n xs given
         logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
         logLvl 10 $ show argss ++ "\n" ++ show all_args
         logLvl 10 $ "Original: \n" ++
-             showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)
+             showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
         -- add an infinite supply of explicit arguments to update the possible
         -- cases for (the return type may be variadic, or function type, sp
         -- there may be more case splitting that the idris_implicits record
@@ -60,10 +60,10 @@ genClauses fc n xs given
                         _ -> repeat (pexp Placeholder)
         let tryclauses = mkClauses parg all_args
         logLvl 2 $ show (length tryclauses) ++ " initially to check"
-        logLvl 5 $ showSep "\n" (map (showImp Nothing True False) tryclauses)
+        logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)
         let new = filter (noMatch i) (nub tryclauses)
         logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
-        logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)
+        logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
 --           ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
         return new
 --         return (map (\t -> PClause n t [] PImpossible []) new)

src/Idris/Delaborate.hs

@@ -1,10 +1,12 @@
 {-# LANGUAGE PatternGuards #-}
 
-module Idris.Delaborate where
+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where
 
 -- Convert core TT back into high level syntax, primarily for display
 -- purposes.
 
+import Util.Pretty
+
 import Idris.AbsSyntax
 import Idris.Core.TT
 import Idris.Core.Evaluate
@@ -33,7 +35,7 @@ delab' :: IState -> Term -> Bool -> Bool -> PTerm
 delab' i t f mvs = delabTy' i [] t f mvs
 
 delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any
-          -> Term 
+          -> Term
           -> Bool -- ^ use full names
           -> Bool -- ^ Don't treat metavariables specially
           -> PTerm
@@ -50,8 +52,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
                        | Just n' <- lookup n env = PRef un n'
                        | otherwise
                             = case lookup n (idris_metavars ist) of
-                                  Just (Just _, mi, _) -> mkMVApp (dens n) []
-                                  _ -> PRef un (dens n)
+                                  Just (Just _, mi, _) -> mkMVApp n []
+                                  _ -> PRef un n
     de env _ (Bind n (Lam ty) sc)
           = PLam n (de env [] ty) (de ((n,n):env) [] sc)
     de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)
@@ -96,9 +98,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
     deFn env (P _ n _) args | not mvs
          = case lookup n (idris_metavars ist) of
                 Just (Just _, mi, _) ->
-                     mkMVApp (dens n) (drop mi (map (de env []) args))
-                _ -> mkPApp (dens n) (map (de env []) args)
-         | otherwise = mkPApp (dens n) (map (de env []) args)
+                     mkMVApp n (drop mi (map (de env []) args))
+                _ -> mkPApp n (map (de env []) args)
+         | otherwise = mkPApp n (map (de env []) args)
     deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))
 
     mkMVApp n []
@@ -115,105 +117,109 @@ delabTy' ist imps tm fullname mvs = de [] imps tm
     imp (PConstraint p l _ d) arg = PConstraint p l arg d
     imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d
 
+-- | How far to indent sub-errors
+errorIndent :: Int
+errorIndent = 8
 
-indented text = boxIt '\n' $ unlines $ map ('\t':) $ lines text where
-    boxIt c text = (c:text) ++ if last text == c
-                                  then ""
-                                  else [c]
+-- | Actually indent a sub-error - no line at end because a newline can end
+-- multiple layers of indent
+indented :: Doc a -> Doc a
+indented = nest errorIndent . (line <>)
+
+pprintTerm :: IState -> PTerm -> Doc OutputAnnotation
+pprintTerm ist = prettyImp (opt_showimp (idris_options ist))
 
 pshow :: IState -> Err -> String
-pshow i err = pshow' i (fmap (errReverse i) err)
+pshow ist err = displayDecorated (consoleDecorate ist) .
+                renderPretty 1.0 80 .
+                fmap (fancifyAnnots ist) $ pprintErr ist err
 
-pshow' i (Msg s) = s
-pshow' i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
-   "\nThis is probably a bug, or a missing error message.\n" ++
-   "Please consider reporting at " ++ bugaddr
-pshow' i (CantUnify _ x y e sc s)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-        "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
-          ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++
---         " (" ++ show x ++ " and " ++ show y ++ ") " ++
-        case e of
-            Msg "" -> ""
-            _ -> "\nSpecifically:" ++
-                indented (pshow' i e) ++
-                if (opt_errContext (idris_options i)) then showSc i sc else ""
-pshow' i (CantConvert x y env)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-          "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
-                 ++ indented (showImp (Just i) imps colour (delab i y)) ++
-                 if (opt_errContext (idris_options i)) then showSc i env else ""
-pshow' i (CantSolveGoal x env)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-          "Can't solve goal " ++ indented (showImp (Just i) imps colour (delab i x)) ++
-                 if (opt_errContext (idris_options i)) then showSc i env else ""
-pshow' i (UnifyScope n out tm env)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-          "Can't unify" ++ indented (show n) ++ "with"
-                 ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
-                 indented (show out) ++ "is not in scope" ++
-                 if (opt_errContext (idris_options i)) then showSc i env else ""
-pshow' i (CantInferType t)
-    = "Can't infer type for " ++ t
-pshow' i (NonFunctionType f ty)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-          showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
-            ++ showImp (Just i) imps colour (delab i ty) ++ ")"
-pshow' i (NotEquality tm ty)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-          showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("
-            ++ showImp (Just i) imps colour (delab i ty) ++ ")"
-pshow' i (TooManyArguments f)
-    = "Too many arguments for " ++ show f
-pshow' i (CantIntroduce ty)
-    = let imps = opt_showimp (idris_options i) in
-      let colour = idris_colourRepl i in
-          "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
-pshow' i (InfiniteUnify x tm env)
-    = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
-      " would lead to infinite value" ++
-                 if (opt_errContext (idris_options i)) then showSc i env else ""
-pshow' i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
-                                " when unifying " ++ show (delab i x) ++ " and " ++
-                                                     show (delab i y)
-pshow' i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
-pshow' i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
-pshow' i (NoTypeDecl n) = "No type declaration for " ++ show n
-pshow' i (NoSuchVariable n) = "No such variable " ++ show n
-pshow' i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
-pshow' i UniverseError = "Universe inconsistency"
-pshow' i ProgramLineComment = "Program line next to comment"
-pshow' i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
-pshow' i (NonCollapsiblePostulate n)
-    = "The return type of postulate " ++ show n ++ " is not collapsible"
-pshow' i (AlreadyDefined n) = show n ++ " is already defined"
-pshow' i (ProofSearchFail e) = pshow' i e
-pshow' i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)
-pshow' i (At f e) = show f ++ ":" ++ pshow' i e
-pshow' i (Elaborating s n e) = "When elaborating " ++ s ++
-                               showqual i n ++ ":\n" ++ pshow' i e
-pshow' i (ProviderError msg) = "Type provider error: " ++ msg
-pshow' i (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: " ++ pshow' i e
-pshow' i (ReflectionError parts orig) = let parts' = map (concat . intersperse " " . map showPart) parts in
-                                       concat (intersperse "\n" parts') ++
-                                       "\nOriginal error:\n" ++ indented (pshow' i orig)
-      where showPart :: ErrorReportPart -> String
-            showPart (TextPart str) = str
-            showPart (NamePart n)   = let colour = idris_colourRepl i in
-                                      showName (Just i) [] False colour n
-            showPart (TermPart tm)  = let colour = idris_colourRepl i
-                                      in showImp (Just i) False colour (delab i tm)
-            showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
-pshow' i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
-                                     indented (pshow' i err) ++
-                                     "\nThis is probably a bug. Please consider reporting it at " ++ bugaddr
+pprintErr :: IState -> Err -> Doc OutputAnnotation
+pprintErr i err = pprintErr' i (fmap (errReverse i) err)
 
+pprintErr' i (Msg s) = text s
+pprintErr' i (InternalMsg s) =
+  vsep [ text "INTERNAL ERROR:" <+> text s,
+         text "This is probably a bug, or a missing error message.",
+         text ("Please consider reporting at " ++ bugaddr)
+       ]
+pprintErr' i (CantUnify _ x y e sc s) =
+  text "Can't unify" <> indented (pprintTerm i (delab i x)) <$>
+  text "with" <> indented (pprintTerm i (delab i y)) <>
+  case e of
+    Msg "" -> empty
+    _ -> line <> line <> text "Specifically:" <>
+         indented (pprintErr' i e) <>
+         if (opt_errContext (idris_options i)) then text $ showSc i sc else empty
+pprintErr' i (CantConvert x y env) =
+  text "Can't convert" <> indented (pprintTerm i (delab i x)) <>
+  text "with" <> indented (pprintTerm i (delab i y)) <>
+  if (opt_errContext (idris_options i)) then text (showSc i env) else empty
+pprintErr' i (UnifyScope n out tm env) =
+  text "Can't unify" <> indented (annName n) <+>
+  text "with" <> indented (pprintTerm i (delab i tm)) <+>
+  text "as" <> indented (annName out) <> text "is not in scope" <>
+  if (opt_errContext (idris_options i)) then text (showSc i env) else empty
+pprintErr' i (CantInferType t) = text "Can't infer type for" <+> text t
+pprintErr' i (NonFunctionType f ty) =
+  pprintTerm i (delab i f) <+>
+  text "does not have a function type" <+>
+  parens (pprintTerm i (delab i ty))
+pprintErr' i (NotEquality tm ty) =
+  pprintTerm i (delab i tm) <+>
+  text "does not have an equality type" <+>
+  parens (pprintTerm i (delab i ty))
+pprintErr' i (TooManyArguments f) = text "Too many arguments for" <+> annName f
+pprintErr' i (CantIntroduce ty) =
+  text "Can't use lambda here: type is" <+> pprintTerm i (delab i ty)
+pprintErr' i (InfiniteUnify x tm env) =
+  text "Unifying" <+> annName' x (showbasic x) <+> text "and" <+> pprintTerm i (delab i tm) <+>
+  text "would lead to infinite value" <>
+  if (opt_errContext (idris_options i)) then text (showSc i env) else empty
+pprintErr' i (NotInjective p x y) =
+  text "Can't verify injectivity of" <+> pprintTerm i (delab i p) <+>
+  text " when unifying" <+> pprintTerm i (delab i x) <+> text "and" <+>
+  pprintTerm i (delab i y)
+pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)
+pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>
+                                    cat (punctuate comma (map text as))
+pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n
+pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n
+pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> pprintTerm i (delab i t)
+pprintErr' i UniverseError = text "Universe inconsistency"
+pprintErr' i ProgramLineComment = text "Program line next to comment"
+pprintErr' i (Inaccessible n) = annName n <+> text "is not an accessible pattern variable"
+pprintErr' i (NonCollapsiblePostulate n) = text "The return type of postulate" <+>
+                                           annName n <+> text "is not collapsible"
+pprintErr' i (AlreadyDefined n) = annName n<+>
+                                  text "is already defined"
+pprintErr' i (ProofSearchFail e) = pprintErr' i e
+pprintErr' i (NoRewriting tm) = text "rewrite did not change type" <+> pprintTerm i (delab i tm)
+pprintErr' i (At f e) = annotate (AnnFC f) (text (show f)) <> colon <> pprintErr' i e
+pprintErr' i (Elaborating s n e) = text "When elaborating" <+> text s <>
+                                   annName' n (showqual i n) <> colon <$>
+                                   pprintErr' i e
+pprintErr' i (ProviderError msg) = text ("Type provider error: " ++ msg)
+pprintErr' i (LoadingFailed fn e) = text "Loading" <+> text fn <+> text "failed:" <+>  pprintErr' i e
+pprintErr' i (ReflectionError parts orig) =
+  let parts' = map (hsep . map showPart) parts in
+  vsep parts' <> line <> line <>
+  text "Original error:" <$> indented (pprintErr' i orig)
+  where showPart :: ErrorReportPart -> Doc OutputAnnotation
+        showPart (TextPart str) = text str
+        showPart (NamePart n)   = annName n
+        showPart (TermPart tm)  = pprintTerm i (delab i tm)
+        showPart (SubReport rs) = indented . hsep . map showPart $ rs
+pprintErr' i (ReflectionFailed msg err) =
+  text "When attempting to perform error reflection, the following internal error occurred:" <>
+  indented (pprintErr' i err) <>
+  text ("This is probably a bug. Please consider reporting it at " ++ bugaddr)
+
+annName :: Name -> Doc OutputAnnotation
+annName n = annName' n (show n)
+
+annName' :: Name -> String -> Doc OutputAnnotation
+annName' n str = annotate (AnnName n Nothing Nothing) (text str)
 
 showSc i [] = ""
 showSc i xs = "\n\nIn context:\n" ++ showSep "\n" (map showVar (reverse xs))

src/Idris/ElabDecls.hs

@@ -67,12 +67,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
          ctxt <- getContext
          i <- getIState
 
-         logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'
+         logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
          ty' <- addUsingConstraints syn fc ty'
          ty' <- implicit syn n ty'
 
          let ty = addImpl i ty'
-         logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
+         logLvl 2 $ show n ++ " type " ++ showTmImpls ty
          ((tyT, defer, is), log) <-
                tclift $ elaborate ctxt n (TType (UVal 0)) []
                         (errAt "type of " n (erun fc (build i info False [] n ty)))
@@ -326,10 +326,10 @@ elabEliminator paramPos n ty cons info = do
   let clauseConsElimArgs = map getPiName consTerms
   let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
   let clauseGeneralArgs  = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
-  let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy
+  let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
   eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
   let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
-  elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
+  elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
   State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
   -- Do not elaborate clauses if there aren't any
   case eliminatorClauses of
@@ -814,7 +814,7 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
          i <- getIState
          t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
          let t = addImpl i t_in
-         logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
+         logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
          ((t', defer, is), log) <-
               tclift $ elaborate ctxt n (TType (UVal 0)) []
                        (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -959,9 +959,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
                               missing' <- filterM (checkPossible info fc True n) missing
                               let clhs = map getLHS pdef
                               logLvl 2 $ "Must be unreachable:\n" ++
-                                          showSep "\n" (map (showImp Nothing True False) missing') ++
+                                          showSep "\n" (map showTmImpls missing') ++
                                          "\nAgainst: " ++
-                                          showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
+                                          showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
                               -- filter out anything in missing' which is
                               -- matched by any of clhs. This might happen since
                               -- unification may force a variable to take a
@@ -1125,8 +1125,8 @@ elabPE info fc caller r =
             logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
                         showSep "\n" 
                            (map (\ (lhs, rhs) ->
-                              (showImp Nothing True False lhs ++ " = " ++ 
-                               showImp Nothing True False rhs)) pats)
+                              (showTmImpls lhs ++ " = " ++ 
+                               showTmImpls rhs)) pats)
             elabType info defaultSyntax "" fc opts newnm specTy
             let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
             elabClauses info fc opts newnm def
@@ -1180,7 +1180,7 @@ elabValBind info aspat tm_in
    = do ctxt <- getContext
         i <- getIState
         let tm = addImpl i tm_in
-        logLvl 10 (showImp Nothing True False tm)
+        logLvl 10 (showTmImpls tm)
         -- try:
         --    * ordinary elaboration
         --    * elaboration as a Type
@@ -1271,7 +1271,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
         let params = getParamsInType i [] fn_is fn_ty
         let lhs = stripUnmatchable i $
                     addImplPat i (propagateParams params (stripLinear i lhs_in))
-        logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
+        logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
         logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
 
         ((lhs', dlhs, []), _) <-
@@ -1286,7 +1286,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
         (clhs_c, clhsty) <- recheckC fc [] lhs_tm
         let clhs = normalise ctxt [] clhs_c
         
-        logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
+        logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
 
         rep <- useREPL
         when rep $ do
@@ -1312,10 +1312,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
         mapM_ (elabDecl' EAll info) wbefore
         -- Now build the RHS, using the type of the LHS as the goal.
         i <- getIState -- new implicits from where block
-        logLvl 5 (showImp Nothing True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))
+        logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
         let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
                                  (expandParams decorate newargs defs (defs \\ decls) rhs_in)
-        logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
+        logLvl 2 $ "RHS: " ++ showTmImpls rhs
         ctxt <- getContext -- new context with where block added
         logLvl 5 "STARTING CHECK"
         ((rhs', defer, is), _) <-
@@ -1468,7 +1468,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
         -- pattern bindings
         i <- getIState
         let lhs = addImplPat i (stripLinear i lhs_in)
-        logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
+        logLvl 5 ("LHS: " ++ showTmImpls lhs)
         ((lhs', dlhs, []), _) <-
             tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
               (errAt "left hand side of with in " fname
@@ -1481,7 +1481,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
         logLvl 5 ("Checked " ++ show clhs)
         let bargs = getPBtys lhs_tm
         let wval = addImplBound i (map fst bargs) wval_in
-        logLvl 5 ("Checking " ++ showImp Nothing True False wval)
+        logLvl 5 ("Checking " ++ showTmImpls wval)
         -- Elaborate wval in this context
         ((wval', defer, is), _) <-
             tclift $ elaborate ctxt (sMN 0 "withRHS")
@@ -1545,7 +1545,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
                     (map (pexp . (PRef fc) . fst) bargs_pre ++
                         pexp wval :
                     (map (pexp . (PRef fc) . fst) bargs_post))
-        logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)
+        logLvl 5 ("New RHS " ++ showTmImpls rhs)
         ctxt <- getContext -- New context with block added
         i <- getIState
         ((rhs', defer, is), _) <-
@@ -1576,8 +1576,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
     mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
         = do i <- getIState
              let tm = addImplPat i tm_in
-             logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
-                                      showImp Nothing True False toplhs)
+             logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
+                                      showTmImpls toplhs)
              case matchClause i toplhs tm of
                 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")
                 Right mvars ->
@@ -1587,8 +1587,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
     mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
         = do i <- getIState
              let tm = addImplPat i tm_in
-             logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
-                                      showImp Nothing True False toplhs)
+             logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
+                                      showTmImpls toplhs)
              withs' <- mapM (mkAuxC wname toplhs ns ns') withs
              case matchClause i toplhs tm of
                 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
@@ -1655,7 +1655,7 @@ elabClass info syn doc fc constraints tn ps ds
                                constraint
          let cons = [("", cn, cty, fc, [])]
          let ddecl = PDatadecl tn tty cons
-         logLvl 5 $ "Class data " ++ showDImp True ddecl
+         logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
          elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
          -- for each constraint, build a top level function to chase it
          logLvl 5 $ "Building functions"
@@ -1697,7 +1697,7 @@ elabClass info syn doc fc constraints tn ps ds
     getMName (PTy _ _ _ _ n _) = nsroot n
     tdecl allmeths (PTy doc syn _ o n t)
            = do t' <- implicit' syn allmeths n t
-                logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
+                logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
                 return ( (n, (toExp (map fst ps) Exp t')),
                          (n, (doc, o, (toExp (map fst ps) Imp t'))),
                          (n, (syn, o, t) ) )
@@ -1734,8 +1734,8 @@ elabClass info syn doc fc constraints tn ps ds
              let lhs = PApp fc (PRef fc cfn) [pconst capp]
              let rhs = PResolveTC (fileFC "HACK")
              let ty = PPi constraint (sMN 0 "pc") c con
-             iLOG (showImp Nothing True False ty)
-             iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
+             iLOG (showTmImpls ty)
+             iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
              i <- getIState
              let conn = case con of
                             PRef _ n -> n
@@ -1759,9 +1759,9 @@ elabClass info syn doc fc constraints tn ps ds
              let anames = map (\x -> sMN x "arg") [0..]
              let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
              let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
-             iLOG (showImp Nothing True False ty)
+             iLOG (showTmImpls ty)
              iLOG (show (m, ty', capp, margs))
-             iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
+             iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
              return [PTy doc syn fc o m ty',
                      PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
 
@@ -1849,7 +1849,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
          let wbTys = map mkTyDecl mtys
          let wbVals = map (decorateid (decorate ns iname)) ds'
          let wb = wbTys ++ wbVals
-         logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)
+         logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)
          logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
                                       show (concat (nub wparams))
          let lhs = PRef fc iname
@@ -2156,8 +2156,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)
 
 checkInferred :: FC -> PTerm -> PTerm -> Idris ()
 checkInferred fc inf user =
-     do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++
-                                     showImp Nothing True False user
+     do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++
+                                     showTmImpls user
         logLvl 10 $ "Checking match"
         i <- getIState
         tclift $ case matchClause' True i user inf of
@@ -2174,8 +2174,8 @@ checkInferred fc inf user =
 inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
 inferredDiff fc inf user =
      do i <- getIState
-        logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
-                                     showImp Nothing True False user
+        logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++
+                                     showTmImpls user
         tclift $ case matchClause' True i user inf of
             Right vs -> return False
             Left (x, y) -> return True

src/Idris/IdeSlave.hs

@@ -69,6 +69,23 @@ instance (SExpable a, SExpable b, SExpable c) => SExpable (a, b, c) where
 instance (SExpable a, SExpable b, SExpable c, SExpable d) => SExpable (a, b, c, d) where
   toSExp (l, m, n, o) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o]
 
+instance SExpable NameOutput where
+  toSExp TypeOutput = SymbolAtom "type"
+  toSExp FunOutput  = SymbolAtom "function"
+  toSExp DataOutput = SymbolAtom "data"
+
+instance SExpable OutputAnnotation where
+  toSExp (AnnName n Nothing   _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
+                                           (SymbolAtom "implicit", BoolAtom False)]
+  toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),
+                                           (SymbolAtom "decor", toSExp ty),
+                                           (SymbolAtom "implicit", BoolAtom False)]
+  toSExp (AnnBoundName n imp)    = toSExp [(SymbolAtom "name", StringAtom (show n)),
+                                           (SymbolAtom "decor", SymbolAtom "bound"),
+                                           (SymbolAtom "implicit", BoolAtom imp)]
+  toSExp AnnConstData            = toSExp [(SymbolAtom "decor", SymbolAtom "data")]
+  toSExp AnnConstType            = toSExp [(SymbolAtom "decor", SymbolAtom "type")]
+
 escape :: String -> String
 escape = concatMap escapeChar
   where

src/Idris/Parser.hs

@@ -1062,7 +1062,7 @@ loadSource h lidr f
                                    f file pos
                   unless (null ds') $ do
                     let ds = namespaces mname ds'
-                    logLvl 3 (showDecls True ds)
+                    logLvl 3 (show $ showDecls True ds)
                     i <- getIState
                     logLvl 10 (show (toAlist (idris_implicits i)))
                     logLvl 3 (show (idris_infixes i))

src/Idris/Prover.hs

@@ -89,47 +89,52 @@ elabStep st e = do case runStateT e st of
 
 dumpState :: IState -> ProofState -> Idris ()
 dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
-  iputGoal . render $ pretty nm <> colon <+> text "No more goals."
+  iputGoal . renderPretty 0.7 breakingSize $
+    prettyName False [] nm <> colon <+> text "No more goals."
 dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
   let OK ty  = goalAtFocus ps
   let OK env = envAtFocus ps
-  iputGoal . render $
-    prettyOtherGoals hs $$
-    prettyAssumptions env $$
-    prettyGoal ty
+  iputGoal . renderPretty 0.7 breakingSize $
+    prettyOtherGoals hs <> line <>
+    prettyAssumptions env <> line <>
+    prettyGoal (zip (assumptionNames env) (repeat False)) ty
   where
     -- XXX
-    tPretty t = pretty $ delab ist t
+    tPretty bnd t = pprintPTerm True bnd $ delab ist t
 
-    prettyPs [] = empty
-    prettyPs ((MN _ r, _) : bs) 
-        | r == txt "rewrite_rule" = prettyPs bs
-    prettyPs ((n, Let t v) : bs) =
-      nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
-        tPretty t $$ prettyPs bs)
-    prettyPs ((n, b) : bs) =
-      pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
+    assumptionNames :: Env -> [Name]
+    assumptionNames = map fst
 
-    prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
-    prettyG b = tPretty $ binderTy b
+    prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
+    prettyPs bnd [] = empty
+    prettyPs bnd ((n@(MN _ r), _) : bs)
+        | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
+    prettyPs bnd ((n, Let t v) : bs) =
+      nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
+        tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
+    prettyPs bnd ((n, b) : bs) =
+      line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs
 
-    prettyGoal ty =
-      text "----------                 Goal:                  ----------" $$
-      pretty h <> colon $$ nest nestingSize (prettyG ty)
+    prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
+    prettyG bnd b = tPretty bnd $ binderTy b
+
+    prettyGoal bnd ty =
+      text "----------                 Goal:                  ----------" <$$>
+      bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)
 
     prettyAssumptions env =
       if length env == 0 then
         empty
       else
-        text "----------              Assumptions:              ----------" $$
-        nest nestingSize (prettyPs $ reverse env)
+        text "----------              Assumptions:              ----------" <>
+        nest nestingSize (prettyPs [] $ reverse env)
 
     prettyOtherGoals hs =
       if length hs == 0 then
         empty
       else
-        text "----------              Other goals:              ----------" $$
-        pretty hs
+        text "----------              Other goals:              ----------" <$$>
+        nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
 
 lifte :: ElabState [PDecl] -> ElabD a -> Idris a
 lifte st e = do (v, _) <- elabStep st e

src/Idris/REPL.hs

@@ -448,10 +448,11 @@ process h fn (Eval t)
                                             ist <- getIState
                                             logLvl 3 $ "Raw: " ++ show (tm', ty')
                                             logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
-                                            imp <- impShow
-                                            c <- colourise
-                                            ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
-                                                     showImp (Just ist) imp c (delab ist ty'))
+                                            let imp = opt_showimp (idris_options ist)
+                                                tmDoc = prettyImp imp (delab ist tm')
+                                                tyDoc = prettyImp imp (delab ist ty')
+                                            ihPrintTermWithType h tmDoc tyDoc
+
 process h fn (ExecVal t)
                   = do ctxt <- getContext
                        ist <- getIState
@@ -459,10 +460,8 @@ process h fn (ExecVal t)
 --                       let tm' = normaliseAll ctxt [] tm
                        let ty' = normaliseAll ctxt [] ty
                        res <- execute tm
-                       imp <- impShow
-                       c <- colourise
-                       ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++
-                                showImp (Just ist) imp c (delab ist ty'))
+                       ihPrintResult h (showTm ist (delab ist res) ++ " : " ++
+                                        showTm ist (delab ist ty'))
 process h fn (Check (PRef _ n))
    = do ctxt <- getContext
         ist <- getIState
@@ -472,9 +471,7 @@ process h fn (Check (PRef _ n))
           ts@(t:_) ->
             case lookup t (idris_metavars ist) of
                 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
-                Nothing -> ihPrintResult h $
-                           concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++
-                                                                  showImp (Just ist) imp c (delabTy ist n)) $ ts
+                Nothing -> ihPrintFunTypes h n (map (\n -> (n, delabTy ist n)) ts)
           [] -> ihPrintError h $ "No such variable " ++ show n
   where
     showMetavarInfo c imp ist n i
@@ -487,27 +484,27 @@ process h fn (Check (PRef _ n))
                                    MN _ _ -> "_"
                                    UN nm | ('_':'_':_) <- str nm -> "_"
                                    _ -> showName (Just ist) [] False c n) ++
-                               " : " ++ showImp (Just ist) imp c t ++ "\n"
+                               " : " ++ showTm ist t ++ "\n"
                  in
                     current ++ putTy c imp ist (i-1) sc
     putTy c imp ist _ sc = putGoal c imp ist sc
     putGoal c imp ist g
                = "--------------------------------------\n" ++
                  showName (Just ist) [] False c n ++ " : " ++
-                 showImp (Just ist) imp c g
+                 showTm ist g
 
 
 process h fn (Check t)
    = do (tm, ty) <- elabVal toplevel False t
         ctxt <- getContext
         ist <- getIState
-        imp <- impShow
-        c <- colourise
-        let ty' = normaliseC ctxt [] ty
+        let imp = opt_showimp (idris_options ist)
+            ty' = normaliseC ctxt [] ty
         case tm of
-             TType _ -> ihPrintResult h ("Type : Type 1")
-             _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
-                                   showImp (Just ist) imp c (delab ist ty))
+           TType _ ->
+             ihPrintTermWithType h (prettyImp imp PType) type1Doc
+           _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))
+                                      (prettyImp imp (delab ist ty))
 
 process h fn (DocStr n)
                       = do i <- getIState
@@ -540,9 +537,9 @@ process h fn (Defn n)
                             [t] -> iputStrLn (showTotal t i)
                             _ -> return ()
     where printCase i (_, lhs, rhs)
-             = do c <- colourise
-                  iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++
-                             showImp (Just i) True c (delab i rhs))
+             = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
+               in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
+                             showTm i' (delab i rhs))
 process h fn (TotCheck n)
                         = do i <- getIState
                              case lookupNameTotal n (tt_ctxt i) of
@@ -848,7 +845,7 @@ process h fn (TestInline t)
                                 let tm' = inlineTerm ist tm
                                 imp <- impShow
                                 c <- colourise
-                                iPrintResult (showImp (Just ist) imp c (delab ist tm'))
+                                iPrintResult (showTm ist (delab ist tm'))
 process h fn Execute
                    = do (m, _) <- elabVal toplevel False
                                         (PApp fc
@@ -876,11 +873,11 @@ process h fn (Pattelab t)
 
 process h fn (Missing n)
     = do i <- getIState
-         c <- colourise
+         let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
          case lookupCtxt n (idris_patdefs i) of
                   [] -> return ()
                   [(_, tms)] ->
-                       iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))
+                       iPrintResult (showSep "\n" (map (showTm i') tms))
                   _ -> iPrintError $ "Ambiguous name"
 process h fn (DynamicLink l)
                            = do i <- getIState
@@ -949,9 +946,8 @@ dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
 dumpInstance :: Name -> Idris ()
 dumpInstance n = do i <- getIState
                     ctxt <- getContext
-                    imp <- impShow
                     case lookupTy n ctxt of
-                         ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
+                         ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts
 
 showTotal :: Totality -> IState -> String
 showTotal t@(Partial (Other ns)) i

src/Util/Pretty.hs

@@ -1,10 +1,11 @@
 module Util.Pretty (
-  module Text.PrettyPrint.HughesPJ,
+  module Text.PrettyPrint.Annotated.Leijen,
   Sized(..), breakingSize, nestingSize,
   Pretty(..)
 ) where
 
-import Text.PrettyPrint.HughesPJ
+--import Text.PrettyPrint.HughesPJ
+import Text.PrettyPrint.Annotated.Leijen
 
 -- A rough notion of size for pretty printing various types.
 class Sized a where
@@ -23,11 +24,7 @@ breakingSize = 15
 nestingSize :: Int
 nestingSize = 1
 
-class Pretty a where
-  pretty :: a -> Doc
+class Pretty a ty where
+  pretty :: a -> Doc ty
 
-instance Pretty () where
-  pretty () = text "()"
 
-instance Pretty a => Pretty [a] where
-  pretty l = foldr ($$) empty $ map pretty l

test/reg007/expected

@@ -1,13 +1,12 @@
 reg007.lidr:8:1:A.n is already defined
 reg007.lidr:12:9:When elaborating right hand side of hurrah:
 Can't unify
-	n = lala
+        n = lala
 with
-	0 = 1
+        0 = 1
 
 Specifically:
-	Can't unify
-		1
-	with
-		0
-
+        Can't unify
+                1
+        with
+                0

test/reg007/run

@@ -1,3 +1,3 @@
 #!/usr/bin/env bash
-idris --check $@ reg007.lidr
+idris --nocolour --check $@ reg007.lidr
 rm -f *.ibc

test/reg010/expected

@@ -1,12 +1,11 @@
 reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:
 Can't unify
-	P x
+        P x
 with
-	P y
+        P y
 
 Specifically:
-	Can't unify
-		P x
-	with
-		P y
-
+        Can't unify
+                P x
+        with
+                P y

test/reg023/expected

@@ -1,12 +1,11 @@
 reg023.idr:7:5:When elaborating right hand side of bad:
 Can't unify
-	Nat
+        Nat
 with
-	f Nat
+        f Nat
 
 Specifically:
-	Can't unify
-		Nat
-	with
-		f Nat
-
+        Can't unify
+                Nat
+        with
+                f Nat

test/test020/expected

@@ -1,14 +1,13 @@
 When elaborating right hand side of foo:
 test020a.idr:14:18:Can't unify
-	Vect n a
+        Vect n a
 with
-	List a
+        List a
 
 Specifically:
-	Can't unify
-		Vect n a
-	with
-		List a
-
+        Can't unify
+                Vect n a
+        with
+                List a
 [3, 2, 1]
 "Number 42"

test/test030/expected

@@ -1,12 +1,11 @@
 test030a.idr:12:14:When elaborating right hand side of testReflect1:
 Can't unify
-	IsJust (Just x)
+        IsJust (Just x)
 with
-	IsJust (prove (getProof x))
+        IsJust (prove (getProof x))
 
 Specifically:
-	Can't unify
-		Just x
-	with
-		Nothing
-
+        Can't unify
+                Just x
+        with
+                Nothing

test/test037/expected

@@ -1,18 +1,17 @@
 In file ErrorReflection.idr line 78 column 5 
-	When elaborating right hand side of  Main.bad : 
-		DSL type error: (t'(504) => t'(504)) doesn't match ()
+        When elaborating right hand side of  Main.bad : 
+                DSL type error: (t'(504) => t'(504)) doesn't match ()
 
 Original error:
 
-	ErrorReflection.idr:78:5:When elaborating right hand side of bad:
-	Can't unify
-		Tm [] (Main.TFun t' t')
-	with
-		Tm [] Main.TUnit
-	
-	Specifically:
-		Can't unify
-			Main.TFun t' t'
-		with
-			Main.TUnit
-
+        ErrorReflection.idr:78:5:When elaborating right hand side of bad:
+        Can't unify
+                Tm [] (TFun t' t')
+        with
+                Tm [] TUnit
+        
+        Specifically:
+                Can't unify
+                        TFun t' t'
+                with
+                        TUnit