Finished making holes.el a real minor-mode. There is a new file

holes-load.el which defines the autoloads (enough of them?). All
functions have the prefix "holes-", and offending keyboard shortcuts
have been either removed or bound to the minor mode. I made holes-mode
minor mode automatically turned on in all proof buffers in coq mode
(including shell, script and response buffers as it may be useful to
 copy paste parts of this buffers into holes).

4 files changed, 58 insertions, 16 deletions

diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 3e720aad..adac6527 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -364,8 +364,8 @@
 ;; previous line of previous line.
 
 ;; prevcol is the indentation column of the previous line, prevpoint
-;; is the indetation point of previous line, record tells if we are
-;; inside a the accolades of a record.
+;; is the indentation point of previous line, record tells if we are
+;; inside the accolades of a record.
 
 (defun coq-indent-expr-offset (kind prevcol prevpoint record)
   "Returns the indentation column of the current line. This function indents a *expression* line (a line inside of a command). Use `coq-indent-command-offset' to indent a line belonging to a command. The fourth argument must be t if inside the {}s of a record, nil otherwise."
@@ -481,12 +481,10 @@
 
 (defun coq-indent-offset ()
   (let (kind prevcol prevpoint)
-	 (message "ici")
 	 (save-excursion
 		(setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert)
 				prevcol (current-column)
 				prevpoint (point)))
-	 (message "la")
 	 (cond 
 	  ((= kind 0) 0) ; top of the buffer reached
 	  ((= kind 1) ; we are at the command level
diff --git a/coq/coq.el b/coq/coq.el
index fcd6a753..6735ca42 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -6,7 +6,7 @@
 ;; $Id$ 
 
 (require 'proof)
-(require 'holes) ; in generic directory
+(require 'holes-load) ; in lib directory
 ;; coq-syntaxe is required below
 ;; ----- coq-shell configuration options
 
@@ -369,6 +369,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no
       ;;go to next span
       (setq span (next-span span 'type))
       )
+    ;;let's build the backtrack command now:
     (let (last-staten)
       (setq last-staten (coq-last-statenum-safe))
       (setq ans
@@ -797,6 +798,8 @@ Based on idea mentioned in Coq reference manual."
 
   ;; font-lock
   (setq font-lock-keywords coq-font-lock-keywords-1)
+  ;;holes
+  (holes-mode 1)
 
   (proof-config-done)
 
@@ -815,7 +818,6 @@ Based on idea mentioned in Coq reference manual."
                      tag-table-alist)))
 
   (setq blink-matching-paren-dont-ignore-comments t)
-
   ;; multiple file handling
   (setq proof-cannot-reopen-processed-files t
         ;; proof-shell-inform-file-retracted-cmd 'coq-retract-file
@@ -867,7 +869,7 @@ Based on idea mentioned in Coq reference manual."
   
   (coq-init-syntax-table)
   (setq font-lock-keywords coq-font-lock-keywords-1)
-
+  (holes-mode 1)
   (proof-shell-config-done))
 
 (defun coq-goals-mode-config ()
@@ -875,11 +877,13 @@ Based on idea mentioned in Coq reference manual."
   (setq pg-goals-error-regexp coq-error-regexp)
   (coq-init-syntax-table)
   (setq font-lock-keywords coq-font-lock-keywords-1)
+  (holes-mode 1)
   (proof-goals-config-done))
 
 (defun coq-response-config ()
    (coq-init-syntax-table)
    (setq font-lock-keywords coq-font-lock-keywords-1)
+   (holes-mode 1)
    (proof-response-config-done))
 
 
diff --git a/lib/holes-load.el b/lib/holes-load.el
new file mode 100644
index 00000000..0c0a8b80
--- /dev/null
+++ b/lib/holes-load.el
@@ -0,0 +1,14 @@
+; To use holes-mode, require this file in your .emacs and add path to
+; holes.el in the load-path of emacs
+
+(autoload 'holes-mode "holes"
+  "Minor mode for using \"holes\" in your buffers." t)
+(autoload 'holes-set-make-active-hole "holes"
+  "Makes a new hole and make it active." t)
+(autoload 'holes-abbrev-complete "holes"
+  "Completes an abbreviation, and replace #s ans @{}s by holes.")
+(autoload 'holes-insert-and-expand "holes"
+  "insert and expand an abbreviation, and replace #s ans @{}s by holes.")
+
+(provide 'holes-load)
+
diff --git a/lib/holes.el b/lib/holes.el
index cf2ddfa0..a48e9935 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -20,8 +20,6 @@
 
 (require 'span)
 
-;(defvar holes-mode)
-
 (defun holes-short-doc ()
   "prints a short doc for holes"
   (interactive)
@@ -740,16 +738,29 @@ and this is this one. This is not buffer local.")
     map)
   "Keymap to use on the holes's overlays.")
 
+(defvar holes-mode-map
+  (let ((map (make-sparse-keymap)))
+	 (define-key map [(control c) h] 'holes-set-make-active-hole)
+	 (define-key map [(control c) (meta y)] 'holes-replace-update-active-hole)
+	 (define-key map [(control meta down-mouse-1)] 'holes-mouse-set-make-active-hole)
+	 (define-key map [(control meta shift down-mouse-1)] 'holes-mouse-replace-active-hole)
+	 (define-key map [(meta return)] 'holes-set-point-next-hole-destroy)
+    map)
+  "Keymap of holes-mode. This is not the keymap used on holes's overlay
+(see `hole-map' instead). This one is active whenever we are on a
+buffer where holes-mode is active.")  
+
+(message "holes: milieu")
+
+(or (assq 'holes-mode minor-mode-map-alist)
+    (setq minor-mode-map-alist
+          (cons (cons 'holes-mode holes-mode-map)
+                minor-mode-map-alist)))
 
+(message "holes: milieu après")
 
-;  (global-set-key  [(control meta ? ) ] 'holes-set-active-hole-next)
+;(global-set-key  [(control meta **WRONG** space ) ] 'holes-set-active-hole-next)
 
-;  (global-set-key [(control meta y)] 'holes-replace-update-active-hole)
-  ; this shortcut was for mark-defun
-;  (global-set-key [(control meta h)]   'holes-set-make-active-hole)
-;  (global-set-key [(control meta down-mouse-1)] 'holes-mouse-set-make-active-hole)
-;  (global-set-key [(control meta shift down-mouse-1)] 'holes-mouse-replace-active-hole)
-;  (global-set-key [(meta return)] 'holes-set-point-next-hole-destroy)
 
 ;;;;;;;;;;; End Customizable key bindings ;;;;;
 
@@ -920,5 +931,20 @@ created. return t if num is > 0, nil otherwise."
 	 )
   )
 
+(defvar holes-mode nil "t if holes mode is on, nil otherwise.")
+
+(defun holes-mode (&optional arg)
+  "if arg is nil, then toggle holes mode on/off. If arg is
+positive, then turn holes mode on. If arg is negative, then
+turn it off."
+  (interactive)
+  (setq holes-mode (if (null arg) (not holes-mode)
+							(> (prefix-numeric-value arg) 0)))
+  )
+
+(or (assq 'holes-mode minor-mode-alist)
+	 (setq minor-mode-alist
+			 (cons '(holes-mode " Holes") minor-mode-alist)))
+
 (provide 'holes)