{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

module Agda.Syntax.Common.Pretty.ANSI ( printTreeAnsi, putDocLn, putDocTree, putDocTreeLn ) where

import Control.Monad.IO.Class ( MonadIO(..) )
import Data.Functor ((<&>))
import Data.Text    qualified as Text
import Data.Text.IO qualified as Text

import System.Console.ANSI
import System.Console.ANSI.Codes ( osc )
import System.IO ( stdout )

-- UNUSED:
-- import Text.PrettyPrint.Annotated.HughesPJ ( renderDecoratedM )

import Agda.Interaction.Options.HasOptions ( HasOptions(commandLineOptions) )
import Agda.Interaction.Options.Base

import Agda.Syntax.Common.Aspect as Aspect
import Agda.Syntax.Common.Pretty ( Doc, DocTree )

import Agda.Utils.DocTree (renderTree', renderToTree, treeToTextNoAnn)

-- | Print an annotated, pretty-printing 'DocTree' onto a VT100-compatible terminal.
printTreeAnsi :: DocTree -> IO ()
printTreeAnsi :: DocTree -> IO ()
printTreeAnsi = (Text -> IO ()) -> (Aspects -> IO () -> IO ()) -> DocTree -> IO ()
forall ann t.
Monoid t =>
(Text -> t) -> (ann -> t -> t) -> DocTree ann -> t
renderTree' Text -> IO ()
Text.putStr \ Aspects
ann IO ()
t -> Aspects -> IO ()
startAnn Aspects
ann IO () -> IO () -> IO ()
forall a. Semigroup a => a -> a -> a
<> IO ()
t IO () -> IO () -> IO ()
forall a. Semigroup a => a -> a -> a
<> Aspects -> IO ()
endAnn Aspects
ann

startAnn :: Aspects -> IO ()
startAnn :: Aspects -> IO ()
startAnn 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 (\ Aspect
a -> [SGR] -> IO ()
setSGR (Aspect -> [SGR]
aspSGR Aspect
a) IO () -> IO () -> IO ()
forall a. Semigroup a => a -> a -> a
<> Aspect -> IO ()
startIO Aspect
a) (Maybe Aspect -> IO ()) -> Maybe Aspect -> IO ()
forall a b. (a -> b) -> a -> b
$ Aspects -> Maybe Aspect
aspect Aspects
ann

endAnn :: Aspects -> IO ()
endAnn :: Aspects -> IO ()
endAnn 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 Aspect -> IO ()
endIO (Aspects -> Maybe Aspect
aspect Aspects
ann) IO () -> IO () -> IO ()
forall a. Semigroup a => a -> a -> a
<> [SGR] -> IO ()
setSGR [SGR
Reset]

-- Andreas, 2025-07-28
-- ansi-terminal has no good interface for hyperlinks in the start/end style,
-- so we have to implement this manually here, breaking the abstraction.
startIO :: Aspect -> IO ()
startIO :: Aspect -> IO ()
startIO = \case
  URL Text
ref -> [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
osc [Char]
"8" ([Char]
";" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack Text
ref)
  Aspect
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

endIO :: Aspect -> IO ()
endIO :: Aspect -> IO ()
endIO = \case
  URL Text
_ -> [Char] -> IO ()
putStr ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
osc [Char]
"8" [Char]
";"
  Aspect
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

aspSGR :: Aspect -> [SGR]
aspSGR :: Aspect -> [SGR]
aspSGR = \case
  URL Text
_url      -> [Underlining -> SGR
SetUnderlining Underlining
SingleUnderline]
  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            -> []

-- UNUSED:
-- -- | Render an annotated, pretty-printing 'Doc'ument to a VT100-compatible terminal.
-- renderAnsiIO :: Doc -> IO ()
-- renderAnsiIO = renderDecoratedM startAnn endAnn putStr (putStr "\n")

putDocTree :: (MonadIO m, HasOptions m) => DocTree -> m ()
putDocTree :: forall (m :: * -> *). (MonadIO m, HasOptions m) => DocTree -> m ()
putDocTree DocTree
doc = do
  col <- m CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions m CommandLineOptions
-> (CommandLineOptions -> DiagnosticsColours)
-> m DiagnosticsColours
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> CommandLineOptions -> DiagnosticsColours
optDiagnosticsColour m DiagnosticsColours -> (DiagnosticsColours -> m Bool) -> m Bool
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    DiagnosticsColours
AutoColour   -> 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)
    DiagnosticsColours
AlwaysColour -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    DiagnosticsColours
NeverColour  -> Bool -> m Bool
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

  liftIO do
    if col
      then printTreeAnsi doc
      else Text.putStr (treeToTextNoAnn doc)

putDocTreeLn :: (MonadIO m, HasOptions m) => DocTree -> m ()
putDocTreeLn :: forall (m :: * -> *). (MonadIO m, HasOptions m) => DocTree -> m ()
putDocTreeLn DocTree
doc = do
  DocTree -> m ()
forall (m :: * -> *). (MonadIO m, HasOptions m) => DocTree -> m ()
putDocTree DocTree
doc
  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
$ [Char] -> IO ()
putStr [Char]
"\n"

putDoc :: (MonadIO m, HasOptions m) => Doc -> m ()
putDoc :: forall (m :: * -> *). (MonadIO m, HasOptions m) => Doc -> m ()
putDoc = DocTree -> m ()
forall (m :: * -> *). (MonadIO m, HasOptions m) => DocTree -> m ()
putDocTree (DocTree -> m ()) -> (Doc -> DocTree) -> Doc -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> DocTree
forall ann. Null ann => Doc ann -> DocTree ann
renderToTree

putDocLn :: (MonadIO m, HasOptions m) => Doc -> m ()
putDocLn :: forall (m :: * -> *). (MonadIO m, HasOptions m) => Doc -> m ()
putDocLn Doc
doc = do
  Doc -> m ()
forall (m :: * -> *). (MonadIO m, HasOptions m) => Doc -> m ()
putDoc Doc
doc
  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
$ [Char] -> IO ()
putStr [Char]
"\n"