@@ -26,9 +26,11 @@
2626
2727(defun idris-thing-at-point ()
2828 "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))
3030 (line (idris-get-line-num)))
31− (cons name line)))
31+ (if name
32+ (cons (string-no-properties (symbol-name name)) line)
33+ (error "Nothing identifiable under point"))))
3234
3335(defun idris-load ()
3436 "Load the current buffer using Idris client mode"
@@ -41,7 +43,7 @@
4143(defun idris-type-at-point ()
4244 "Show the type of the name at point"
4345 (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)))
4547
4648(defun idris-add-clause ()
4749 "Add clauses to the declaration at point"
@@ -49,7 +51,8 @@
4951 (idris-load)
5052 (let ((what (idris-thing-at-point)))
5153 (call-idris-client (concat ":ac! " (number-to-string (cdr what)) (car what))))
52− (revert-buffer t t))
54+ (revert-buffer t t)
55+ (idris-load))
5356
5457(defun idris-case-split ()
5558 "Case split the pattern var at point"
@@ -57,7 +60,8 @@
5760 (idris-load)
5861 (let ((what (idris-thing-at-point)))
5962 (call-idris-client (concat ":cs! " (number-to-string (cdr what)) " " (car what))))
60− (revert-buffer t t))
63+ (revert-buffer t t)
64+ (idris-load))
6165
6266(defun idris-proof-search (&optional hints)
6367 "Invoke the proof search"
@@ -65,7 +69,8 @@
6569 (let ((hints (if hints (split-string hints "[^a-zA-Z0-9']") " "))
6670 (what (idris-thing-at-point)))
6771 (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)
73+ (idris-load))
6974
7075(defun idris-add-missing ()
7176 "Add missing cases"
@@ -73,7 +78,8 @@
7378 (idris-load)
7479 (let ((what (idris-thing-at-point)))
7580 (call-idris-client (concat ":am! " (number-to-string (cdr what)) " " (car what))))
76− (revert-buffer t t))
81+ (revert-buffer t t)
82+ (idris-load))
7783
7884;;;; Bindings to imitate Agda somewhat
7985(define-key idris-mode-map (kbd "C-c C-c") 'idris-case-split)
@@ -82,5 +88,7 @@
8288(define-key idris-mode-map (kbd "C-c C-t") 'idris-type-at-point)
8389(define-key idris-mode-map (kbd "C-c C-d") 'idris-add-clause)
8490
91+(add-hook 'idris-mode-hook
92+ (lambda () (add-hook 'after-save-hook 'idris-load t)))
8593
8694(provide 'auto-idris)