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.

4 files changed, 24 insertions, 19 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index b7860a3f..c047f342 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -107,6 +107,16 @@ you a reprimand!)"
   :type 'boolean
   :group 'proof-general)
 
+(defcustom proof-script-indent nil
+  ;; Particular proof assistants can enable this if they feel
+  ;; confident about it.  (I don't). -da
+  "If non-nil, enable indentation code for proof scripts.
+Currently the indentation code can be rather slow for large scripts,
+or may be critical on the setting of regular expressions for 
+particular provers."
+  :type 'boolean
+  :group 'proof-general)
+
 ;;
 ;; Faces.
 ;; We ought to test that these work sensibly:
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)))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index f9b4a0b4..403f1af4 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -11,7 +11,12 @@
 
 (require 'proof)
 (require 'proof-syntax)
-(require 'proof-indent)
+
+;; If it's disabled by proof-script-indent, it won't need to be
+;; loaded.
+(autoload 'proof-indent-line "proof-indent" 
+	   "Indent current line of proof script")
+
 
 ;; Spans are our abstraction of extents/overlays.
 (eval-and-compile
@@ -1444,9 +1449,6 @@ sent to the assistant."
 (define-key map [(control c) ?h]	  'proof-help)
 (define-key map [(meta p)]		  'proof-previous-matching-command)
 (define-key map [(meta n)]		  'proof-next-matching-command)
-;; FIXME da: this shouldn't need setting, because it works
-;; via indent-line-function which is set below.  Check this.
-(define-key map [tab] 'proof-indent-line)
 (proof-define-keys map proof-universal-keys))
 
 
@@ -1498,8 +1500,8 @@ finish setup which depends on specific proof assistant configuration."
     'proof-active-terminator)
 
   (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'proof-indent-line)
-
+  (if proof-script-indent
+      (setq indent-line-function 'proof-indent-line))
 
   ;; Toolbar
   ;; (NB: autloads proof-toolbar, which extends proof-menu variable)
diff --git a/todo b/todo
index f6664848..2646ce38 100644
--- a/todo
+++ b/todo
@@ -64,13 +64,9 @@ A Revise ProofGeneral.texi and publish LaTeX version as an LFCS
 
 A* Bug in proof-mode configuration of func-menu.  (30mins)
 
-A* FIX INDENTATION CODE, EDITING .ML (& other?) FILES IS CHRONICALLY SLOW.
-  This is going to hit us hard as soon as the mode gets used in
-  earnest.
-  (da, 10mins: disable it!)
-  (da, 2hrs: will investigate if fault lies with Isabelle syntax config)
-  (8hrs, estimated time to fixup indentation code otherwise.  May be
-         best removed altogether, or replaced with elisp code clone)
+C Improve indentation code and see why it's so slow (at
+  least for Isabelle).   Enable it for particular provers if
+  it works okay  (but must test in on large files).
 
 C Regions in script buffer have nice "name" property and configurers
   have to set regexps carefully so that it works, but is it actually