-
Notifications
You must be signed in to change notification settings - Fork 339
/
Main.hs
288 lines (242 loc) · 9 KB
/
Main.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
{-# 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 "(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"
[ "--batch"
-- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern):
-- Use Emacs batch mode so that it can run without a terminal.
, "--user", ""
-- 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.
, "--eval"
, apply [ "with-temp-file", escape file, apply [ "insert", 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 $ \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" $
[ "--quick" -- 'quick' implies 'no-site-file'
, "--directory", dataDir
, "--batch" -- 'batch' implies 'no-init-file' but not 'no-site-file'.
, "--eval"
, "(progn \
\(setq debug-on-error t) \
\(setq byte-compile-error-on-warn t) \
\(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
parens :: String -> String
parens s = concat [ "(", s, ")" ]
-- LISP application
apply :: [String] -> String
apply = parens . unwords