diff options
| author | David Aspinall | 2000-05-09 10:13:26 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-05-09 10:13:26 +0000 |
| commit | 63e91b61a837f6aa127b34852a9690abacc95b03 (patch) | |
| tree | 12277ad1155573e8048c640c3810ce6a6fd5c004 | |
| parent | d45ab840ce48b79d792dd07f68ab88b422ea7840 (diff) | |
Improve loading
| -rw-r--r-- | generic/proof-easy-config.el | 1 | ||||
| -rw-r--r-- | generic/proof-indent.el | 13 |
2 files changed, 8 insertions, 6 deletions
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el index d59d4394..af18d843 100644 --- a/generic/proof-easy-config.el +++ b/generic/proof-easy-config.el @@ -70,6 +70,7 @@ (customize-set-variable 'proof-assistant name) (customize-set-variable 'proof-assistant-symbol sym)))) +;;;###autoload (defmacro proof-easy-config (sym name &rest body) "Configure Proof General for proof-assistant using BODY as a setq body." `(progn diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 6849cdd6..00ab6fc6 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -5,16 +5,16 @@ ;; ;; $Id$ ;; -;; FIXME: byte compile complains about not knowing -;; proof-goto-end-of-locked, proof-locked-end -(require 'proof) +(require 'proof) ; loader +(require 'proof-script) ; indent code is for script editing +;;; FIXME: for compilation might be nice ;;; ;;; To nuke byte compile warnings ;;; -(require 'proof-syntax) ; for proof-indent-commands-regexp. -(require 'proof-script) ; for proof-goto-end-of-locked, +;(require 'proof-syntax) ; for proof-indent-commands-regexp. +;(require 'proof-script) ; for proof-goto-end-of-locked, ; proof-locked-end @@ -80,7 +80,8 @@ (forward-char forward-amount)) (list instring cmt-level stack)))) - + +;;;###autoload (defun proof-indent-line () "Indent current line of proof script" (interactive) |