Opened 10 years ago

Closed 9 years ago

#485 closed defect (fixed)

"Time commands" option offsets the cursor when errors are reported

Reported by: coquser Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords: coq-time-commands time commands cursor
Cc:

Description

When activating the "Time Commands" option, every time an error is displayed, the cursor is off 5 characters to the right.

Happens in the latest development build as well as in the last stable.

To reproduce, open a buffer and type:

Inductive t := T : x -> y -> t.

Try to run it when "Time Commands" is on. The error is reported on the t character instead of the y character.

Change History (2)

comment:1 Changed 9 years ago by coquser

Here's a patch

--- coq.el.~11.203.~	2015-04-27 11:06:17.183468737 -0400
+++ coq.el	2015-04-27 13:35:56.779091243 -0400
@@ -1895,11 +1895,13 @@
 ;; Pre-processing of input string
 ;;
 
+(defconst coq--time-prefix "Time ")
+
 ;; Remark: `action' and `string' are known by `proof-shell-insert-hook'
 (defun coq-preprocessing ()
   (if coq-time-commands
       (with-no-warnings  ;; NB: dynamic scoping of `string'
-        (setq string (concat "Time " string)))))
+        (setq string (concat coq--time-prefix string)))))
 
 (add-hook 'proof-shell-insert-hook 'coq-preprocessing)
 
@@ -2392,7 +2394,8 @@
           (coq-find-real-start)
           
           ;; utf8 adaptation is made in coq-get-last-error-location above
-          (goto-char (+ (point) pos))
+          (let ((time-offset (if coq-time-commands (length coq--time-prefix) 0)))
+            (goto-char (+ (point) (- pos time-offset))))
           (span-make-self-removing-span (point) (+ (point) lgth)
                                         'face 'proof-warning-face))))))

-- cpitcla

comment:2 Changed 9 years ago by courtieu

Resolution: fixed
Status: newclosed

Fixed. Thanks.

Note: See TracTickets for help on using tickets.