idris2-highlight-input.el

;;; idris2-highlight-input.el --- Compiler-driven highlighting of user input  -*- lexical-binding: t; -*-

;; Copyright (C) 2015  David Raymond Christiansen

;; Author: David Raymond Christiansen <david@davidchristiansen.dk>
;; Keywords: languages

;; This program is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation, either version 3 of the License, or
;; (at your option) any later version.

;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with this program.  If not, see <http://www.gnu.org/licenses/>.

;;; Commentary:

;; This file contains routines for highlighting user input with
;; information generated by the Idris2 elaborator.

;;; Code:

(require 'idris2-common-utils)
(require 'idris2-settings)

(defun idris2-highlight-remove-overlays (&optional buffer)
  "Remove all Idris2 highlighting overlays from BUFFER, or the current buffer if it's nil."
  (interactive)
  (with-current-buffer (or buffer (current-buffer))
    (save-restriction
      (widen)
      (dolist (overlay (overlays-in (point-min) (point-max)))
        (when (overlay-get overlay 'idris2-source-highlight)
          (delete-overlay overlay))))))

(defun idris2-highlight-column (idris2-col)
  "Compute the Emacs position offset of the Idris2 column IDRIS-COL, for highlighting.

In particular, this takes bird tracks into account in literate Idris2."
  (+ idris2-col (if (idris2-lidr-p) 1 -1)))

(defun idris2-highlight--overlay-modification-hook (&rest args)
  "Delete semantic overlays if they are changed.

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))))

(defun idris2-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."
  (when idris2-semantic-source-highlighting
    (save-restriction
      (widen)
      (if (or (> end-line start-line)
              (and (= end-line start-line)
                   (> end-col start-col)))
          (with-current-buffer buffer
            (save-excursion
              (goto-char (point-min))
              (let* ((start-pos (+ (line-beginning-position start-line)
                                   (idris2-highlight-column start-col)))
                     (end-pos (+ (line-beginning-position end-line)
                                 (idris2-highlight-column end-col)))
                     (highlight-overlay (make-overlay start-pos end-pos
                                                      (get-buffer buffer))))
                (overlay-put highlight-overlay 'idris2-source-highlight t)
                (idris2-add-overlay-properties highlight-overlay
                                               (idris2-semantic-properties highlight))
                (overlay-put highlight-overlay
                             'modification-hooks
                             '(idris2-highlight--overlay-modification-hook)))))
        (when (eq idris2-semantic-source-highlighting 'debug)
          (message "Not highlighting absurd span %s:%s-%s:%s with %s"
                   start-line start-col
                   end-line end-col
                   highlight ))))))

(provide 'idris2-highlight-input)
;;; idris2-highlight-input.el ends here