@@ -1,94 +0,0 @@
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)