1
;;; agda2-mode.el --- Major mode for Agda
7
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13
(defvar agda2-version "2.2.4"
14
"The version of the Agda mode.
15
Note that, by default, the same version of the underlying Haskell
16
library is used (see `agda2-ghci-options').")
18
(require 'cl) ; haskell-indent requires it anyway.
19
(set (make-local-variable 'lisp-indent-function)
20
'common-lisp-indent-function)
26
(require 'agda2-highlight)
27
(require 'agda2-abbrevs)
28
(require 'haskell-indent)
29
(require 'haskell-ghci)
30
;; due to a bug in haskell-mode-2.1
31
(setq haskell-ghci-mode-map (copy-keymap comint-mode-map))
32
;; Load filladapt, if it is installed.
36
(unless (fboundp 'overlays-in) (load "overlay")) ; for Xemacs
37
(unless (fboundp 'propertize) ; for Xemacs 21.4
38
(defun propertize (string &rest properties)
39
"Return a copy of STRING with text properties added.
40
First argument is the string to copy.
41
Remaining arguments form a sequence of PROPERTY VALUE pairs for text
42
properties to add to the result."
43
(let ((str (copy-sequence string)))
44
(add-text-properties 0 (length str) properties str)
46
(unless (fboundp 'run-mode-hooks)
47
(fset 'run-mode-hooks 'run-hooks)) ; For Emacs versions < 21.
49
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
52
(defmacro agda2-protect (form &optional default)
53
"Expands to (condition-case nil FORM (error DEFAULT))."
54
`(condition-case nil ,form (error ,default)))
55
(put 'agda2-protect 'lisp-indent-function 0)
57
(defmacro agda2-let (varbind funcbind &rest body)
58
"Expands to (let* VARBIND (labels FUNCBIND BODY...))."
59
`(let* ,varbind (labels ,funcbind ,@body)))
60
(put 'agda2-let 'lisp-indent-function 2)
62
(defun agda2-chunkify (n xs)
63
"Returns a list containing chunks of XS of length at most N.
64
All the elements of XS are included, in their original order."
69
(let ((new-i (+ i (min n (- len i)))))
70
(setq out (cons (subseq xs i new-i) out))
74
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
78
"Major mode for interactively developing Agda programs."
81
(defcustom agda2-include-dirs
83
"The directories Agda uses to search for files.
84
The directory names should be relative to the root of the current project."
85
:type '(repeat directory)
88
(defcustom agda2-ghci-options
89
(list (concat "-package Agda-" agda2-version))
90
"Options set in GHCi before loading `agda2-toplevel-module'.
91
Note that only dynamic options can be set using this variable."
92
:type '(repeat string)
95
(defcustom agda2-toplevel-module "Agda.Interaction.GhciTop"
96
"The name of the Agda toplevel module."
97
:type 'string :group 'agda2)
99
(defcustom agda2-mode-hook
100
'(agda2-fix-ghci-for-windows)
101
"Hooks for `agda2-mode'."
102
:type 'hook :group 'agda2)
104
(defcustom agda2-indentation
106
"*The kind of indentation used in `agda2-mode'."
107
:type '(choice (const :tag "Haskell" haskell)
108
(const :tag "Extended relative" eri)
109
(const :tag "None" nil))
112
(defcustom agda2-information-window-max-height
114
"*The maximum height of the information window.
115
A multiple of the frame height."
119
(defcustom agda2-fontset-name
120
(unless (or (eq window-system 'mac)
121
;; Emacs-23 uses a revamped font engine which should
122
;; make agda2-fontset-name unnecessary in most cases.
123
;; And if it turns out to be necessary, we should
124
;; probably use face-remapping-alist rather than
125
;; set-frame-font so the special font only applies to
126
;; Agda buffers, and so it applies in all frames where
127
;; Agda buffers are displayed.
128
(boundp 'face-remapping-alist))
130
"Default font to use in the selected frame when activating the Agda mode.
131
This is only used if it's non-nil and Emacs is not running in a
134
Note that this setting (if non-nil) affects non-Agda buffers as
135
well, and that you have to restart Emacs if you want settings to
136
this variable to take effect."
137
:type '(choice (string :tag "Fontset name")
138
(const :tag "Do not change the font" nil))
141
(defcustom agda2-fontset-spec-of-fontset-agda2
142
"-*-fixed-Medium-r-Normal-*-18-*-*-*-c-*-fontset-agda2,
143
ascii:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO8859-1,
144
latin-iso8859-2:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-2,
145
latin-iso8859-3:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-3,
146
latin-iso8859-4:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-4,
147
cyrillic-iso8859-5:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-5,
148
greek-iso8859-7:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-7,
149
latin-iso8859-9:-*-Fixed-*-r-*-*-18-*-*-*-c-*-iso8859-9,
150
mule-unicode-0100-24ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1,
151
mule-unicode-2500-33ff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1,
152
mule-unicode-e000-ffff:-Misc-Fixed-Medium-R-Normal--18-120-100-100-C-90-ISO10646-1,
153
japanese-jisx0208:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0208.1990-0,
154
japanese-jisx0212:-Misc-Fixed-Medium-R-Normal-ja-18-*-*-*-C-*-JISX0212.1990-0,
155
thai-tis620:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-TIS620.2529-1,
156
lao:-Misc-Fixed-Medium-R-Normal--24-240-72-72-C-120-MuleLao-1,
157
tibetan:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-160-MuleTibetan-0,
158
tibetan-1-column:-TibMdXA-fixed-medium-r-normal--16-160-72-72-m-80-MuleTibetan-1,
159
korean-ksc5601:-Daewoo-Mincho-Medium-R-Normal--16-120-100-100-C-160-KSC5601.1987-0,
160
chinese-gb2312:-ISAS-Fangsong ti-Medium-R-Normal--16-160-72-72-c-160-GB2312.1980-0,
161
chinese-cns11643-1:-HKU-Fixed-Medium-R-Normal--16-160-72-72-C-160-CNS11643.1992.1-0,
162
chinese-big5-1:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0,
163
chinese-big5-2:-ETen-Fixed-Medium-R-Normal--16-150-75-75-C-160-Big5.ETen-0"
164
"Specification of the \"fontset-agda2\" fontset.
165
This fontset is only created if `agda2-fontset-name' is
166
\"fontset-agda2\" and Emacs is not run in a terminal.
168
Note that the text \"fontset-agda2\" has to be part of the
169
string (in a certain way; see the default setting) in order for the
170
agda2 fontset to be created properly.
172
Note also that the default setting may not work unless suitable
173
fonts are installed on your system. Refer to the README file
174
accompanying the Agda distribution for more details.
176
Note finally that you have to restart Emacs if you want settings
177
to this variable to take effect."
181
(if (and (equal agda2-fontset-name "fontset-agda2") window-system)
182
(create-fontset-from-fontset-spec agda2-fontset-spec-of-fontset-agda2 t t))
184
(defun agda2-fix-ghci-for-windows ()
185
(if (string-match "windows" system-configuration)
186
(setq haskell-ghci-program-name "ghc"
187
haskell-ghci-program-args '("--interactive"))))
189
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
190
;;;; Global and buffer-local vars, initialization
192
(defvar agda2-mode-syntax-table
193
(let ((tbl (make-syntax-table)))
194
;; Set the syntax of every char to "w" except for those whose default
195
;; syntax in `standard-syntax-table' is `paren' or `whitespace'.
196
(map-char-table (lambda (keys val)
197
;; `keys' here can be a normal char, a generic char
198
;; (Emacs<23), or a char range (Emacs>=23).
199
(unless (memq (car val)
202
(list (string-to-syntax "(")
203
(string-to-syntax ")")
204
(string-to-syntax " ")))))
205
(modify-syntax-entry keys "w" tbl)))
206
(standard-syntax-table))
207
;; Then override the remaining special cases.
208
(dolist (cs '((?{ . "(}1n") (?} . "){4n") (?- . "w 123b") (?\n . "> b")
209
(?. . ".") (?\; . ".") (?_ . ".") (?! . ".")))
210
(modify-syntax-entry (car cs) (cdr cs) tbl))
212
"Syntax table used by the Agda mode:
214
{} | Comment characters, matching parentheses.
215
- | Comment character, word constituent.
219
Remaining characters inherit their syntax classes from the
220
standard syntax table if that table treats them as matching
221
parentheses or whitespace. Otherwise they are treated as word
224
(defconst agda2-command-table
226
(agda2-load "\C-c\C-l" (global) "Load")
227
(agda2-load "\C-c\C-x\C-l")
228
(agda2-compile "\C-c\C-x\C-c" (global) "Compile")
229
(agda2-text-state "\C-c\C-x\C-d" (global) "Deactivate Agda")
230
(agda2-quit "\C-c\C-x\C-q" (global) "Quit")
231
(agda2-restart "\C-c\C-x\C-r" (global) "Restart")
232
(agda2-display-implicit-arguments "\C-c\C-x\C-h" (global) "Toggle display of hidden arguments")
233
(agda2-highlight-reload-or-clear "\C-c\C-x\C-s" (global) "Reload syntax highlighting information")
234
(agda2-show-constraints ,(kbd "C-c C-=") (global) "Show constraints")
235
(agda2-solveAll ,(kbd "C-c C-s") (global) "Solve constraints")
236
(agda2-show-goals ,(kbd "C-c C-?") (global) "Show goals")
237
(agda2-next-goal "\C-c\C-f" (global) "Next goal") ; Forward.
238
(agda2-previous-goal "\C-c\C-b" (global) "Previous goal") ; Back.
239
(agda2-give ,(kbd "C-c C-SPC") (local) "Give")
240
(agda2-refine "\C-c\C-r" (local) "Refine")
241
(agda2-make-case "\C-c\C-c" (local) "Case")
242
(agda2-goal-type "\C-c\C-t" (local) "Goal type")
243
(agda2-show-context "\C-c\C-e" (local) "Context (environment)")
244
(agda2-infer-type-maybe-toplevel "\C-c\C-d" (local global) "Infer (deduce) type")
245
(agda2-goal-and-context ,(kbd "C-c C-,") (local) "Goal type and context")
246
(agda2-goal-and-context-and-inferred ,(kbd "C-c C-.") (local) "Goal type, context and inferred type")
247
(agda2-compute-normalised-maybe-toplevel "\C-c\C-n" (local global) "Evaluate term to normal form")
248
(agda2-indent ,(kbd "TAB"))
249
(agda2-indent-reverse [S-iso-lefttab])
250
(agda2-indent-reverse [S-lefttab])
251
(agda2-indent-reverse [S-tab])
252
(agda2-goto-definition-mouse [mouse-2])
253
(agda2-goto-definition-keyboard "\M-.")
254
(agda2-go-back "\M-*")
256
"Table of commands, used to build keymaps and menus.
257
Each element has the form (CMD &optional KEYS WHERE DESC) where
258
CMD is a command; KEYS is its key binding (if any); WHERE is a
259
list which should contain 'local if the command should exist in
260
the goal menu and 'global if the command should exist in the main
261
menu; and DESC is the description of the command used in the
264
(defvar agda2-mode-map
265
(let ((map (make-sparse-keymap "Agda mode")))
266
(define-key map [menu-bar Agda]
267
(cons "Agda" (make-sparse-keymap "Agda")))
268
(define-key map [down-mouse-3] 'agda2-popup-menu-3)
269
(dolist (d (reverse agda2-command-table))
270
(destructuring-bind (f &optional keys kinds desc) d
271
(if keys (define-key map keys f))
272
(if (member 'global kinds)
274
(vector 'menu-bar 'Agda (intern desc)) (cons desc f)))))
276
"Keymap for `agda2-mode'.")
278
(defvar agda2-goal-map
279
(let ((map (make-sparse-keymap "Agda goal")))
280
(dolist (d (reverse agda2-command-table))
281
(destructuring-bind (f &optional keys kinds desc) d
282
(if (member 'local kinds)
284
(vector (intern desc)) (cons desc f)))))
286
"Keymap for agda2 goal menu.")
288
(defvar agda2-buffer nil "Agda subprocess buffer. Set in `agda2-restart'.")
289
(defvar agda2-process nil "Agda subprocess. Set in `agda2-restart'.")
291
;; Some buffer locals
292
(defvar agda2-buffer-external-status ""
293
"External status of an `agda2-mode' buffer (dictated by the Haskell side).")
294
(make-variable-buffer-local 'agda2-buffer-external-status)
296
(defconst agda2-help-address
298
"Address accepting submissions of bug reports and questions.")
300
;; Annotation for a goal
302
;; ---------- overlay: agda2-gn num, face highlight, after-string num,
303
;; modification-hooks (agda2-protect-goal-markers)
304
;; - text-props: category agda2-delim1
305
;; - text-props: category agda2-delim2
306
;; - text-props: category agda2-delim3
307
;; - text-props: category agda2-delim4
309
;; Char categories for {! ... !}
310
(defvar agda2-open-brace "{")
311
(defvar agda2-close-brace " }")
312
(setplist 'agda2-delim1 `(display ,agda2-open-brace))
313
(setplist 'agda2-delim2 `(display ,agda2-open-brace rear-nonsticky t
315
(setplist 'agda2-delim3 `(display ,agda2-close-brace agda2-delim3 t))
316
(setplist 'agda2-delim4 `(display ,agda2-close-brace rear-nonsticky t))
318
;; Note that strings used with the display property are compared by
319
;; reference. If the agda2-*-brace definitions were inlined, then
320
;; goals would be displayed as "{{ }}n" instead of "{ }n".
322
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
326
(add-to-list 'auto-mode-alist '("\\.l?agda\\'" . agda2-mode))
328
(modify-coding-system-alist 'file "\\.l?agda\\'" 'utf-8)
330
(define-derived-mode agda2-mode nil "Agda"
331
"Major mode for agda files.
333
Note that when this mode is activated the default font of the
334
current frame is changed to the fontset `agda2-fontset-name'.
335
The reason is that Agda programs often use mathematical symbols
336
and other Unicode characters, so we try to provide a suitable
337
default font setting, which can display many of the characters
338
encountered. If you prefer to use your own settings, set
339
`agda2-fontset-name' to nil.
343
(setq local-abbrev-table agda2-mode-abbrev-table
346
'((:eval (unless (eq 0 (length agda2-buffer-external-status))
347
(concat ":" agda2-buffer-external-status)))))
348
(let ((l '(max-specpdl-size 2600
349
max-lisp-eval-depth 2800)))
350
(while l (set (make-local-variable (pop l)) (pop l))))
351
(if (and window-system agda2-fontset-name)
353
(set-frame-font agda2-fontset-name)
354
(error (error "Unable to change the font; change agda2-fontset-name or tweak agda2-fontset-spec-of-fontset-agda2"))))
356
(agda2-highlight-setup)
357
(agda2-highlight-reload)
358
(agda2-comments-and-paragraphs-setup)
359
(force-mode-line-update)
360
;; Protect global value of default-input-method from set-input-method.
361
(make-local-variable 'default-input-method)
362
(set-input-method "Agda"))
364
(defun agda2-restart ()
365
"Kill and restart the *ghci* buffer and load `agda2-toplevel-module'."
367
(save-excursion (let ((agda2-bufname "*ghci*")
368
(ignore-dot-ghci "-ignore-dot-ghci"))
369
(agda2-protect (kill-buffer agda2-bufname))
370
;; Make sure that the user's .ghci is not read.
371
;; Users can override this by adding
372
;; "-read-dot-ghci" to
373
;; `haskell-ghci-program-args'.
374
(unless (equal (car-safe haskell-ghci-program-args)
376
(set (make-local-variable 'haskell-ghci-program-args)
377
(cons ignore-dot-ghci haskell-ghci-program-args)))
378
(haskell-ghci-start-process nil)
379
(setq agda2-process haskell-ghci-process
380
agda2-buffer haskell-ghci-process-buffer
381
mode-name "Agda GHCi")
382
(set (make-local-variable 'comint-input-sender)
384
(set-buffer-file-coding-system 'utf-8)
385
(set-buffer-process-coding-system 'utf-8 'utf-8)
386
(rename-buffer agda2-bufname)))
387
(apply 'agda2-go nil ":set" agda2-ghci-options)
388
(agda2-go nil ":mod +" agda2-toplevel-module)
391
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
392
;;;; Communicating with Agda
394
(defun agda2-raise-ghci-error ()
396
The error message directs the user to the *ghci* buffer."
397
(error "Problem encountered. The *ghci* buffer can perhaps explain why."))
399
(defun agda2-send (proc s)
400
"Sends the string S to PROC.
401
Splits up S into small chunks and sends them one after the other,
402
because when GHCi is used in shell buffers it chokes on overly
403
long strings (some versions of GHCi, on some systems)."
404
(let* ((chunk-size 200))
405
(dolist (chunk (agda2-chunkify chunk-size s))
406
(comint-send-string proc chunk)))
407
(comint-send-string proc "\n"))
409
(defun agda2-go (require-response &rest args)
410
"Executes commands in GHCi.
411
Sends the list of strings ARGS to GHCi, waits for output and
412
executes the responses, if any. If REQUIRE-RESPONSE is non-nil
413
then an error is raised if no responses are received."
415
(unless (eq 'run (agda2-process-status))
416
;; Try restarting automatically, but only once, in case there is
417
;; some major problem.
419
(unless (eq 'run (agda2-process-status))
420
(agda2-raise-ghci-error)))
422
(haskell-ghci-go (apply 'concat (agda2-intersperse " " args)) nil))
424
(with-current-buffer haskell-ghci-process-buffer
425
(haskell-ghci-wait-for-output)
426
(let ((tempfile (make-temp-file "agda2-mode")))
428
(let ((coding-system-for-read 'utf-8)
429
(coding-system-for-write 'utf-8))
430
(comint-write-output tempfile)
432
(insert-file-contents tempfile)
433
(setq response (buffer-substring-no-properties
434
(point-min) (point-max)))))
435
(delete-file tempfile))))
436
(when (and (>= 0 (agda2-respond response))
438
(agda2-raise-ghci-error))))
440
(defun agda2-goal-cmd (require-response cmd &optional want ask &rest args)
441
"When in a goal, send CMD, goal num and range, and strings ARGS to agda2.
442
WANT is an optional prompt. When ASK is non-nil, use minibuffer.
443
If REQUIRE-RESPONSE is non-nil then an error is raised if no
444
responses are received."
445
(multiple-value-bind (o g) (agda2-goal-at (point))
446
(unless g (error "For this command, please place the cursor in a goal"))
447
(let ((txt (buffer-substring-no-properties (+ (overlay-start o) 2)
448
(- (overlay-end o) 2))))
449
(if (not want) (setq txt "")
450
(when (or ask (string-match "\\`\\s *\\'" txt))
451
(setq txt (read-string (concat want ": ") txt))))
452
(apply 'agda2-go require-response cmd
455
(agda2-string-quote txt) args))))
457
;; Note that the following function is a security risk, since it
458
;; evaluates code without first inspecting it. The code (supposedly)
459
;; comes from the Agda backend, but there could be bugs in the backend
460
;; which can be exploited by an attacker which manages to trick
461
;; someone into type-checking compromised Agda code.
463
(defun agda2-respond (response)
464
"Interprets response strings.
465
For every occurrence of 'agda2_mode_code<sexp>' in RESPONSE the
466
sexp is executed. The number of executed responses is returned."
467
(let ((no-responses 0))
468
(while (string-match "agda2_mode_code" response)
470
(setq response (substring response (match-end 0)))
471
(let ((inhibit-read-only t))
472
(eval (read response))))
475
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
476
;;;; User commands and response processing
479
"Load current buffer."
481
(agda2-go t "cmd_load"
482
(agda2-string-quote (buffer-file-name))
483
(agda2-list-quote agda2-include-dirs)
486
(defun agda2-compile ()
487
"Compile the current module."
489
(agda2-go t "cmd_compile"
490
(agda2-string-quote (buffer-file-name))
491
(agda2-list-quote agda2-include-dirs)
494
(defun agda2-load-action (gs)
495
"Annotate new goals GS in current buffer."
499
"Give to the goal at point the expression in it" (interactive)
500
(agda2-goal-cmd t "cmd_give" "expression to give"))
502
(defun agda2-give-action (old-g paren)
503
"Update the goal OLD-G with the expression in it."
504
(agda2-update old-g paren))
506
(defun agda2-refine ()
507
"Refine the goal at point by the expression in it." (interactive)
508
(agda2-goal-cmd t "cmd_refine" "expression to refine"))
510
(defun agda2-make-case ()
511
"Refine the pattern var given in the goal.
512
Assumes that <clause> = {!<var>!} is on one line."
514
(agda2-goal-cmd t "cmd_make_case" "partten var to case"))
516
(defun agda2-make-case-action (newcls)
517
"Replace the line at point with new clauses NEWCLS and reload."
518
(agda2-forget-all-goals);; we reload later anyway.
520
;; (p1 (goto-char (agda2-decl-beginning)))
521
(p1 (goto-char (+ (current-indentation) (line-beginning-position))))
522
(indent (current-column))
525
(re-search-forward "!}" (line-end-position) 'noerr)
526
(delete-region p1 (point))
527
(while (setq cl (pop newcls))
529
(if newcls (insert "\n" (make-string indent ? ))))
533
(defun agda2-status-action (status)
534
"Display the string STATUS in the current buffer's mode line.
535
\(precondition: the current buffer has to use the Agda mode as the
537
(setq agda2-buffer-external-status status))
539
(defun agda2-info-action (name text)
540
"Insert TEXT into the Agda info buffer, display it, and display NAME
541
in the buffer's mode line."
543
(with-current-buffer (get-buffer-create "*Agda information*")
546
(set-syntax-table agda2-mode-syntax-table)
547
(set-input-method "Agda")
548
(goto-char (point-min))
549
(put-text-property 0 (length name) 'face '(:weight bold) name)
550
(setq mode-line-buffer-identification name)
551
(save-selected-window
552
(pop-to-buffer (current-buffer) 'not-this-window 'norecord)
553
(fit-window-to-buffer
555
(* (frame-height) agda2-information-window-max-height))))))
557
(defun agda2-show-goals()
558
"Show all goals." (interactive)
559
(agda2-go t "cmd_metas"))
561
(defun agda2-show-constraints()
562
"Show constraints." (interactive)
563
(agda2-go t "cmd_constraints"))
565
(defun agda2-text-state ()
566
"UNDER CONSTRUCTION" (interactive)
567
(dolist (o (overlays-in (point-min) (point-max)))
569
(agda2-go nil "cmd_reset")
570
(let ((inhibit-read-only t))
571
(annotation-preserve-mod-p-and-undo
572
(set-text-properties (point-min) (point-max) '()))
573
(force-mode-line-update)))
575
(defun agda2-next-goal () "Go to the next goal, if any." (interactive)
576
(agda2-mv-goal 'next-single-property-change 'agda2-delim2 1 (point-min)))
577
(defun agda2-previous-goal () "Go to the previous goal, if any." (interactive)
578
(agda2-mv-goal 'previous-single-property-change 'agda2-delim3 0 (point-max)))
579
(defun agda2-mv-goal (change delim adjust wrapped)
581
((go (p) (while (and (setq p (funcall change p 'category))
582
(not (eq (get-text-property p 'category) delim))))
583
(if p (goto-char (+ adjust p)))))
584
(or (go (point)) (go wrapped) (message "No goals in the buffer"))))
587
"Quit and clean up after agda2." (interactive)
588
(agda2-protect (progn (kill-buffer agda2-buffer)
589
(kill-buffer (current-buffer)))))
591
(defmacro agda2-maybe-normalised (name comment cmd prompt)
592
"This macro constructs a function NAME which runs CMD.
593
COMMENT is used to build the function's comment. The function
594
NAME takes a prefix argument which tells whether it should
595
normalise types or not when running CMD (through
596
`agda2-goal-cmd' t; PROMPT, if non-nil, is used as the goal
598
(let ((eval (make-symbol "eval")))
599
`(defun ,name (&optional not-normalise)
602
With a prefix argument the result is not explicitly normalised.")
604
(let ((,eval (if not-normalise "Instantiated" "Normalised")))
605
(agda2-goal-cmd t (concat ,cmd " Agda.Interaction.BasicOps." ,eval)
608
(defmacro agda2-maybe-normalised-toplevel (name comment cmd prompt)
609
"This macro constructs a function NAME which runs CMD.
610
COMMENT is used to build the function's comments. The function
611
NAME takes a prefix argument which tells whether it should
612
normalise types or not when running CMD (through `agda2-go' t; the
613
string PROMPT is used as the goal command prompt)."
614
(let ((eval (make-symbol "eval")))
615
`(defun ,name (not-normalise expr)
618
With a prefix argument the result is not explicitly normalised.")
619
(interactive ,(concat "P\nM" prompt ": "))
620
(let ((,eval (if not-normalise "Instantiated" "Normalised")))
621
(agda2-go t (concat ,cmd " Agda.Interaction.BasicOps." ,eval " "
622
(agda2-string-quote expr)))))))
624
(agda2-maybe-normalised
626
"Show the type of the goal at point"
630
(agda2-maybe-normalised
632
"Infer the type of the goal at point"
634
"expression to type")
636
(agda2-maybe-normalised-toplevel
637
agda2-infer-type-toplevel
638
"Infers the type of the given expression. The scope used for
639
the expression is that of the last point inside the current
644
(defun agda2-infer-type-maybe-toplevel ()
645
"Infers the type of the given expression.
646
Either uses the scope of the current goal or, if point is not in a goal, the
649
(call-interactively (if (agda2-goal-at (point))
651
'agda2-infer-type-toplevel)))
653
(agda2-maybe-normalised
654
agda2-goal-and-context
655
"Shows the type of the goal at point and the currect context"
656
"cmd_goal_type_context"
659
(agda2-maybe-normalised
660
agda2-goal-and-context-and-inferred
661
"Shows the context, the goal and the given expression's inferred type"
662
"cmd_goal_type_context_infer"
663
"expression to type")
665
(agda2-maybe-normalised
667
"Show the context of the goal at point"
671
(defun agda2-solveAll ()
672
"Solves all goals that are already instantiated internally."
674
(agda2-go t "cmd_solveAll"))
676
(defun agda2-solveAll-action (iss)
679
(let* ((g (pop iss)) (txt (pop iss)))
680
(agda2-replace-goal g txt)
684
(defun agda2-compute-normalised (&optional arg)
685
"Compute the normal form of the expression in the goal at point.
686
With a prefix argument \"abstract\" is ignored during the computation."
688
(let ((cmd (concat "cmd_compute"
689
(if arg " True" " False"))))
690
(agda2-goal-cmd t cmd "expression to normalise")))
692
(defun agda2-compute-normalised-toplevel (expr &optional arg)
693
"Computes the normal form of the given expression.
694
The scope used for the expression is that of the last point inside the current
696
With a prefix argument \"abstract\" is ignored during the computation."
697
(interactive "MExpression: \nP")
698
(let ((cmd (concat "cmd_compute_toplevel"
699
(if arg " True" " False")
701
(agda2-go t (concat cmd (agda2-string-quote expr)))))
703
(defun agda2-compute-normalised-maybe-toplevel ()
704
"Computes the normal form of the given expression,
705
using the scope of the current goal or, if point is not in a goal, the
707
With a prefix argument \"abstract\" is ignored during the computation."
709
(if (agda2-goal-at (point))
710
(call-interactively 'agda2-compute-normalised)
711
(call-interactively 'agda2-compute-normalised-toplevel)))
713
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
716
(defun agda2-annotate (goals)
717
"Annotates the goals in the current buffer with text properties.
718
The goal numbers should be given by GOALS (in the order they
719
appear in the buffer)."
720
(agda2-forget-all-goals)
722
((delims() (re-search-forward "[?]\\|[{][-!]\\|[-!][}]\\|--" nil t))
723
(is-lone-questionmark ()
728
"\\(.[{(]\\|.\\s \\)[?]\\(\\s \\|[)};]\\|$\\)"))))
729
(make(p) (agda2-make-goal p (point) (pop goals)))
730
(inside-comment() (and stk (null (car stk))))
731
(inside-goal() (and stk (integerp (car stk)))))
733
(goto-char (point-min))
734
(while (and goals (delims))
735
(labels ((c (s) (equal s (match-string 0))))
737
((c "--") (when (not stk) (end-of-line)))
738
((c "{-") (when (not (inside-goal)) (push nil stk)))
739
((c "{!") (when (not (inside-comment)) (push (- (point) 2) stk)))
740
((c "-}") (when (inside-comment) (pop stk)))
741
((c "!}") (when (inside-goal)
743
(unless stk (make top))))
745
(when (and (not stk) (is-lone-questionmark))
748
(make (- (point) 4)))))))))))
750
(defun agda2-make-goal (p q n)
751
"Make a goal with number N at <P>{!...!}<Q>. Assume the region is clean."
752
(annotation-preserve-mod-p-and-undo
753
(flet ((atp (x ps) (add-text-properties x (1+ x) ps)))
754
(atp p '(category agda2-delim1))
755
(atp (1+ p) '(category agda2-delim2))
756
(atp (- q 2) '(category agda2-delim3))
757
(atp (1- q) '(category agda2-delim4)))
758
(let ((o (make-overlay p q nil t nil)))
759
(overlay-put o 'modification-hooks '(agda2-protect-goal-markers))
760
(overlay-put o 'agda2-gn n)
761
(overlay-put o 'face 'highlight)
762
(overlay-put o 'after-string (propertize (format "%s" n) 'face 'highlight)))))
764
(defun agda2-protect-goal-markers (ol action beg end &optional length)
765
"Ensures that the goal markers cannot be tampered with.
766
Except if `inhibit-read-only' is non-nil or /all/ of the goal is
769
;; This is the after-change hook.
771
;; This is the before-change hook.
773
((and (<= beg (overlay-start ol)) (>= end (overlay-end ol)))
774
;; The user is trying to remove the whole goal:
775
;; manually evaporate the overlay and add an undo-log entry so
776
;; it gets re-added if needed.
777
(when (listp buffer-undo-list)
778
(push (list 'apply 0 (overlay-start ol) (overlay-end ol)
779
'move-overlay ol (overlay-start ol) (overlay-end ol))
782
((or (< beg (+ (overlay-start ol) 2))
783
(> end (- (overlay-end ol) 2)))
784
(unless inhibit-read-only
785
(signal 'text-read-only nil))))))
787
(defun agda2-update (old-g new-txt)
788
"Update the goal OLD-G.
789
If NEW-TXT is a string, then the goal is replaced by the string,
790
and otherwise the text inside the goal is retained (parenthesised
791
if NEW-TXT is `'paren').
793
Removes the goal braces, but does not remove the goal overlay or
795
(multiple-value-bind (p q) (agda2-range-of-goal old-g)
797
(cond ((stringp new-txt)
798
(agda2-replace-goal old-g new-txt))
799
((equal new-txt 'paren)
800
(goto-char (- q 2)) (insert ")")
801
(goto-char (+ p 2)) (insert "(")))
802
(multiple-value-bind (p q) (agda2-range-of-goal old-g)
803
(delete-region (- q 2) q)
804
(delete-region p (+ p 2))))))
806
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
809
(defun agda2-process-status ()
810
"Status of `agda2-buffer', or \"no process\"."
811
(agda2-protect (process-status agda2-process) "no process"))
813
(defun agda2-intersperse (sep xs)
814
(let(ys)(while xs (push (pop xs) ys)(push sep ys))(pop ys)(nreverse ys)))
816
(defun agda2-goal-Range (o)
817
"Range of goal overlay O."
818
(format "(Range [Interval %s %s])"
819
(agda2-mkPos (+ (overlay-start o) 2))
820
(agda2-mkPos (- (overlay-end o) 2))))
822
(defun agda2-mkPos (&optional p)
823
"Position value of P or point."
826
(format "(Pn \"%s\" %d %d %d)" (buffer-file-name)
827
(point) (count-lines (point-min) (point)) (1+ (current-column)))))
829
(defun agda2-char-quote (c)
830
"Convert character C to the notation used in Haskell strings.
831
The non-ASCII characters are actually rendered as
832
\"\\xNNNN\\&\", i.e. followed by a \"null character\", to avoid
833
problems if they are followed by digits. ASCII characters (code
834
points < 128) are converted to singleton strings."
837
;; FIXME: Why return a list rather than a string? --Stef
838
(append (format "\\x%x\\&" (encode-char c 'ucs)) nil)))
840
(defun agda2-string-quote (s)
841
"Convert string S into a string representing it in Haskell syntax.
842
Escape newlines, double quotes, etc.. in the string S, add
843
surrounding double quotes, and convert non-ASCII characters to the \\xNNNN
844
notation used in Haskell strings."
845
(let ((pp-escape-newlines t))
846
(mapconcat 'agda2-char-quote (pp-to-string s) "")))
848
(defun agda2-list-quote (strings)
849
"Convert a list of STRINGS into a string representing it in Haskell syntax."
850
(concat "[" (mapconcat 'agda2-string-quote strings ", ") "]"))
852
(defun agda2-goal-at(pos)
853
"Return (goal overlay, goal number) at POS, or nil."
854
(let ((os (and pos (overlays-at pos))) o g)
855
(while (and os (not(setq g (overlay-get (setq o (pop os)) 'agda2-gn)))))
858
(defun agda2-goal-overlay (g)
859
"Returns the overlay of goal number G, if any."
862
(mapcar (lambda (o) (if (equal (overlay-get o 'agda2-gn) g) o))
863
(overlays-in (point-min) (point-max))))))
865
(defun agda2-range-of-goal (g)
866
"The range of goal G."
867
(let ((o (agda2-goal-overlay g)))
868
(if o (list (overlay-start o) (overlay-end o)))))
870
(defun agda2-goto-goal (g)
871
(let ((p (+ 2 (car (agda2-range-of-goal g)))))
872
(if p (goto-char p))))
874
(defun agda2-replace-goal (g newtxt)
875
"Replace the content of goal G with NEWTXT." (interactive)
877
(multiple-value-bind (p q) (agda2-range-of-goal g)
878
(setq p (+ p 2) q (- q 2))
879
(let ((indent (and (goto-char p) (current-column))))
880
(delete-region p q) (insert newtxt)
881
(while (re-search-backward "^" p t)
882
(insert-char ? indent) (backward-char (1+ indent)))))))
884
(defun agda2-forget-all-goals ()
885
"Remove all goal annotations.
886
\(Including some text properties which might be used by other
888
(annotation-preserve-mod-p-and-undo
889
(remove-text-properties (point-min) (point-max)
890
'(category nil agda2-delim2 nil agda2-delim3 nil
891
display nil rear-nonsticky nil)))
892
(let ((p (point-min)))
893
(while (< (setq p (next-single-char-property-change p 'agda2-gn))
895
(delete-overlay (car (agda2-goal-at p))))))
897
(defun agda2-decl-beginning ()
898
"Find the beginning point of the declaration containing the point.
899
To do: dealing with semicolon separated decls."
902
(let* ((pEnd (point))
903
(pDef (progn (goto-char (point-min))
904
(re-search-forward "\\s *" pEnd t)))
905
(cDef (current-column)))
906
(while (re-search-forward
907
"where\\(\\s +\\)\\S \\|^\\(\\s *\\)\\S " pEnd t)
909
(setq pDef (goto-char (match-end 1))
910
cDef (current-column))
911
(goto-char (match-end 2))
912
(if (>= cDef (current-column))
914
cDef (current-column))))
917
(if (equal (current-word) "mutual")
918
(or (match-end 2) (match-end 1))
921
(defun agda2-beginning-of-decl ()
923
(goto-char (agda2-decl-beginning)))
925
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
928
(defun agda2-indent ()
929
"This is what happens when TAB is pressed.
930
Depends on the setting of `agda2-indentation'."
932
(cond ((eq agda2-indentation 'haskell) (haskell-indent-cycle))
933
((eq agda2-indentation 'eri) (eri-indent))))
935
(defun agda2-indent-reverse ()
936
"This is what happens when S-TAB is pressed.
937
Depends on the setting of `agda2-indentation'."
939
(cond ((eq agda2-indentation 'eri) (eri-indent-reverse))))
941
(defun agda2-indent-setup ()
942
"Set up and start the indentation subsystem.
943
Depends on the setting of `agda2-indentation'."
945
(cond ((eq agda2-indentation 'haskell)
946
(labels ((setl (var val) (set (make-local-variable var) val)))
947
(setl 'indent-line-function 'haskell-indent-cycle)
948
(setl 'haskell-indent-off-side-keywords-re
949
"\\<\\(do\\|let\\|of\\|where\\|sig\\|struct\\)\\>[ \t]*"))
950
(local-set-key "\177" 'backward-delete-char-untabify)
951
(set (make-local-variable 'haskell-literate)
952
(if (string-match "\\.lagda$" (buffer-file-name))
954
(setq haskell-indent-mode t)
955
(run-hooks 'haskell-indent-hook))))
957
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
958
;; Comments and paragraphs
960
(defun agda2-comments-and-paragraphs-setup nil
961
"Set up comment and paragraph handling for Agda mode."
963
;; Syntax table setup for comments is done elsewhere.
965
;; Enable highlighting of comments via Font Lock mode (which uses
966
;; the syntax table).
967
(set (make-local-variable 'font-lock-defaults)
968
'(nil nil nil nil nil))
970
;; Empty lines (all white space according to Emacs) delimit
972
(set (make-local-variable 'paragraph-start) "\\s-*$")
973
(set (make-local-variable 'paragraph-separate) paragraph-start)
975
;; Support for adding/removing comments.
976
(set (make-local-variable 'comment-start) "-- ")
978
;; Support for proper filling of text in comments (requires that
979
;; Filladapt is activated).
980
(when (featurep 'filladapt)
981
(add-to-list (make-local-variable
982
'filladapt-token-table)
983
'("--" agda2-comment))
984
(add-to-list (make-local-variable 'filladapt-token-match-table)
985
'(agda2-comment agda2-comment) t)
986
(add-to-list (make-local-variable 'filladapt-token-conversion-table)
987
'(agda2-comment . exact))))
989
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
990
;; Go to definition site
992
(defun agda2-goto-definition-keyboard (&optional other-window)
993
"Go to the definition site of the name under point (if any).
994
If this function is invoked with a prefix argument then another window is used
995
to display the given position."
997
(annotation-goto-indirect (point) other-window))
999
(defun agda2-goto-definition-mouse (ev prefix)
1000
"Go to the definition site of the name clicked on, if any.
1001
Otherwise, yank (see `mouse-yank-at-click')."
1002
(interactive "e\nP")
1003
(let ((pos (posn-point (event-end ev))))
1004
(if (annotation-goto-possible pos)
1005
(annotation-goto-indirect pos)
1006
;; FIXME: Shouldn't we use something like
1007
;; (call-interactively (key-binding ev))? --Stef
1008
(mouse-yank-at-click ev prefix))))
1010
(defun agda2-go-back nil
1011
"Go back to the previous position in which
1012
`agda2-goto-definition-keyboard' or `agda2-goto-definition-mouse' was
1015
(annotation-go-back))
1017
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1018
;; Implicit arguments
1020
(defun agda2-display-implicit-arguments (&optional arg)
1021
"Toggle display of implicit arguments.
1022
With prefix argument, turn on display of implicit arguments if
1023
the argument is a positive number, otherwise turn it off."
1025
(cond ((eq arg nil) (agda2-go t "toggleImplicitArgs"))
1027
(> arg 0)) (agda2-go t "showImplicitArgs" "True"))
1028
(t (agda2-go t "showImplicitArgs" "False"))))
1030
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1033
(defun agda2-popup-menu-3 (ev)
1034
"If in a goal, popup the goal menu and call chosen command."
1038
(and (agda2-goal-at (goto-char (posn-point (event-end ev))))
1039
(setq choice (x-popup-menu ev agda2-goal-map))
1041
(lookup-key agda2-goal-map (apply 'vector choice)))))))
1043
(provide 'agda2-mode)
1044
;;; agda2-mode.el ends here
added
removed
src/data/emacs-mode/agda2-mode.el
