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

2 files changed, 49 insertions, 9 deletions

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)