{-# LANGUAGE ScopedTypeVariables #-} -- | A program which either tries to add setup code for Agda's Emacs -- mode to the users .emacs file, or provides information to Emacs -- about where the Emacs mode is installed. module Main (main) where import Control.Exception as E import Control.Monad import Data.Char import Data.List (intercalate, isInfixOf) import Data.Maybe import Data.Version import Numeric import System.Directory import System.Environment import System.Exit import System.FilePath import System.IO -- import System.IO.Error (isDoesNotExistError) import System.Process import Paths_Agda (getDataDir, version) -- | The program. main :: IO () main = do prog <- getProgName args <- getArgs case args of [arg] | arg == locateFlag -> printEmacsModeFile | arg == setupFlag -> do dotEmacs <- findDotEmacs setupDotEmacs (Files { thisProgram = prog , dotEmacs = dotEmacs }) | arg == compileFlag -> compileElispFiles _ -> do inform usage exitFailure -- Command line options. setupFlag = "setup" locateFlag = "locate" compileFlag = "compile" -- | Usage information. usage :: String usage = unlines [ "This program, which is part of Agda version " ++ ver ++ ", can be run" , "in three modes, depending on which option it is invoked with:" , "" , setupFlag , "" , " The program tries to add setup code for Agda's Emacs mode to the" , " current user's .emacs file. It is assumed that the .emacs file" , " uses the character encoding specified by the locale." , "" , locateFlag , "" , " The path to the Emacs mode's main file is printed on standard" , " output (using the UTF-8 character encoding and no trailing" , " newline)." , "" , compileFlag , "" , " The program tries to compile Agda's Emacs mode's source files." , "" , " WARNING: If you reinstall the Agda mode without recompiling the Emacs" , " Lisp files, then Emacs may continue using the old, compiled files." ] -- | The current version of Agda. ver :: String ver = intercalate "." $ map show $ versionBranch version ------------------------------------------------------------------------ -- 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 = do dataDir <- getDataDir let path = dataDir "emacs-mode" "agda2.el" hSetEncoding stdout utf8 putStr path ------------------------------------------------------------------------ -- Setting up the .emacs file data Files = Files { dotEmacs :: FilePath -- ^ The .emacs file. , thisProgram :: FilePath -- ^ The name of the current program. } -- | Tries to set up the Agda mode in the given .emacs file. setupDotEmacs :: Files -> IO () setupDotEmacs files = do informLn $ "The .emacs file used: " ++ dotEmacs files already <- alreadyInstalled files if already then informLn "It seems as if setup has already been performed." else do appendFile (dotEmacs files) (setupString files) inform $ unlines $ [ "Setup done. Try to (re)start Emacs and open an Agda file." , "The following text was appended to the .emacs file:" ] ++ lines (setupString files) -- | Tries to find the user's .emacs file by querying Emacs. findDotEmacs :: IO FilePath findDotEmacs = askEmacs "(insert (expand-file-name user-init-file))" -- | Has the Agda mode already been set up? alreadyInstalled :: Files -> IO Bool alreadyInstalled files = do exists <- doesFileExist (dotEmacs files) if not exists then return False else withFile (dotEmacs files) ReadMode $ (evaluate . (identifier files `isInfixOf`)) <=< hGetContents -- 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 :: Files -> String identifier files = takeFileName (thisProgram files) ++ " " ++ locateFlag -- | The string appended to the end of the .emacs file. setupString :: Files -> String setupString files = unlines [ "" , "(load-file (let ((coding-system-for-read 'utf-8))" , " (shell-command-to-string \"" ++ identifier files ++ "\")))" ] ------------------------------------------------------------------------ -- 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 query = do tempDir <- getTemporaryDirectory bracket (openTempFile tempDir "askEmacs") (removeFile . fst) $ \(file, h) -> do hClose h exit <- rawSystemWithDiagnostics "emacs" [ "--no-desktop", "-nw", "--no-splash" -- Andreas, 2014-01-11: ^ try a leaner startup of emacs -- Andreas, 2018-09-08: -nw instead of --no-window-system as some emacses do not support the long version , "--eval" , "(with-temp-file " ++ escape file ++ " " ++ query ++ ")" , "--kill" ] unless (exit == ExitSuccess) $ do informLn "Unable to query Emacs." exitFailure withFile file ReadMode $ \h -> do result <- hGetContents 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 cmd args = rawSystem cmd args `E.catch` \ (e :: IOException) -> do informLn $ unwords [ "FAILED:", showCommandForUser cmd args ] informLn $ unwords [ "Exception:", show e ] -- The PATH might be useful in other exceptions, like "permission denied". -- when (isDoesNotExistError e) $ do path <- fromMaybe "(not found)" <$> findExecutable 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 s = "\"" ++ concatMap esc s ++ "\"" where esc c | c `elem` ['\\', '"'] = '\\' : [c] | isAscii c && isPrint c = [c] | otherwise = "\\x" ++ showHex (fromEnum c) "\\ " ------------------------------------------------------------------------ -- Compiling Emacs Lisp files -- | The Agda mode's Emacs Lisp files, given in the order in which -- they should be compiled. emacsLispFiles :: [FilePath] emacsLispFiles = [ "agda2-abbrevs.el" , "annotation.el" , "agda2-queue.el" , "eri.el" , "agda2.el" , "agda-input.el" , "agda2-highlight.el" , "agda2-mode.el" ] -- | Tries to compile the Agda mode's Emacs Lisp files. compileElispFiles :: IO () compileElispFiles = do dataDir <- ( "emacs-mode") <$> getDataDir let elFiles = map (dataDir ) emacsLispFiles elFiles <- filterM doesFileExist elFiles results <- mapM (compile dataDir) elFiles case catMaybes results of [] -> return () fs -> do informLn "Unable to compile the following Emacs Lisp files:" mapM_ (informLn . (" " ++)) fs exitFailure where compile dataDir f = do exit <- rawSystemWithDiagnostics "emacs" $ [ "--no-init-file", "--no-site-file" , "--directory", dataDir , "--batch" , "--eval" , "(progn \ \(setq byte-compile-error-on-warn t) \ \(byte-compile-disable-warning 'cl-functions) \ \(batch-byte-compile))" , f ] return $ if exit == ExitSuccess then Nothing else Just f ------------------------------------------------------------------------ -- Helper functions -- These functions inform the user about something by printing on -- stderr. inform = hPutStr stderr informLn = hPutStrLn stderr