diff options
| -rw-r--r-- | coq/coq-indent.el | 6 | ||||
| -rw-r--r-- | coq/coq.el | 10 | ||||
| -rw-r--r-- | lib/holes-load.el | 14 | ||||
| -rw-r--r-- | lib/holes.el | 44 |
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 @@ -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) |