diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-09 18:17:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-09 18:17:08 +0000 |
| commit | 1044ec7dbc0335ae122fe062f79219ac310a4f09 (patch) | |
| tree | 85b00eb6591bee6abf846c992853f4167847307a /generic/proof-indent.el | |
| parent | 746c0cbf5c4ba0d718de33c74bb7c5fa50607123 (diff) | |
Added proof-script-indent user option, to enable indentation code.
Disabled by default. May be activated by particular proof assistants
if they feel confident about it. I don't.
Made proof-indent be autoloaded as needed. Lets pray it won't be.
Diffstat (limited to 'generic/proof-indent.el')
| -rw-r--r-- | generic/proof-indent.el | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 4fa130e7..868b064c 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -15,12 +15,8 @@ ;;; To nuke byte compile warnings ;;; (require 'proof-syntax) ; for proof-commands-regexp. -(autoload 'proof-goto-end-of-locked "proof-script" - "Jump to the end of the locked region.") -(autoload 'proof-locked-end "proof-script" - "Return end of the locked region of the current buffer.") -;;; -;;; +(require 'proof-script) ; for proof-goto-end-of-locked, + ; proof-locked-end ;; This is quite different from sml-mode, but borrows some bits of @@ -77,6 +73,7 @@ (list instring comment-level stack)))) (defun proof-indent-line () + "Indent current line of proof script" (interactive) (if (and (member (current-buffer) proof-script-buffer-list) (< (point) (proof-locked-end))) |