branch: elpa/idris-mode commit 3f529d72cd6ab809dafae82a57f7550e5a4993b6 Merge: 03e6cdfe41 cf69a2c921 Author: Jan de Muijnck-Hughes <j...@users.noreply.github.com> Commit: GitHub <nore...@github.com>
Merge pull request #601 from keram/impro-sem-high Improve semantic syntax highlighting --- idris-commands.el | 4 +- idris-highlight-input.el | 153 ++++++++++++++++++++++++++--------------------- idris-repl.el | 3 +- idris-settings.el | 6 ++ test/idris-tests.el | 45 ++++++++++++++ 5 files changed, 141 insertions(+), 70 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..70d9472f7e 100644 --- a/idris-highlight-input.el +++ b/idris-highlight-input.el @@ -51,78 +51,97 @@ 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) +(defun idris-highlight-input-region (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)))) + (save-excursion + (save-restriction + (widen) + (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) + (mapc #'delete-overlay existing-idris-overlays-in-range) + (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 - for h in hs - do (pcase h - (`(((:filename ,fn) - (:start ,start-line-raw ,start-col-raw) - (:end ,end-line-raw ,end-col-raw)) - ,props) - (when (string= (file-name-nondirectory fn) - (file-name-nondirectory (buffer-file-name))) - (let ((start-line (if (>=-protocol-version 2 1) - (1+ start-line-raw) - start-line-raw)) - (start-col (if (>=-protocol-version 2 1) - (1+ start-col-raw) - start-col-raw)) - (end-line (if (>=-protocol-version 2 1) - (1+ end-line-raw) - end-line-raw)) - (end-col (if (>= idris-protocol-version 1) - (1+ end-col-raw) - end-col-raw))) - (idris-highlight-input-region (current-buffer) - start-line start-col - end-line end-col - props))))))) + (pcase-dolist + (`(((:filename ,fn) + (:start ,start-line-raw ,start-col-raw) + (:end ,end-line-raw ,end-col-raw)) + ,props) + hs) + (when (string= (file-name-nondirectory fn) + (file-name-nondirectory (buffer-file-name))) + (let ((start-line (if (>=-protocol-version 2 1) + (1+ start-line-raw) + start-line-raw)) + (start-col (if (>=-protocol-version 2 1) + (1+ start-col-raw) + start-col-raw)) + (end-line (if (>=-protocol-version 2 1) + (1+ end-line-raw) + end-line-raw)) + (end-col (if (>= idris-protocol-version 1) + (1+ end-col-raw) + end-col-raw))) + (idris-highlight-input-region start-line start-col + end-line end-col + props))))) + +(defun idris-highlight-input-region-debug (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-repl.el b/idris-repl.el index 09e322a673..82337ae3dc 100644 --- a/idris-repl.el +++ b/idris-repl.el @@ -369,8 +369,7 @@ and semantic annotations PROPS." (start-col-repl (+ input-col start-col)) (end-line-repl (+ input-line end-line -1)) (end-col-repl (+ input-col end-col))) - (idris-highlight-input-region buffer - start-line-repl start-col-repl + (idris-highlight-input-region start-line-repl start-col-repl end-line-repl end-col-repl props)))))) 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-tests.el b/test/idris-tests.el index f431e9a6d0..e14944e046 100644 --- a/test/idris-tests.el +++ b/test/idris-tests.el @@ -134,6 +134,51 @@ (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* ((buffer (find-file "test-data/AddClause.idr")) + (buffer-content (buffer-substring-no-properties (point-min) (point-max)))) + (idris-run) + (dotimes (_ 5) (accept-process-output nil 0.1)) + (unwind-protect + (progn + (goto-char (point-max)) + (let ((idris-semantic-source-highlighting nil)) + (insert " ") ;; to make the buffer dirty + (idris-load-file) + (dotimes (_ 10) (accept-process-output nil 0.1)) + (should (not (idris-buffer-contains-semantic-highlighting-p)))) + + (let ((idris-semantic-source-highlighting t)) + (insert " ") ;; to make the buffer dirty + (idris-load-file) + (dotimes (_ 30) (accept-process-output nil 0.1)) + (should (idris-buffer-contains-semantic-highlighting-p)) + ;;cleanup + (mapc 'delete-overlay (overlays-in (point-min) (point-max)))) + + (let ((idris-semantic-source-highlighting t) + (idris-semantic-source-highlighting-max-buffer-size 8)) + (insert " ") ;; to make the buffer dirty + (idris-load-file) + (dotimes (_ 10) (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))))))) + + ;; Cleanup (Tear down) + (dotimes (_ 5) (accept-process-output nil 0.1)) + (idris-delete-ibc t) + (erase-buffer) + (insert buffer-content) + (save-buffer) + (kill-buffer))) + (idris-quit)) + (load "idris-commands-test") (load "idris-navigate-test") (load "idris-repl-test")