Made customizable holes mode completion in abbreviations.

3 files changed, 40 insertions, 32 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index 4a62c30f..bcc4a1e4 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -189,6 +189,12 @@ structure."
       (setq lgth (length l)))
     res))
 
+(defcustom coq-holes-minor-mode t
+  "*Whether to apply holes minor mode (see `holes-show-doc') in
+  coq mode."
+  :type 'boolean
+  :group 'coq)
+
 (defun coq-build-abbrev-table-from-db (db)
   "Take a keyword database DB and return an abbrev table.
 See `coq-syntax-db' for DB structure."
@@ -200,8 +206,10 @@ See `coq-syntax-db' for DB structure."
 	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
 	     )
 	;; careful: nconc destructive!
-	(when e2 
-	  (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete)))))
+	(when e2
+	  (if coq-holes-minor-mode
+	      (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))
+	      (setq res (nconc res (list `(,e2 ,e3))))))
 	(setq l tl)))
     res))
 
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 2b2545da..00dbcf60 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -2,7 +2,7 @@
 ;; Copyright (C) 1997-2007 LFCS Edinburgh. 
 ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;; Maintainer: Pierre Courtieu <courtieu@lri.fr>
+;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
 
 ;; $Id$
 
diff --git a/coq/coq.el b/coq/coq.el
index 5d2cab81..e4ebe943 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1499,7 +1499,7 @@ be asked to the user."
 ;; directly to the response buffer. This allows also to clean the response
 ;; buffer (better to only scroll it?)
 (defun coq-get-last-error-location (&optional parseresp clean)
- "Return location information on last error sent by coq.
+  "Return location information on last error sent by coq.
 Return a two elements list (POS LEN) if successful, nil otherwise.
 POS is the number of characters preceding the underlined expression,
 and LEN is its length.
@@ -1519,30 +1519,30 @@ buffer."
   (if (not parseresp) last-coq-error-location
     ;; proof-shell-handle-error-or-interrupt-hook is called from shell buffer
     (with-current-buffer proof-response-buffer
-        (goto-char (point-max))
-        (when (re-search-backward "\n> \\(.*\\)\n> \\( *\\)\\(\\^+\\)\n" 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
-            (when clean (delete-region (+ (match-beginning 0) 1) (match-end 0)))
-            (when proof-shell-unicode
-              ;; `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.
-              (let ((bytes (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)))))))
+      (goto-char (point-max))
+      (when (re-search-backward "\n> \\(.*\\)\n> \\( *\\)\\(\\^+\\)\n" 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
+          (when clean (delete-region (+ (match-beginning 0) 1) (match-end 0)))
+          (when proof-shell-unicode
+            ;; `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.
+            (let ((bytes (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)))))))
 
 
 (defun coq-highlight-error (&optional parseresp clean)
@@ -1569,9 +1569,8 @@ buffer."
         (goto-char (+ (proof-locked-end) 1))
         (coq-find-real-start)
 
-        ; coq error positions are in byte, not in chars, so translate
-        ; for utf-8 error message
-        (goto-char (byte-to-position (+ (position-bytes (point)) pos)))
+        ; Seems to work, even with utf8 chars (emacs23)
+        (goto-char (+ (point) pos))
         (let* ((start (point))
                (dummy (goto-char
                        (byte-to-position (+ (position-bytes (point)) lgth))))
@@ -1581,7 +1580,8 @@ buffer."
               (sit-for 20)
             (span-delete sp)))))))
 
-(defvar coq-allow-highlight-error t)
+(defvar coq-allow-highlight-error t
+  "Internal variable. Do not use as configuration variable.")
 
 ;; if a command is sent to coq without being in the script, then don't
 ;; higilight the error.  Remark: `action' and `string' are known by