[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/idris-mode 3f529d72cd 10/10: Merge pull request #601 from
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/idris-mode 3f529d72cd 10/10: Merge pull request #601 from keram/impro-sem-high |
Date: |
Mon, 23 Jan 2023 04:59:57 -0500 (EST) |
branch: elpa/idris-mode
commit 3f529d72cd6ab809dafae82a57f7550e5a4993b6
Merge: 03e6cdfe41 cf69a2c921
Author: Jan de Muijnck-Hughes <jfdm@users.noreply.github.com>
Commit: GitHub <noreply@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")
- [nongnu] elpa/idris-mode updated (7a7a468000 -> 3f529d72cd), ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 7ba6e9b6ab 04/10: Preserve current source code buffer as current when receiving input from Idris compiler, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 3cce2336b7 01/10: Allow per buffer and project controlled semantic source highlighting, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 4cbe153905 03/10: Move definition of *-words-of-encouragement to idris-repl.el, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 3f529d72cd 10/10: Merge pull request #601 from keram/impro-sem-high,
ELPA Syncer <=
- [nongnu] elpa/idris-mode 03e6cdfe41 09/10: Merge pull request #612 from keram/code-impro5, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode d01b47c972 06/10: Apply minor documentation improvements, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 1451b8ffa3 05/10: Improve documentation in inferior-idris.el, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 5c6e255b92 07/10: Replace obsolete `interactive-p` function in idris-navigate.el and, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode cf69a2c921 02/10: Simplify and improve semantic source highlighting code by:, ELPA Syncer, 2023/01/23
- [nongnu] elpa/idris-mode 86ec653651 08/10: Improve documentation for idris-log.el, ELPA Syncer, 2023/01/23