diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2005-02-15 18:35:28 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2005-02-15 18:35:28 +0000 |
| commit | 53a064b3643455b8df0527798ab1fd58f7227c3b (patch) | |
| tree | 695f35d4f9993218bf9a404308844fc390a113b9 /coq/coq-indent.el | |
| parent | dcf999c2498f16c1f230a0ebeb182a07f466f813 (diff) | |
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).
Diffstat (limited to 'coq/coq-indent.el')
| -rw-r--r-- | coq/coq-indent.el | 6 |
1 files changed, 2 insertions, 4 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 |