From 52b7c9b307a6476052a0d98ea145a02c5081f71e Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 9 Jul 2024 16:13:22 +0200 Subject: [PATCH] Fix #781 PG does not position to error. We cannot use the " ^^^ " thing to compute the error location because commands are not stripped of newlines anymoire (#774). Solution: use the character position information with the following subtleties - position are given by coq **bytes** positions. - position given by coq is the position from the previous "." fed to coq. I.e. we must be careful to strip any blank after the final "." of a command. --- coq/coq.el | 66 +++++++++++++++++------------------------- generic/proof-shell.el | 12 ++++++-- 2 files changed, 37 insertions(+), 41 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 9d23dafca..6e528f487 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2957,7 +2957,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." "Last error from `coq-get-last-error-location' and `coq-highlight-error'.") (defvar coq--error-location-regexp - "^Toplevel input[^:]+:\n> \\(.*\\)\n> \\([^^]*\\)\\(\\^+\\)\n" + "^Toplevel input, characters \\(?1:[0-9]+\\)-\\(?2:[0-9]+\\):\n" "A regexp to search the header of coq error locations.") ;; I don't use proof-shell-last-output here since it is not always set to the @@ -2985,43 +2985,27 @@ buffer." (if (not parseresp) last-coq-error-location ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer ;; then highlight the corresponding error location - (proof-with-current-buffer-if-exists proof-response-buffer - (goto-char (point-max)) ;\nToplevel input, character[^:]:\n - (when (re-search-backward coq--error-location-regexp nil t) - (let ((text (match-string 1)) - (pos (length (match-string 2))) - (len (length (match-string 3)))) - ;; clean the response buffer from ultra-ugly underlined command line - ;; parsed above. Don't kill the first \n - (let ((inhibit-read-only t)) - (when clean (delete-region (match-beginning 0) (match-end 0)))) - (when proof-shell-unicode ;; TODO: remove this (when...) when coq-8.3 is out. - ;; `pos' and `len' are actually specified in bytes, apparently. So - ;; let's convert them, assuming the encoding used is utf-8. - ;; Presumably in Emacs-23 we could use `string-bytes' for that - ;; since the internal encoding happens to use utf-8 as well. - ;; Actually in coq-8.3 one utf8 char = one space so we do not need - ;; this at all - (let ((bytes text)) ;(encode-coding-string text 'utf-8-unix) - ;; Check that pos&len make sense in `bytes', if not give up. - (when (>= (length bytes) (+ pos len)) - ;; We assume here that `text' is a single line and use \n as - ;; a marker so we can find it back after decoding. - (setq bytes (concat (substring bytes 0 pos) - "\n" (substring bytes pos (+ pos len)))) - (let ((chars (decode-coding-string bytes 'utf-8-unix))) - (setq pos (string-match "\n" chars)) - (setq len (- (length chars) pos 1)))))) - (setq last-coq-error-location (list pos len))))))) - + (let* ((reg coq--error-location-regexp) + (msg proof-shell-last-response-output)) + (if (not (string-match reg msg)) + (setq last-coq-error-location (list 0 0)) + (let ((pos (string-to-number (match-string 1 msg))) + (end (string-to-number (match-string 2 msg)))) + (setq last-coq-error-location (list pos (- end pos)))))))) + +(defun point-add-bytes (nbytes) + "Return current point shifted by NBYTES bytes." + (byte-to-position (+ (position-bytes (point)) nbytes))) (defun coq-highlight-error (&optional parseresp clean) - "Parse the last Coq output looking at an error message. + "Return position and length of error in last message. + Highlight the text pointed by it. Coq error message must be like this: \" -> command with an error here ... +Toplevel input, characters 60-66: +> ... > ^^^^ \" @@ -3030,7 +3014,10 @@ If PARSERESP is nil, don't really parse response buffer but take the value of `last-coq-error-location'. If PARSERESP and CLEAN are non-nil, delete the error location from the response -buffer." +buffer. + +Important: Coq gives char positions in bytes instead of chars. +" (proof-with-current-buffer-if-exists proof-script-buffer (let ((mtch (coq-get-last-error-location parseresp clean))) (when mtch @@ -3038,12 +3025,13 @@ buffer." (lgth (cadr mtch))) (goto-char (+ (proof-unprocessed-begin) 1)) (coq-find-real-start) - - ;; utf8 adaptation is made in coq-get-last-error-location above - (let ((time-offset (if coq-time-commands (length coq--time-prefix) 0))) - (goto-char (+ (point) pos)) - (span-make-self-removing-span (point) (+ (point) (- lgth time-offset)) - 'face 'proof-warning-face))))))) + (message "*** point = %S" (point)) + ;; locations are given in bytes. translate into valid positions + (let* ((beg (goto-char (point-add-bytes pos))) + (end (goto-char (point-add-bytes lgth)))) + (message "*** beg = %S/%S, end = %S/%S" pos beg lgth end) + (goto-char beg) ;; move point to error + (span-make-self-removing-span beg end 'face 'proof-warning-face))))))) (defun coq-highlight-error-hook () (coq-highlight-error t t)) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 14e1ede31..a851ff0f6 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -930,6 +930,10 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*). ;; Low-level commands for shell communication ;; +(defun proof-remove-trailing-blanks (s) + (let ((pos (string-match "\\s-*\\'" s))) + (substring s 0 pos))) + ;;;###autoload (defun proof-shell-insert (strings action &optional scriptspan) "Insert STRINGS at the end of the proof shell, call `scomint-send-input'. @@ -969,8 +973,12 @@ used in `proof-add-to-queue' when we start processing a queue, and in (run-hooks 'proof-shell-insert-hook) ;; Replace CRs from string with spaces to avoid spurious prompts. - (if proof-shell-strip-crs-from-input - (setq string (subst-char-in-string ?\n ?\ string))) + (when proof-shell-strip-crs-from-input + (setq string (subst-char-in-string ?\n ?\ string))) + + ;; avoid feeding the proof assistant with blanks at the end that + ;; will mess with error locations + (setq string (proof-remove-trailing-blanks string)) (insert string)