module Main (main) where
import Control.Exception
import Control.Monad
import Data.Char
import Data.List
import Data.Version
import Numeric
import System.Directory
import System.Environment
import System.Exit
import System.FilePath
import System.IO
#if !(MIN_VERSION_base(4,2,0))
import qualified System.IO.UTF8 as UTF8
#endif
import System.Process
import Paths_Agda (getDataDir, version)
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
})
_ -> do inform usage
exitFailure
setupFlag = "setup"
locateFlag = "locate"
usage :: String
usage = unlines
[ "This program, which is part of Agda version " ++ ver ++ ", can be run"
, "in two 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"
#if MIN_VERSION_base(4,2,0)
, " uses the character encoding specified by the locale."
#else
, " uses ASCII or some other character encoding which ASCII is"
, " compatible with (like Latin-1 or UTF-8)."
#endif
, ""
, 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)."
]
ver :: String
ver = intercalate "." $ map show $
versionBranch version
printEmacsModeFile :: IO ()
printEmacsModeFile = do
dataDir <- getDataDir
let path = dataDir </> "emacs-mode" </> "agda2.el"
#if MIN_VERSION_base(4,2,0)
hSetEncoding stdout utf8
putStr path
#else
UTF8.putStr path
#endif
data Files = Files { dotEmacs :: FilePath
, thisProgram :: FilePath
}
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)
findDotEmacs :: IO FilePath
findDotEmacs = askEmacs "(insert (expand-file-name user-init-file))"
alreadyInstalled :: Files -> IO Bool
alreadyInstalled files = do
exists <- doesFileExist (dotEmacs files)
if not exists then return False else
withFile (dotEmacs files) ReadMode $ \h ->
evaluate . (identifier files `isInfixOf`) =<< hGetContents h
identifier :: Files -> String
identifier files =
takeFileName (thisProgram files) ++ " " ++ locateFlag
setupString :: Files -> String
setupString files = unlines
[ ""
, "(load-file (let ((coding-system-for-read 'utf-8))"
, " (shell-command-to-string \""
++ identifier files ++ "\")))"
]
askEmacs :: String -> IO String
askEmacs query = do
tempDir <- getTemporaryDirectory
bracket (openTempFile tempDir "askEmacs")
(removeFile . fst) $ \(file, h) -> do
hClose h
exit <- rawSystem "emacs"
[ "--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)
return result
escape :: FilePath -> FilePath
escape s = "\"" ++ concatMap esc s ++ "\""
where
esc c | c `elem` ['\\', '"'] = '\\' : [c]
| isAscii c && isPrint c = [c]
| otherwise = "\\x" ++ showHex (fromEnum c) "\\ "
inform = hPutStr stderr
informLn = hPutStrLn stderr