diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-24 23:36:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-24 23:36:23 +0000 |
| commit | f6ffea40923b498a8a65c99214b08749a3126e9d (patch) | |
| tree | 295ce918dfb7a50a10ef2dbd1608f3143850ba37 /generic | |
| parent | 15af2f935c8ffc6e6b36f709f07f3ff18309c2e6 (diff) | |
Fixes and cleanups for coq-indent-line, see Trac #172
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-indent.el | 6 | ||||
| -rw-r--r-- | generic/proof-script.el | 12 |
2 files changed, 11 insertions, 7 deletions
diff --git a/generic/proof-indent.el b/generic/proof-indent.el index ab0a522c..e792d931 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -60,7 +60,8 @@ (found-prev (proof-indent-goto-prev))) (if (not found-prev) (goto-char current)) ; recover position (cond - ((and found-prev (or proof-indent-hang (= (current-indentation) (current-column)))) + ((and found-prev (or proof-indent-hang + (= (current-indentation) (current-column)))) (+ indent (current-column) (if (and inner (not (proof-indent-inner-p))) 0 (proof-indent-indent)) @@ -83,7 +84,8 @@ (indent-line-to (max 0 (save-excursion (back-to-indentation) - (proof-indent-calculate (proof-indent-offset) (proof-indent-inner-p)))))) + (proof-indent-calculate + (proof-indent-offset) (proof-indent-inner-p)))))) (if (< (current-column) (current-indentation)) (back-to-indentation))))) diff --git a/generic/proof-script.el b/generic/proof-script.el index 7b45c797..447d4176 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2459,7 +2459,10 @@ command." ;; We also need this (modify-syntax-entry ?\n " "))) - + ;; Set default indent function (can be overriden in derived modes) + (make-local-variable 'indent-line-function) + (setq indent-line-function 'proof-indent-line) + ;; During write-file it can happen that we re-set the mode for ;; the currently active scripting buffer. The user might also ;; do this for some reason. We could maybe let @@ -2474,10 +2477,12 @@ command." ;; that they can be adjusted by prover specific code if need be. (proof-script-set-buffer-hooks) - (add-hook 'after-set-visited-file-name-hooks 'proof-script-set-visited-file-name nil t) + (add-hook 'after-set-visited-file-name-hooks + 'proof-script-set-visited-file-name nil t) (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)) + (proof-menu-define-keys proof-mode-map) ;; NB: proof-mode-map declared above (defun proof-script-set-visited-file-name () @@ -2779,9 +2784,6 @@ finish setup which depends on specific proof assistant configuration." (define-key proof-mode-map (vector proof-terminal-char) 'proof-electric-terminator))) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'proof-indent-line) - ;; Toolbar and scripting menu ;; NB: autoloads proof-toolbar, which defines proof-toolbar-scripting-menu. (proof-toolbar-setup) |