    -- {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Setup up the emacs mode for Agda.

    module Agda.Setup.EmacsMode
      ( help
      -- * Locate
      , locateFlag
      , printEmacsModeFile
      -- * Setup
      , setupFlag
      , setupDotEmacs
      -- * Compile
      , compileFlag
      , compileElispFiles
      -- * Utilities
      , inform
      )
    where

    import Control.Applicative    ( liftA2 )
    import Control.Exception as E ( bracket, catch, evaluate, IOException )
    import Control.Monad          ( unless )

    import Data.Bifunctor         ( first, second )
    import Data.Bool              ( bool )
    import Data.Char              ( isAscii, isPrint )
    import Data.Functor           ( (<&>) )
    import Data.List              ( isInfixOf )
    import Data.Maybe             ( catMaybes, fromMaybe )

    import Numeric                ( showHex )

    import System.Directory       ( doesFileExist, findExecutable, getTemporaryDirectory, removeFile )
    import System.Exit            ( exitFailure, ExitCode(ExitSuccess) )
    import System.FilePath        ( (</>), getSearchPath )
    import System.IO              ( IOMode(ReadMode)
                                  , hClose, hSetEncoding, hGetContents, hPutStr, hPutStrLn
                                  , openTempFile, stderr, stdout, utf8, withFile
                                  )
    import System.Process         ( rawSystem, showCommandForUser )

    import Agda.Setup             ( getDataDir )
    import Agda.Setup.DataFiles   ( emacsLispFiles, emacsModeDir )

    -- Command line options.

    setupFlag :: String
    setupFlag :: [Char]
    setupFlag   = [Char]
    "setup"

    locateFlag :: String
    locateFlag :: [Char]
    locateFlag  = [Char]
    "locate"

    compileFlag :: String
    compileFlag :: [Char]
    compileFlag = [Char]
    "compile"

    -- | Help topic for @--emacs-mode@.

    help :: String
    help :: [Char]
    help = [[Char]] -> [Char]
    unlines
      [ [Char]
    "Option --emacs-mode allows to administer the Agda Emacs mode."
      , [Char]
    "It accepts three commands:"
      , [Char]
    ""
      , [Char]
    setupFlag
      , [Char]
    ""
      , [Char]
    "  This command unpacks Agda's data files, including the Emacs mode,"
      , [Char]
    "  into Agda's data directory (see option --print-agda-data-dir)."
      , [Char]
    ""
      , [Char]
    "  It then tries to add setup code for Agda's Emacs mode to the"
      , [Char]
    "  current user's .emacs file. It is assumed that the .emacs file"
      , [Char]
    "  uses the character encoding specified by the locale."
      , [Char]
    ""
      , [Char]
    compileFlag
      , [Char]
    ""
      , [Char]
    "  This command unpacks Agda's data files, including the Emacs mode,"
      , [Char]
    "  into Agda's data directory."
      , [Char]
    ""
      , [Char]
    "  It then tries to compile Agda's Emacs mode's source files."
      , [Char]
    ""
      , [Char]
    "  WARNING: If you reinstall the Agda mode without recompiling the Emacs"
      , [Char]
    "  Lisp files, then Emacs may continue using the old, compiled files."
      , [Char]
    ""
      , [Char]
    locateFlag
      , [Char]
    ""
      , [Char]
    "  The path to the Emacs mode's main file is printed on standard"
      , [Char]
    "  output (using the UTF-8 character encoding and no trailing"
      , [Char]
    "  newline)."
      ]

    ------------------------------------------------------------------------
    -- Locating the Agda mode

    -- | Prints out the path to the Agda mode's main file (using UTF-8 and
    -- without any trailing newline).

    printEmacsModeFile :: IO ()
    printEmacsModeFile :: IO ()
    printEmacsModeFile = do
      dataDir <- IO [Char]
    getDataDir
      let path = [Char]
    dataDir [Char] -> [Char] -> [Char]
    </> [Char]
    emacsModeDir [Char] -> [Char] -> [Char]
    </> [Char]
    "agda2.el"
      hSetEncoding stdout utf8
      putStr path

    ------------------------------------------------------------------------
    -- Setting up the .emacs file

    -- | Tries to set up the Agda mode in the given .emacs file.

    setupDotEmacs :: String -> IO ()
    setupDotEmacs :: [Char] -> IO ()
    setupDotEmacs [Char]
    agda = do
      let cmd :: [Char]
    cmd   = [Char]
    agda [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " --emacs-mode"
      let elisp :: [Char]
    elisp = [Char] -> [Char]
    setupString [Char]
    cmd

      dotEmacs <- IO [Char]
    findDotEmacs
      informLn $ "The .emacs file used: " ++ dotEmacs

      alreadyInstalled cmd dotEmacs >>= \case
        Bool
    True  -> do
          [Char] -> IO ()
    informLn [Char]
    "It seems as if setup has already been performed."
        Bool
    False -> do
          [Char] -> [Char] -> IO ()
    appendFile [Char]
    dotEmacs [Char]
    elisp
          [Char] -> IO ()
    inform ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $
            [ [Char]
    "Setup done. Try to (re)start Emacs and open an Agda file."
            , [Char]
    "The following text was appended to the .emacs file:"
            ] [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]]
    lines [Char]
    elisp

    -- | Tries to find the user's .emacs file by querying Emacs.

    findDotEmacs :: IO FilePath
    findDotEmacs :: IO [Char]
    findDotEmacs = [Char] -> IO [Char]
    askEmacs [Char]
    "(expand-file-name user-init-file)"

    -- | Has the Agda mode already been set up?

    alreadyInstalled :: String -> FilePath -> IO Bool
    alreadyInstalled :: [Char] -> [Char] -> IO Bool
    alreadyInstalled [Char]
    cmd [Char]
    dotEmacs = do
      [Char] -> IO Bool
    doesFileExist [Char]
    dotEmacs IO Bool -> (Bool -> IO Bool) -> IO Bool
    forall a b. IO a -> (a -> IO b) -> IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
        Bool
    False -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Bool
    True  -> [Char] -> IOMode -> (Handle -> IO Bool) -> IO Bool
    forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
    withFile [Char]
    dotEmacs IOMode
    ReadMode \ Handle
    f -> do
          txt <- Handle -> IO [Char]
    hGetContents Handle
    f
          evaluate $ identifier cmd `isInfixOf` txt
            -- Uses evaluate to ensure that the file is not closed prematurely.

    -- | If this string occurs in the .emacs file, then it is assumed that
    -- setup has already been performed.

    identifier :: String -> String
    identifier :: [Char] -> [Char]
    identifier [Char]
    cmd = [Char]
    cmd [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    locateFlag

    -- | The string appended to the end of the .emacs file.

    setupString :: String -> String
    setupString :: [Char] -> [Char]
    setupString [Char]
    cmd = [[Char]] -> [Char]
    unlines
      [ [Char]
    ""
      , [Char]
    "(load-file (let ((coding-system-for-read 'utf-8))"
      , [Char]
    "                (shell-command-to-string \""
                            [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [Char]
    identifier [Char]
    cmd [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\")))"
      ]

    ------------------------------------------------------------------------
    -- Querying Emacs

    -- | Evaluates the given Elisp command using Emacs. The output of the
    -- command (whatever was written into the current buffer) is returned.
    --
    -- Note: The input is not checked. The input is assumed to come from a
    -- trusted source.

    askEmacs :: String -> IO String
    askEmacs :: [Char] -> IO [Char]
    askEmacs [Char]
    query = do
      tempDir <- IO [Char]
    getTemporaryDirectory
      bracket (openTempFile tempDir "askEmacs")
              (removeFile . fst) $ \ ([Char]
    file, Handle
    h) -> do
        Handle -> IO ()
    hClose Handle
    h
        exit <- [Char] -> [[Char]] -> IO ExitCode
    rawSystemWithDiagnostics [Char]
    "emacs"
          [ [Char]
    "--batch"
              -- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern):
              -- Use Emacs batch mode so that it can run without a terminal.
          , [Char]
    "--user", [Char]
    ""
              -- The flag --user is necessary with --batch so that user-init-file is defined.
              -- The empty user is the default user.
              -- (Option --batch includes --no-init-file, this is reverted by supplying --user.)
          -- Andreas, 2022-05-25, issue #5901 reloaded:
          -- Loading the init file without loading the site fails for some users:
          -- , "--quick"
          --     -- Option --quick includes --no-site-file.
          , [Char]
    "--eval"
          , [[Char]] -> [Char]
    apply [ [Char]
    "with-temp-file", [Char] -> [Char]
    escape [Char]
    file, [[Char]] -> [Char]
    apply [ [Char]
    "insert", [Char]
    query ] ]
              -- Short cutting the temp file via just [ "princ", query ]
              -- does not work if the loading of the user-init-file prints extra stuff.
              -- Going via the temp file we can let this stuff go to stdout without
              -- affecting the output we care about.
          ]
        unless (exit == ExitSuccess) do
          informLn "Unable to query Emacs."
          exitFailure
        withFile file ReadMode \ Handle
    h -> do
          result <- Handle -> IO [Char]
    hGetContents Handle
    h
          _ <- evaluate (length result)
            -- Uses evaluate to ensure that the file is not closed prematurely.
          return result

    -- | Like 'rawSystem' but handles 'IOException' by printing diagnostics
    -- (@PATH@) before 'exitFailure'.

    rawSystemWithDiagnostics
      :: FilePath  -- ^ Command to run.
      -> [String]  -- ^ Arguments to command.
      -> IO ExitCode
    rawSystemWithDiagnostics :: [Char] -> [[Char]] -> IO ExitCode
    rawSystemWithDiagnostics [Char]
    cmd [[Char]]
    args =
        [Char] -> [[Char]] -> IO ExitCode
    rawSystem [Char]
    cmd [[Char]]
    args
      IO ExitCode -> (IOException -> IO ExitCode) -> IO ExitCode
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` \ (IOException
    e :: IOException) -> do
         [Char] -> IO ()
    informLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords [ [Char]
    "FAILED:", [Char] -> [[Char]] -> [Char]
    showCommandForUser [Char]
    cmd [[Char]]
    args ]
         [Char] -> IO ()
    informLn ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unwords [ [Char]
    "Exception:", IOException -> [Char]
    forall a. Show a => a -> [Char]
    show IOException
    e ]
         -- The PATH might be useful in other exceptions, like "permission denied".
         path <- [Char] -> Maybe [Char] -> [Char]
    forall a. a -> Maybe a -> a
    fromMaybe [Char]
    "(not found)" (Maybe [Char] -> [Char]) -> IO (Maybe [Char]) -> IO [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Char] -> IO (Maybe [Char])
    findExecutable [Char]
    cmd
         informLn $ unwords [ "Executable", cmd, "at:", path ]
         informLn "PATH:"
         mapM_ (informLn . ("  - " ++)) =<< getSearchPath
         exitFailure

    -- | Escapes the string so that Emacs can parse it as an Elisp string.

    escape :: FilePath -> FilePath
    escape :: [Char] -> [Char]
    escape [Char]
    s = [Char]
    "\"" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ (Char -> [Char]) -> [Char] -> [Char]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Char -> [Char]
    esc [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\""
      where
      esc :: Char -> [Char]
    esc Char
    c | Char
    c Char -> [Char] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Char
    '\\', Char
    '"']   = Char
    '\\' Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : [Char
    c]
            | Char -> Bool
    isAscii Char
    c Bool -> Bool -> Bool
    && Char -> Bool
    isPrint Char
    c = [Char
    c]
            | Bool
    otherwise              = [Char]
    "\\x" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char] -> [Char]
    forall a. Integral a => a -> [Char] -> [Char]
    showHex (Char -> Int
    forall a. Enum a => a -> Int
    fromEnum Char
    c) [Char]
    "\\ "

    ------------------------------------------------------------------------
    -- Compiling Emacs Lisp files

    -- | Tries to compile the Agda mode's Emacs Lisp files.

    compileElispFiles :: IO ()
    compileElispFiles :: IO ()
    compileElispFiles = do
      dataDir <- IO [Char]
    getDataDir IO [Char] -> ([Char] -> [Char]) -> IO [Char]
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> ([Char] -> [Char] -> [Char]
    </> [Char]
    emacsModeDir)
      let elFiles = ([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char]
    dataDir [Char] -> [Char] -> [Char]
    </>) [[Char]]
    emacsLispFiles
      (existing, missing) <- partitionM doesFileExist elFiles
      failed <- catMaybes <$> mapM (compile dataDir) existing

      -- If any of the .el files was missing or failed to compile, fail execution.
      unless (null missing) $ do
        informLn "Missing Emacs Lisp files:"
        mapM_ (informLn . ("  " ++)) missing
      unless (null failed) $ do
        informLn "Unable to compile the following Emacs Lisp files:"
        mapM_ (informLn . ("  " ++)) failed
      unless (null missing && null failed) exitFailure

      where
      compile :: [Char] -> [Char] -> IO (Maybe [Char])
    compile [Char]
    dataDir [Char]
    f = do
        exit <- [Char] -> [[Char]] -> IO ExitCode
    rawSystemWithDiagnostics [Char]
    "emacs" ([[Char]] -> IO ExitCode) -> [[Char]] -> IO ExitCode
    forall a b. (a -> b) -> a -> b
    $
          [ [Char]
    "--quick"                -- 'quick' implies 'no-site-file'
          , [Char]
    "--directory", [Char]
    dataDir
          , [Char]
    "--batch"                -- 'batch' implies 'no-init-file' but not 'no-site-file'.
          , [Char]
    "--eval"
          , [Char]
    "(progn \
               \(setq byte-compile-error-on-warn t) \
               \(byte-compile-disable-warning 'cl-functions) \
               \(batch-byte-compile))"
          , [Char]
    f
          ]
        return $ if exit == ExitSuccess then Nothing else Just f

    ------------------------------------------------------------------------
    -- Helper functions

    -- These functions inform the user about something by printing on
    -- stderr.

    inform :: String -> IO ()
    inform :: [Char] -> IO ()
    inform   = Handle -> [Char] -> IO ()
    hPutStr   Handle
    stderr

    informLn :: String -> IO ()
    informLn :: [Char] -> IO ()
    informLn = Handle -> [Char] -> IO ()
    hPutStrLn Handle
    stderr

    parens :: String -> String
    parens :: [Char] -> [Char]
    parens [Char]
    s = [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [ [Char]
    "(", [Char]
    s, [Char]
    ")" ]

    -- LISP application
    apply :: [String] -> String
    apply :: [[Char]] -> [Char]
    apply = [Char] -> [Char]
    parens ([Char] -> [Char]) -> ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Char]] -> [Char]
    unwords

    -- Utilities

    -- | A ``monadic'' version of @'partition' :: (a -> Bool) -> [a] -> ([a],[a])
    partitionM :: Applicative m => (a -> m Bool) -> [a] -> m ([a], [a])
    partitionM :: forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m ([a], [a])
    partitionM a -> m Bool
    f =
      (a -> m ([a], [a]) -> m ([a], [a]))
    -> m ([a], [a]) -> [a] -> m ([a], [a])
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ a
    x -> (Bool -> ([a], [a]) -> ([a], [a]))
    -> m Bool -> m ([a], [a]) -> m ([a], [a])
    forall a b c. (a -> b -> c) -> m a -> m b -> m c
    forall (f :: * -> *) a b c.
    Applicative f =>
    (a -> b -> c) -> f a -> f b -> f c
    liftA2 ((([a], [a]) -> ([a], [a]))
    -> (([a], [a]) -> ([a], [a])) -> Bool -> ([a], [a]) -> ([a], [a])
    forall a. a -> a -> Bool -> a
    bool (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
    forall b c a. (b -> c) -> (a, b) -> (a, c)
    forall (p :: * -> * -> *) b c a.
    Bifunctor p =>
    (b -> c) -> p a b -> p a c
    second (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :)) (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
    forall a b c. (a -> b) -> (a, c) -> (b, c)
    forall (p :: * -> * -> *) a b c.
    Bifunctor p =>
    (a -> b) -> p a c -> p b c
    first (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :))) (m Bool -> m ([a], [a]) -> m ([a], [a]))
    -> m Bool -> m ([a], [a]) -> m ([a], [a])
    forall a b. (a -> b) -> a -> b
    $ a -> m Bool
    f a
    x)
            (([a], [a]) -> m ([a], [a])
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([], []))