module Agda.Syntax.Common.Pretty.ANSI where
import Control.Monad.IO.Class
import Control.Monad

import Text.PrettyPrint.Annotated.HughesPJ (renderDecoratedM)

import Agda.Interaction.Options.HasOptions
import Agda.Interaction.Options.Base
import Agda.Syntax.Common.Aspect
import Agda.Syntax.Common.Pretty
import Agda.Utils.Monad

import System.Console.ANSI
import System.IO

-- | Render an annotated, pretty-printing 'Doc'ument into a string
-- suitable for printing on VT100-compatible terminals.
renderAnsiIO :: Doc -> IO ()
renderAnsiIO :: Doc -> IO ()
renderAnsiIO = (Aspects -> IO ())
-> (Aspects -> IO ()) -> (String -> IO ()) -> IO () -> Doc -> IO ()
forall (m :: * -> *) ann r.
Monad m =>
(ann -> m r)
-> (ann -> m r) -> (String -> m r) -> m r -> Doc ann -> m r
renderDecoratedM Aspects -> IO ()
start Aspects -> IO ()
forall {p}. p -> IO ()
end String -> IO ()
putStr (String -> IO ()
putStr String
"\n") where
  start :: Aspects -> IO ()
start = IO () -> (Aspect -> IO ()) -> Maybe Aspect -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe IO ()
forall a. Monoid a => a
mempty ([SGR] -> IO ()
setSGR ([SGR] -> IO ()) -> (Aspect -> [SGR]) -> Aspect -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aspect -> [SGR]
aspSGR) (Maybe Aspect -> IO ())
-> (Aspects -> Maybe Aspect) -> Aspects -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Aspects -> Maybe Aspect
aspect
  end :: p -> IO ()
end p
_ = [SGR] -> IO ()
setSGR [SGR
Reset]

  aspSGR :: Aspect -> [SGR]
  aspSGR :: Aspect -> [SGR]
aspSGR Aspect
String        = [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Red]
  aspSGR Aspect
Number        = [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Magenta]
  aspSGR Aspect
PrimitiveType = [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]
  aspSGR (Name (Just NameKind
nk) Bool
_) = case NameKind
nk of
    NameKind
Bound                   -> []
    NameKind
Generalizable           -> []
    NameKind
Argument                -> []

    Constructor Induction
Inductive   -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Green]
    Constructor Induction
CoInductive -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Green]

    NameKind
Field                   -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Magenta]

    NameKind
Module                  -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Magenta]

    NameKind
Function                -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]
    NameKind
Postulate               -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]
    NameKind
Datatype                -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]
    NameKind
Record                  -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]
    NameKind
Primitive               -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]

    NameKind
Macro                   -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Cyan]
  aspSGR Aspect
_ = []

putDoc :: (MonadIO m, HasOptions m) => Doc -> m ()
putDoc :: forall (m :: * -> *). (MonadIO m, HasOptions m) => Doc -> m ()
putDoc Doc
doc = do
  Bool
outputcol <- IO Bool -> m Bool
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Handle -> IO Bool
hSupportsANSI Handle
stdout)
  CommandLineOptions
wantscol <- m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let
    col :: Bool
col = case CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour CommandLineOptions
wantscol of
      DiagnosticsColours
AutoColour   -> Bool
outputcol
      DiagnosticsColours
AlwaysColour -> Bool
True
      DiagnosticsColours
NeverColour  -> Bool
False

  IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ if Bool
col
    then Doc -> IO ()
renderAnsiIO Doc
doc
    else String -> IO ()
putStrLn (Doc -> String
forall a. Doc a -> String
render Doc
doc)