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 as 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 Aspects
ann = 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 ()) -> Maybe Aspect -> IO ()
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect Aspects
ann
    end :: p -> IO ()
end p
_ann  = [SGR] -> IO ()
setSGR [SGR
Reset]

    aspSGR :: Aspect -> [SGR]
    aspSGR :: Aspect -> [SGR]
aspSGR = \case
      Aspect
String        -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Red]
      Aspect
Number        -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Magenta]
      Aspect
PrimitiveType -> [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Dull Color
Blue]
      Name Maybe NameKind
Nothing Bool
_ -> []
      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]
      Aspect
Aspect.Background -> []
      Aspect
Comment           -> []
      Aspect
Hole              -> []
      Aspect
Keyword           -> []
      Aspect
Markup            -> []
      Aspect
Pragma            -> []
      Aspect
Symbol            -> []

putDoc :: (MonadIO m, HasOptions m) => Doc -> m ()
putDoc :: forall (m :: * -> *). (MonadIO m, HasOptions m) => Doc -> m ()
putDoc Doc
doc = do
  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)
  wantscol <- commandLineOptions
  let
    col = case CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour CommandLineOptions
wantscol of
      DiagnosticsColours
AutoColour   -> Bool
outputcol
      DiagnosticsColours
AlwaysColour -> Bool
True
      DiagnosticsColours
NeverColour  -> Bool
False

  liftIO $ if col
    then renderAnsiIO doc
    else putStrLn (render doc)