branch: elpa/idris-mode
commit 3cce2336b75b6191a1fcdae08c2f1a9d337ab0f1
Author: Marek L <[email protected]>
Commit: Marek L <[email protected]>
Allow per buffer and project controlled semantic source highlighting
---
idris-commands.el | 4 +-
idris-highlight-input.el | 108 +++++++++++++++++++++++++++++------------------
idris-settings.el | 6 +++
test/idris-test-utils.el | 16 +++++++
test/idris-tests.el | 32 ++++++++++++++
5 files changed, 124 insertions(+), 42 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index 07b78d9014..6c72fa5ef6 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -203,10 +203,12 @@ A prefix argument SET-LINE forces loading but only up to
the current line."
;; Actually do the loading
(let* ((dir-and-fn (idris-filename-to-load))
(fn (cdr dir-and-fn))
- (srcdir (car dir-and-fn)))
+ (srcdir (car dir-and-fn))
+ (idris-semantic-source-highlighting
(idris-buffer-semantic-source-highlighting)))
(setq idris-currently-loaded-buffer nil)
(idris-switch-working-directory srcdir)
(idris-delete-ibc t) ;; delete the ibc to avoid interfering with
partial loads
+ (idris-toggle-semantic-source-highlighting)
(idris-eval-async
(if idris-load-to-here
`(:load-file ,fn ,(idris-get-line-num idris-load-to-here))
diff --git a/idris-highlight-input.el b/idris-highlight-input.el
index ec9aaaab67..1f43723443 100644
--- a/idris-highlight-input.el
+++ b/idris-highlight-input.el
@@ -51,51 +51,41 @@ In particular, this takes bird tracks into account in
literate Idris."
See Info node `(elisp)Overlay Properties' to understand how ARGS are used."
;; There are 5 args when it's called post-modification
(when (= (length args) 5)
- (let ((overlay (car args)))
- (delete-overlay overlay))))
+ (delete-overlay (car args))))
(defun idris-highlight-input-region (buffer start-line start-col end-line
end-col highlight)
"Highlight in BUFFER using an overlay from START-LINE and START-COL to
END-LINE and END-COL and the semantic properties specified in HIGHLIGHT."
- (if (or (> end-line start-line)
- (and (= end-line start-line)
- (> end-col start-col)))
- (when idris-semantic-source-highlighting
- (with-current-buffer buffer
- (save-restriction
- (widen)
- (save-excursion
- (goto-char (point-min))
- (let* ((start-pos (+ (line-beginning-position start-line)
- (idris-highlight-column start-col)))
- (end-pos (+ (line-beginning-position end-line)
- (idris-highlight-column end-col)))
- (existing-idris-overlays-in-range (seq-filter
- (lambda (overlay)
- (overlay-get overlay
'idris-source-highlight))
- (overlays-in start-pos
end-pos)))
- (existing-idris-overlay (seq-find (lambda (overlay)
- (and
- (eql start-pos
(overlay-start overlay))
- (eql end-pos
(overlay-end overlay))
- ;; TODO: overlay
properties match
- ))
-
existing-idris-overlays-in-range)))
- (when (null existing-idris-overlay)
- (dolist (old-overlay existing-idris-overlays-in-range)
- (delete-overlay old-overlay))
- (let ((highlight-overlay (make-overlay start-pos end-pos)))
- (overlay-put highlight-overlay 'idris-source-highlight t)
- (idris-add-overlay-properties highlight-overlay
- (idris-semantic-properties
highlight))
- (overlay-put highlight-overlay
- 'modification-hooks
-
'(idris-highlight--overlay-modification-hook)))))))))
- (when (eq idris-semantic-source-highlighting 'debug)
- (message "Not highlighting absurd span %s:%s-%s:%s with %s"
- start-line start-col
- end-line end-col
- highlight))))
+ (with-current-buffer buffer
+ (save-restriction
+ (widen)
+ (save-excursion
+ (goto-char (point-min))
+ (let* ((start-pos (+ (line-beginning-position start-line)
+ (idris-highlight-column start-col)))
+ (end-pos (+ (line-beginning-position end-line)
+ (idris-highlight-column end-col)))
+ (existing-idris-overlays-in-range (seq-filter
+ (lambda (overlay)
+ (overlay-get overlay
'idris-source-highlight))
+ (overlays-in start-pos
end-pos)))
+ (existing-idris-overlay (seq-find (lambda (overlay)
+ (and
+ (eql start-pos
(overlay-start overlay))
+ (eql end-pos (overlay-end
overlay))
+ ;; TODO: overlay
properties match
+ ))
+
existing-idris-overlays-in-range)))
+ (when (null existing-idris-overlay)
+ (dolist (old-overlay existing-idris-overlays-in-range)
+ (delete-overlay old-overlay))
+ (let ((highlight-overlay (make-overlay start-pos end-pos)))
+ (overlay-put highlight-overlay 'idris-source-highlight t)
+ (idris-add-overlay-properties highlight-overlay
+ (idris-semantic-properties
highlight))
+ (overlay-put highlight-overlay
+ 'modification-hooks
+
'(idris-highlight--overlay-modification-hook)))))))))
(defun idris-highlight-source-file (hs)
(cl-loop
@@ -124,5 +114,41 @@ See Info node `(elisp)Overlay Properties' to understand
how ARGS are used."
end-line end-col
props)))))))
+(defun idris-highlight-input-region-debug (_buffer start-line start-col
end-line end-col highlight)
+ (when (not (or (> end-line start-line)
+ (and (= end-line start-line)
+ (> end-col start-col))))
+ (message "Not highlighting absurd span %s:%s-%s:%s with %s"
+ start-line start-col
+ end-line end-col
+ highlight)))
+
+(defun idris-toggle-semantic-source-highlighting ()
+ "Turn on/off semantic highlighting.
+This is controled by value of`idris-semantic-source-highlighting' variable.
+When the value is 'debug additional checks are performed on received data."
+ (if idris-semantic-source-highlighting
+ (progn
+ (if (eq idris-semantic-source-highlighting 'debug)
+ (advice-add 'idris-highlight-input-region
+ :before-until
+ #'idris-highlight-input-region-debug)
+ (advice-remove 'idris-highlight-input-region
+ #'idris-highlight-input-region-debug))
+ (advice-remove 'idris-highlight-source-file #'ignore))
+ (advice-add 'idris-highlight-source-file :around #'ignore)))
+
+(defun idris-buffer-semantic-source-highlighting ()
+ "Return nil if current buffer size is larger than set limit.
+The limit is defined as value of:
+`idris-semantic-source-highlighting-max-buffer-size'.
+Otherwise return current value of `idris-semantic-source-highlighting'"
+ (if (< (buffer-size)
+ idris-semantic-source-highlighting-max-buffer-size)
+ idris-semantic-source-highlighting
+ (message "Semantic source highlighting is disabled for the current buffer.
%s"
+ "Customize `idris-semantic-source-highlighting-max-buffer-size'
to enable it.")
+ nil))
+
(provide 'idris-highlight-input)
;;; idris-highlight-input.el ends here
diff --git a/idris-settings.el b/idris-settings.el
index bf9a3f38f2..34176677f8 100644
--- a/idris-settings.el
+++ b/idris-settings.el
@@ -71,6 +71,12 @@ If `debug', log failed highlighting to buffer `*Messages*'."
:type '(choice (boolean :tag "Enable")
(const :tag "Debug" debug)))
+(defcustom idris-semantic-source-highlighting-max-buffer-size 32768 ;; (expt 2
15)
+ "Disable semantic source highlighting if the buffer exceeds the allotted
size.
+This is to reduce lag when loading large Idris files."
+ :group 'idris
+ :type 'integer)
+
(defcustom idris-log-events nil
"If non-nil, communications between Emacs and Idris are logged.
diff --git a/test/idris-test-utils.el b/test/idris-test-utils.el
index 4c3d8fc19b..ebf411bb70 100644
--- a/test/idris-test-utils.el
+++ b/test/idris-test-utils.el
@@ -133,5 +133,21 @@ BODY is code to be executed within the temp buffer. Point
is
,@body)
(sit-for 0.1)))
+;; Based on
https://www.gnu.org/software/emacs/manual/html_node/ert/Fixtures-and-Test-Suites.html
+(defun with-idris-file-fixture (relative-filepath body)
+ (save-window-excursion
+ (let* ((buffer (find-file relative-filepath))
+ (buffer-content (buffer-substring-no-properties (point-min)
(point-max))))
+ (unwind-protect
+ (progn (goto-char (point-min))
+ (funcall body))
+
+ ;; Cleanup (Tear down)
+ (idris-delete-ibc t)
+ (erase-buffer)
+ (insert buffer-content)
+ (save-buffer)
+ (kill-buffer)))))
+
(provide 'idris-test-utils)
;;; idris-test-utils.el ends here
diff --git a/test/idris-tests.el b/test/idris-tests.el
index f431e9a6d0..154b3239fc 100644
--- a/test/idris-tests.el
+++ b/test/idris-tests.el
@@ -134,6 +134,38 @@
(idris-delete-ibc t)
(kill-buffer))))
+(defun idris-buffer-contains-semantic-highlighting-p ()
+ (seq-find (lambda (overlay) (overlay-get overlay 'idris-source-highlight))
+ (overlays-in (point-min) (point-max))))
+
+(ert-deftest idris-semantic-highlighthing ()
+ (let ((idris-semantic-source-highlighting nil))
+ (with-idris-file-fixture
+ "test-data/AddClause.idr"
+ (lambda ()
+ (idris-load-file)
+ (dotimes (_ 5) (accept-process-output nil 0.1))
+ (should (not (idris-buffer-contains-semantic-highlighting-p))))))
+ (let ((idris-semantic-source-highlighting t))
+ (with-idris-file-fixture
+ "test-data/AddClause.idr"
+ (lambda ()
+ (idris-load-file)
+ (dotimes (_ 5) (accept-process-output nil 0.1))
+ (should (idris-buffer-contains-semantic-highlighting-p)))))
+ (let ((idris-semantic-source-highlighting t)
+ (idris-semantic-source-highlighting-max-buffer-size 8))
+ (with-idris-file-fixture
+ "test-data/AddClause.idr"
+ (lambda ()
+ (idris-load-file)
+ (dotimes (_ 5) (accept-process-output nil 0.1))
+ (should (not (idris-buffer-contains-semantic-highlighting-p)))
+ (with-current-buffer "*Messages*"
+ (should (string-match-p "Semantic source highlighting is disabled for
the current buffer."
+ (buffer-substring-no-properties (point-min)
(point-max))))))))
+ (idris-quit))
+
(load "idris-commands-test")
(load "idris-navigate-test")
(load "idris-repl-test")
