branch: elpa/idris-mode
commit 21803ac767d9695fcb279a43d9a528428ed58737
Merge: 7285acfd85 88e08a2f10
Author: Jan de Muijnck-Hughes <[email protected]>
Commit: GitHub <[email protected]>
Merge pull request #667 from keram/syntax-high-v2
Improve syntax highlighting
---
idris-commands.el | 31 ++++++++++++++++---------------
idris-highlight-input.el | 44 +++++++++++++++++++++++---------------------
idris-settings.el | 18 +++++++++++++-----
inferior-idris.el | 1 +
4 files changed, 53 insertions(+), 41 deletions(-)
diff --git a/idris-commands.el b/idris-commands.el
index e20d74e88e..13df30eebc 100644
--- a/idris-commands.el
+++ b/idris-commands.el
@@ -214,16 +214,13 @@ A prefix argument SET-LINE forces loading but only up to
the current line."
`(:load-file ,fn ,(idris-get-line-num idris-load-to-here))
`(:load-file ,fn))
(lambda (result)
- (pcase result
- (`(:highlight-source ,hs)
- (idris-highlight-source-file hs))
- (_ (idris-make-clean)
- (idris-update-options-cache)
- (setq idris-currently-loaded-buffer (current-buffer))
- (when (member 'warnings-tree idris-warnings-printing)
- (idris-list-compiler-notes))
- (run-hooks 'idris-load-file-success-hook)
- (idris-update-loaded-region result))))
+ (idris-make-clean)
+ (idris-update-options-cache)
+ (setq idris-currently-loaded-buffer (current-buffer))
+ (when (member 'warnings-tree idris-warnings-printing)
+ (idris-list-compiler-notes))
+ (run-hooks 'idris-load-file-success-hook)
+ (idris-update-loaded-region result))
(lambda (_condition)
(when (member 'warnings-tree idris-warnings-printing)
(idris-list-compiler-notes))))))
@@ -267,16 +264,19 @@ This sets the load position to point, if there is one."
(idris-load-to (point)))
(let* ((dir-and-fn (idris-filename-to-load))
(fn (cdr dir-and-fn))
- (srcdir (car dir-and-fn)))
- (setq idris-currently-loaded-buffer nil)
+ (srcdir (car dir-and-fn))
+ (idris-semantic-source-highlighting
+ (and
idris-x-enable-semantic-source-highlighting-in-sync-file-load
+ (idris-buffer-semantic-source-highlighting))))
(idris-switch-working-directory srcdir)
+ (idris-toggle-semantic-source-highlighting)
(let ((result
(idris-eval
(if idris-load-to-here
`(:load-file ,fn ,(idris-get-line-num
idris-load-to-here))
- `(:load-file ,fn)))))
+ `(:load-file ,fn))))
+ (idris-currently-loaded-buffer (current-buffer)))
(idris-update-options-cache)
- (setq idris-currently-loaded-buffer (current-buffer))
(idris-make-clean)
(idris-update-loaded-region (car result)))))
(user-error "Cannot find file for current buffer")))
@@ -1001,7 +1001,8 @@ https://github.com/clojure-emacs/cider";
idris-rex-continuations '()
idris-process-current-working-directory nil
idris-protocol-version 0
- idris-protocol-version-minor 0))
+ idris-protocol-version-minor 0
+ idris--semantic-source-highlighting t))
(defun idris-delete-ibc (no-confirmation)
"Delete the IBC file for the current buffer.
diff --git a/idris-highlight-input.el b/idris-highlight-input.el
index bde3eac0b9..719f7506bb 100644
--- a/idris-highlight-input.el
+++ b/idris-highlight-input.el
@@ -28,6 +28,11 @@
(require 'idris-common-utils)
(require 'idris-settings)
+(defvar idris--semantic-source-highlighting t
+ "Initial state of syntax highligt when connecting to Idris process.
+
+Used to ensure we send the right value in `:enable-syntax' option.")
+
(defun idris-highlight-remove-overlays (&optional buffer)
"Remove all Idris highlighting overlays from BUFFER.
Use the current buffer if BUFFER is nil."
@@ -107,29 +112,19 @@ See Info node `(elisp)Overlay Properties' to understand
how ARGS are used."
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)))
+This is controled by value of `idris-semantic-source-highlighting' variable."
+ (unless (eq idris-semantic-source-highlighting
+ idris--semantic-source-highlighting)
+ (if idris-semantic-source-highlighting
+ (if (>=-protocol-version 2 1)
+ (idris-eval '(:enable-syntax :True))
+ (advice-remove 'idris-highlight-source-file #'ignore))
+ (if (>=-protocol-version 2 1)
+ (idris-eval '(:enable-syntax :False))
+ (advice-add 'idris-highlight-source-file :around #'ignore)))
+ (setq idris--semantic-source-highlighting
idris-semantic-source-highlighting)))
(defun idris-buffer-semantic-source-highlighting ()
"Return nil if current buffer size is larger than set limit.
@@ -143,5 +138,12 @@ Otherwise return current value of
`idris-semantic-source-highlighting'"
"Customize `idris-semantic-source-highlighting-max-buffer-size'
to enable it.")
nil))
+(defun idris-syntax-highlight-event-hook-function (event)
+ (pcase event
+ (`(:output (:ok (:highlight-source ,hs)) ,_target)
+ (idris-highlight-source-file hs)
+ t)
+ (_ nil)))
+
(provide 'idris-highlight-input)
;;; idris-highlight-input.el ends here
diff --git a/idris-settings.el b/idris-settings.el
index 11f7de7657..0ea5c1b967 100644
--- a/idris-settings.el
+++ b/idris-settings.el
@@ -65,18 +65,26 @@ Advanced users may wish to disable this."
:type 'boolean)
(defcustom idris-semantic-source-highlighting t
- "Use the Idris compiler's semantic source information to highlight Idris
code.
-If `debug', log failed highlighting to buffer `*Messages*'."
+ "Use the Idris compiler's semantic source information to highlight Idris
code."
:group 'idris
- :type '(choice (boolean :tag "Enable")
- (const :tag "Debug" debug)))
+ :type 'boolean)
-(defcustom idris-semantic-source-highlighting-max-buffer-size 32768 ;; (expt 2
15)
+(defcustom idris-semantic-source-highlighting-max-buffer-size 65536 ;; (expt 2
16)
"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-x-enable-semantic-source-highlighting-in-sync-file-load nil
+ "*Experimental*
+Enable semantic source highlighting during synchronous file loads triggered
+by Idris commands.
+
+This may improve visual feedback, but can impact responsiveness depending
+on file size and command frequency."
+ :group 'idris
+ :type 'boolean)
+
(defcustom idris-log-events nil
"If non-nil, communications between Emacs and Idris are logged.
diff --git a/inferior-idris.el b/inferior-idris.el
index efae6b1bf5..18b330a3e8 100644
--- a/inferior-idris.el
+++ b/inferior-idris.el
@@ -84,6 +84,7 @@ This is maintained to restart Idris when the arguments
change.")
(add-hook 'idris-event-hooks 'idris-log-hook-function)
(add-hook 'idris-event-hooks 'idris-warning-event-hook-function)
(add-hook 'idris-event-hooks 'idris-prover-event-hook-function)
+ (add-hook 'idris-event-hooks 'idris-syntax-highlight-event-hook-function)
(if idris-hole-show-on-load
(progn
