diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-20 14:24:51 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-20 14:24:51 +0000 |
| commit | 42e140a8405b11a04b309ed3f99805aaa44c5268 (patch) | |
| tree | ffd32fbfd83842e0253da799cab264e03798b8a8 /generic/proof-indent.el | |
| parent | df5251b00f874b9081cf48a2bda8d848b7710750 (diff) | |
BIG CHANGES -- SORRY!
Replaced proof-script-buffer-list with proof-script-buffer.
The list was causing too much confusion and nasty bugs used with
Isabelle multiple files.
Implemented proof-script-buffers and proof-restart-all-buffers,
other functions.
Diffstat (limited to 'generic/proof-indent.el')
| -rw-r--r-- | generic/proof-indent.el | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 868b064c..4cf14084 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -6,8 +6,7 @@ ;; $Id$ ;; ;; FIXME: byte compile complains about not knowing -;; proof-script-buffer-list, proof-goto-end-of-locked, -;; proof-locked-end +;; proof-goto-end-of-locked, proof-locked-end (require 'proof) @@ -33,9 +32,7 @@ (end (point)) instring c) (save-excursion (if (null from) - (if (member (current-buffer) proof-script-buffer-list) - (proof-goto-end-of-locked) - (goto-char 1)) + (proof-goto-end-of-locked) (goto-char from) (setq instring (car state) comment-level (nth 1 state) @@ -75,8 +72,7 @@ (defun proof-indent-line () "Indent current line of proof script" (interactive) - (if (and (member (current-buffer) proof-script-buffer-list) - (< (point) (proof-locked-end))) + (if (< (point) (proof-locked-end)) (if (< (current-column) (current-indentation)) (skip-chars-forward "\t ")) (save-excursion @@ -94,8 +90,7 @@ (defun proof-indent-region (start end) (interactive "r") - (if (and (member (current-buffer) proof-script-buffer-list) - (< (point) (proof-locked-end))) + (if (< (point) (proof-locked-end)) (error "can't indent locked region!")) (save-excursion (goto-char start) |