@@ -26,9 +26,11 @@
27(defun idris-thing-at-point ()
27(defun idris-thing-at-point ()
28 "Return the line number and name at point"
28 "Return the line number and name at point"
29− (let ((name (string-no-properties (symbol-name (symbol-at-point))))
29+ (let ((name (symbol-at-point))
30 (line (idris-get-line-num)))
30 (line (idris-get-line-num)))
31− (cons name line)))
32+ (cons (string-no-properties (symbol-name name)) line)
33+ (error "Nothing identifiable under point"))))
33(defun idris-load ()
35(defun idris-load ()
34 "Load the current buffer using Idris client mode"
36 "Load the current buffer using Idris client mode"
@@ -41,7 +43,7 @@
41(defun idris-type-at-point ()
43(defun idris-type-at-point ()
42 "Show the type of the name at point"
44 "Show the type of the name at point"
43 (interactive)
45 (interactive)
44− (message (call-idris-client (concat ":t " (string-no-properties (symbol-name (symbol-at-point)))) t)))
46+ (message (call-idris-client (concat ":t " (car (idris-thing-at-point))) t)))
46(defun idris-add-clause ()
48(defun idris-add-clause ()
47 "Add clauses to the declaration at point"
49 "Add clauses to the declaration at point"
@@ -49,7 +51,8 @@
49 (idris-load)
51 (idris-load)
50 (let ((what (idris-thing-at-point)))
52 (let ((what (idris-thing-at-point)))
51 (call-idris-client (concat ":ac! " (number-to-string (cdr what)) (car what))))
53 (call-idris-client (concat ":ac! " (number-to-string (cdr what)) (car what))))
52− (revert-buffer t t))
54+ (revert-buffer t t)
54(defun idris-case-split ()
57(defun idris-case-split ()
55 "Case split the pattern var at point"
58 "Case split the pattern var at point"
@@ -57,7 +60,8 @@
57 (idris-load)
60 (idris-load)
58 (let ((what (idris-thing-at-point)))
61 (let ((what (idris-thing-at-point)))
59 (call-idris-client (concat ":cs! " (number-to-string (cdr what)) " " (car what))))
62 (call-idris-client (concat ":cs! " (number-to-string (cdr what)) " " (car what))))
60− (revert-buffer t t))
63+ (revert-buffer t t)
62(defun idris-proof-search (&optional hints)
66(defun idris-proof-search (&optional hints)
63 "Invoke the proof search"
67 "Invoke the proof search"
@@ -65,7 +69,8 @@
65 (let ((hints (if hints (split-string hints "[^a-zA-Z0-9']") " "))
69 (let ((hints (if hints (split-string hints "[^a-zA-Z0-9']") " "))
66 (what (idris-thing-at-point)))
70 (what (idris-thing-at-point)))
67 (call-idris-client (format ":ps! %s %s %s" (number-to-string (cdr what)) (car what) hints)))
71 (call-idris-client (format ":ps! %s %s %s" (number-to-string (cdr what)) (car what) hints)))
68− (revert-buffer t t))
72+ (revert-buffer t t)
70(defun idris-add-missing ()
75(defun idris-add-missing ()
71 "Add missing cases"
76 "Add missing cases"
@@ -73,7 +78,8 @@
73 (idris-load)
78 (idris-load)
74 (let ((what (idris-thing-at-point)))
79 (let ((what (idris-thing-at-point)))
75 (call-idris-client (concat ":am! " (number-to-string (cdr what)) " " (car what))))
80 (call-idris-client (concat ":am! " (number-to-string (cdr what)) " " (car what))))
76− (revert-buffer t t))
81+ (revert-buffer t t)
78;;;; Bindings to imitate Agda somewhat
84;;;; Bindings to imitate Agda somewhat
79(define-key idris-mode-map (kbd "C-c C-c") 'idris-case-split)
85(define-key idris-mode-map (kbd "C-c C-c") 'idris-case-split)
@@ -82,5 +88,7 @@
82(define-key idris-mode-map (kbd "C-c C-t") 'idris-type-at-point)
88(define-key idris-mode-map (kbd "C-c C-t") 'idris-type-at-point)
83(define-key idris-mode-map (kbd "C-c C-d") 'idris-add-clause)
89(define-key idris-mode-map (kbd "C-c C-d") 'idris-add-clause)
91+(add-hook 'idris-mode-hook
92+ (lambda () (add-hook 'after-save-hook 'idris-load t)))
86(provide 'auto-idris)
94(provide 'auto-idris)