git.iko.soy/Idris-dev
on master help sign in
Merge pull request #579 from david-christiansen/emacs-auto
4a5831dEdwin Brady
contribs/tool-support/emacs/auto-idris.elnew file+94
compare with master
unifiedsplit
@@ -0,0 +1,94 @@
1+;;;; Elisp for talking to idris --client
2+;;;; Stopgap until these features work with --ideslave - use with https://github.com/idris-hackers/idris-mode
3+(require 'idris-mode)
4+
5+(defvar *auto-idris-output-buf* "*auto-idris-output*")
6+
7+(defun string-no-properties (str)
8+ (substring-no-properties str 0 (length str)))
9+
10+(defun call-idris-client (cmd &optional return-output)
11+ (if return-output
12+ (with-temp-buffer
13+ (call-process "idris" nil t nil "--client" cmd)
14+ (buffer-string))
15+ (call-process "idris" nil *auto-idris-output-buf* nil "--client" cmd)
16+ nil))
17+
18+(defun idris-get-line-num ()
19+ "Get the current line number"
20+ (save-restriction
21+ (widen)
22+ (save-excursion
23+ (beginning-of-line)
24+ (1+ (count-lines 1 (point))))))
25+
26+
27+(defun idris-thing-at-point ()
28+ "Return the line number and name at point"
29+ (let ((name (symbol-at-point))
30+ (line (idris-get-line-num)))
31+ (if name
32+ (cons (string-no-properties (symbol-name name)) line)
33+ (error "Nothing identifiable under point"))))
34+
35+(defun idris-load ()
36+ "Load the current buffer using Idris client mode"
37+ (interactive)
38+ (save-buffer)
39+ (let* ((file-name (buffer-file-name))
40+ (cmd (concat ":l " file-name)))
41+ (call-idris-client cmd)))
42+
43+(defun idris-type-at-point ()
44+ "Show the type of the name at point"
45+ (interactive)
46+ (message (call-idris-client (concat ":t " (car (idris-thing-at-point))) t)))
47+
48+(defun idris-add-clause ()
49+ "Add clauses to the declaration at point"
50+ (interactive)
51+ (idris-load)
52+ (let ((what (idris-thing-at-point)))
53+ (call-idris-client (concat ":ac! " (number-to-string (cdr what)) (car what))))
54+ (revert-buffer t t)
55+ (idris-load))
56+
57+(defun idris-case-split ()
58+ "Case split the pattern var at point"
59+ (interactive)
60+ (idris-load)
61+ (let ((what (idris-thing-at-point)))
62+ (call-idris-client (concat ":cs! " (number-to-string (cdr what)) " " (car what))))
63+ (revert-buffer t t)
64+ (idris-load))
65+
66+(defun idris-proof-search (&optional hints)
67+ "Invoke the proof search"
68+ (interactive "sHints: ")
69+ (let ((hints (if hints (split-string hints "[^a-zA-Z0-9']") " "))
70+ (what (idris-thing-at-point)))
71+ (call-idris-client (format ":ps! %s %s %s" (number-to-string (cdr what)) (car what) hints)))
72+ (revert-buffer t t)
73+ (idris-load))
74+
75+(defun idris-add-missing ()
76+ "Add missing cases"
77+ (interactive)
78+ (idris-load)
79+ (let ((what (idris-thing-at-point)))
80+ (call-idris-client (concat ":am! " (number-to-string (cdr what)) " " (car what))))
81+ (revert-buffer t t)
82+ (idris-load))
83+
84+;;;; Bindings to imitate Agda somewhat
85+(define-key idris-mode-map (kbd "C-c C-c") 'idris-case-split)
86+(define-key idris-mode-map (kbd "C-c C-a") 'idris-proof-search)
87+(define-key idris-mode-map (kbd "C-c C-m") 'idris-add-missing)
88+(define-key idris-mode-map (kbd "C-c C-t") 'idris-type-at-point)
89+(define-key idris-mode-map (kbd "C-c C-d") 'idris-add-clause)
90+
91+(add-hook 'idris-mode-hook
92+ (lambda () (add-hook 'after-save-hook 'idris-load t)))
93+
94+(provide 'auto-idris)