Begun work on clean byte compilation / clarifying interfaces.

16 files changed, 157 insertions, 97 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 73f58af9..17bb6d6b 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -6,9 +6,11 @@
 
 ;; $Id$
 
+(require 'proof)
 (require 'coq-syntax)
+
+;; FIXME: outline and info should be autoloaded.
 (require 'outline)
-(require 'proof)
 (require 'info)
 
 ; Configuration
diff --git a/generic/proof-config.el b/generic/proof-config.el
index c342631e..bec16319 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1,4 +1,4 @@
-;; proof-config.el  Proof General configuration for proof assistant.
+;; proof-config.el  Proof General configuration for proof assistant
 ;;
 ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
 ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
@@ -628,5 +628,8 @@ data triggered by `proof-shell-retract-files-regexp'."
 
 
 
+
+
+
 ;; End of proof-config.el
 (provide 'proof-config)
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index 515c304f..74638bef 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -5,9 +5,11 @@
 ;;
 ;; $Id$
 ;;
+;; FIXME: byte compile complains about not knowing
+;; proof-script-buffer-list, proof-goto-end-of-locked,
+;; proof-locked-end
 
-(require 'cl)
-(require 'proof-syntax)
+(require 'proof)
 
 (defvar proof-stack-to-indent nil
   "Prover-specific code for indentation.")
diff --git a/generic/proof-script.el b/generic/proof-script.el
index d5ad9587..4486ab9a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -9,7 +9,16 @@
 ;; $Id$
 ;;
 
-(require 'proof-config)
+(require 'proof)
+(require 'proof-syntax)
+(require 'proof-indent)
+
+;; Spans are our abstraction of extents/overlays.
+(cond ((fboundp 'make-extent) (require 'span-extent))
+      ((fboundp 'make-overlay) (require 'span-overlay)))
+
+(eval-when-compile
+  (require 'func-menu))
 
 ;;
 ;;  Internal variables used by script mode
@@ -23,26 +32,6 @@
 (defvar proof-terminal-string nil 
   "End-of-line string for proof process.")
 
-(defvar proof-marker nil 
-  "Marker in proof shell buffer pointing to previous command input.")
-
-(defvar proof-shell-buffer nil
-  "Process buffer where the proof assistant is run.")
-
-(defvar proof-script-buffer-list nil
-  "Scripting buffers with locked regions.
-The first element is current and in scripting minor mode.
-The cdr of the list of corresponding file names is a subset of
-`proof-included-files-list'.")
-
-(defvar proof-pbp-buffer nil
-  "The goals buffer (also known as the pbp buffer).")
-
-(defvar proof-response-buffer nil
-  "The response buffer.")
-
-(deflocal proof-buffer-type nil 
-  "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.")
 
 (defvar proof-action-list nil "action list")
 
@@ -69,7 +58,7 @@ name. Moves point after the match.
 
 The package fume-func provides the function
 `fume-match-find-next-function-name' with the same specification.
-However, fume-func's version is incorrec"
+However, fume-func's version is incorrect"
   ;; DO NOT USE save-excursion; we need to move point!
   ;; save-excursion is called at a higher level in the func-menu
   ;; package 
@@ -1360,9 +1349,11 @@ sent to the assistant."
 ;; sml-mode.
 ;; FIXME: add more doc to the mode below, to give hints on
 ;; configuring for new assistants.
+
+;;;###autoload
 (define-derived-mode proof-mode fundamental-mode 
   proof-mode-name
-  "Proof General major mode for proof scripts.
+  "Proof General major mode class for proof scripts.
 \\{proof-mode-map}"
   (setq proof-buffer-type 'script)
 
@@ -1467,7 +1458,7 @@ finish setup which depends on specific proof assistant configuration."
   (setq indent-line-function 'proof-indent-line)
 
   ;; Toolbar
-  (if (featurep 'proof-toolbar)
+  (if (featurep 'toolbar)
       (proof-toolbar-setup))
 
   ;; Menu
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 24bb5bef..2fb74034 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -9,7 +9,7 @@
 ;; $Id$
 ;;
 
-(require 'proof-config)
+(require 'proof)
 
 ;; Internal variables used by shell mode
 ;;
@@ -22,6 +22,11 @@ Set in proof-shell-mode.")
   "Regexp matching terminator, comment start, or comment end.
 Set in proof-shell-mode.")
 
+(defvar proof-marker nil 
+  "Marker in proof shell buffer pointing to previous command input.")
+
+
+
 
 
 
@@ -35,11 +40,6 @@ Set in proof-shell-mode.")
 ;;
 ;;
 
-(defvar proof-shell-busy nil 
-  "A lock indicating that the proof shell is processing.
-When this is non-nil, proof-shell-ready-prover will give
-an error.")
-
 ;;
 ;; History of these horrible functions.
 ;;
@@ -351,9 +351,6 @@ The default value is \"\n\" to match up to the end of the line.")
 (defvar proof-shell-delayed-output nil
   "Last interesting output from proof process output and what to do with it.")
 
-(defvar proof-shell-proof-completed nil
-  "Flag indicating that a completed proof has just been observed.")
-
 (defvar proof-analyse-using-stack nil
   "Are annotations sent by proof assistant local or global")
 
@@ -933,9 +930,11 @@ how far we've got."
 ;; Proof General shell mode definition				    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; This has to come after proof-mode is defined
+;; OLD COMMENT: "This has to come after proof-mode is defined"
+
+;;###autoload
 (define-derived-mode proof-shell-mode comint-mode 
-  "proof-shell" "Proof shell mode - not standalone"
+  "proof-shell" "Proof General shell mode class for proof assistant processes"
   (setq proof-buffer-type 'shell)
   (setq proof-shell-busy nil)
   (setq proof-shell-delayed-output (cons 'insert "done"))
diff --git a/generic/proof-site.el b/generic/proof-site.el
index d88d2324..ea3b7198 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -132,6 +132,18 @@ NOTE: to change proof assistant, you must start a new Emacs session.")
       (setq load-path
 	    (cons proof-lisp-path load-path))))
 
+;; During compilation from the Makefile, generic is on the load path.
+;; Add all of the prover directories.
+;; FIXME: this doesn't work quite right.  We want to test
+;; whether we are running during a compilation.  How?
+; (eval-when-compile
+;  (dolist (assistant proof-internal-assistant-table)
+;    (let ((path (concat proof-internal-home-directory
+;			(concat (symbol-name (car assistant)) "/"))))
+;      (or (member path load-path)
+;	  (setq load-path
+;		(cons path load-path))))))
+
 ;; Now add auto-loads and load-path elements to support the 
 ;; proof assistants selected, and define a stub 
 (let ((assistants proof-assistants) assistant)
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index f5e83ee3..9f83e936 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -157,7 +157,9 @@ Only do it if proof-splash-display is nil."
 ;; redisplay until proof-internal-display-splash-time has elapsed. 
 
 ;; Display the screen ASAP...
-(proof-splash-display-screen)
+;; FIXME: don't want this to display during compilation!
+(eval-when (load)
+  (proof-splash-display-screen))
 
 (defun proof-splash-timeout-waiter ()
   "Wait for proof-splash-timeout, then remove self from hook."
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 265791db..9ea7ee56 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -6,6 +6,7 @@
 ;; $Id$
 ;;
 
+
 (require 'font-lock)
 
 ;;; FIXME: change this to proof-
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index f562ed14..68c73834 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -10,7 +10,12 @@
 ;; Toolbar is just for scripting buffer at  the moment.
 ;;
 
-(require 'proof-config)
+(require 'proof-script)
+(require 'proof-shell)
+
+;; FIXME: would be nice to have proof-shell autoloaded when shell is
+;; actually started.  Need to fixup references to variables here to be
+;; autoloaded functions from proof-shell, and remove from enablers.
 
 (defcustom proof-toolbar-wanted t
   "*Whether to use toolbar in proof mode."
@@ -31,6 +36,20 @@
 This gives a bare toolbar that works for any prover.  To add
 prover specific buttons, see proof-toolbar.el.")
 
+(defconst proof-toolbar-iconlist
+  '((proof-toolbar-next-icon "next")
+    (proof-toolbar-undo-icon "undo")
+    (proof-toolbar-retract-icon "retract")
+    (proof-toolbar-use-icon "use")
+    (proof-toolbar-goal-icon "goal")
+    (proof-toolbar-qed-icon  "qed")
+    (proof-toolbar-restart-icon "restart"))
+  "List of icon variable names and their associated image files.
+A list of lists of the form (VAR IMAGE).  IMAGE is the root name
+for an image file in proof-internal-images-directory.  The toolbar
+code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm
+and chooses the best one for the display properites.")
+
 (defvar proof-toolbar-button-list proof-toolbar-default-button-list
   "A toolbar descriptor evaluated in proof-toolbar-setup.
 Specifically, a list of sexps which evaluate to entries in a toolbar
@@ -40,15 +59,25 @@ will work for any proof assistant.")
 (defvar proof-toolbar nil
   "Proof mode toolbar button list.  Set in proof-toolbar-setup.")
 
+(defconst proof-old-toolbar default-toolbar
+  "Saved value of default-toolbar for proofmode.")
+
+
 ;; FIXME: edit-toolbar cannot edit proof toolbar (even in a proof mode)
 ;; Need a variable containing  a specifier or similar.
-; (defvar proof-toolbar-specifier nil
-;   "Specifier for proof toolbar.")
+;; (defvar proof-toolbar-specifier nil
+;;   "Specifier for proof toolbar.")
+;; This doesn't seem worth fixing until XEmacs toolbar implementation
+;; settles a bit.  Enablers don't work too well at the moment.
 
+;; FIXME: could automatically defvar the icon variables.
+
+;;; ###autoload
 (defun proof-toolbar-setup ()
-  "Initialize proof-toolbar and enable it for the current buffer.
+  "Initialize Proof General toolbar and enable it for the current buffer.
 If proof-mode-use-toolbar is nil, change the current buffer toolbar
 to the default toolbar."
+  (interactive)
   (if (and
        proof-toolbar-wanted
        ;; NB for FSFmacs use window-system, not console-type
@@ -74,9 +103,6 @@ to the default toolbar."
 	(set-specifier default-toolbar proof-toolbar (current-buffer)))
     (set-specifier default-toolbar proof-old-toolbar (current-buffer))))
 
-(defconst proof-old-toolbar default-toolbar
-  "Saved value of default-toolbar for proofmode.")
-
 ;;
 ;; GENERIC PROOF TOOLBAR BUTTONS
 ;;
@@ -186,16 +212,6 @@ Initialised in proof-toolbar-setup.")
    ;; (proof-toolbar-qed-enable-p)
    "Save proved theorem"])
 
-(defconst proof-toolbar-iconlist
-  '((proof-toolbar-next-icon "next")
-    (proof-toolbar-undo-icon "undo")
-    (proof-toolbar-retract-icon "retract")
-    (proof-toolbar-use-icon "use")
-    (proof-toolbar-goal-icon "goal")
-    (proof-toolbar-qed-icon  "qed")
-    (proof-toolbar-restart-icon "restart"))
-  "List of icon variable names and their associated image files")
-
 ;;
 ;; GENERIC PROOF TOOLBAR FUNCTIONS
 ;;
@@ -280,6 +296,7 @@ Move point if the end of the locked position is invisible."
   "Insert a save theorem command into the script buffer, issue it."
   (interactive)
   (if (proof-toolbar-qed-enable-p)
-      (call-interactively 'proof-issue-save)))
+      (call-interactively 'proof-issue-save)
+    (error "I can't see a completed proof!")))
 ;; 
 (provide 'proof-toolbar)
\ No newline at end of file
diff --git a/generic/proof.el b/generic/proof.el
index 890c5275..bd4669a6 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;; proof.el  Proof General loader.
+;; proof.el  Proof General loader.  All files require this one.
 ;;
 ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
 ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen,
@@ -15,26 +15,16 @@
 
 (require 'proof-site)			; site config
 
-(require 'proof-config)			; variables
+(require 'proof-config)			; configuration variables
 
 (require 'proof-splash)			; splash screen
 
-;; FIXME da: I think these ones should be autoloaded!!
-(require 'cl)
-(require 'compile)
-(require 'comint)
-(require 'etags)			
-(require 'easymenu)
-
-
-;; Spans are our abstraction of extents/overlays.
-(cond ((fboundp 'make-extent) (require 'span-extent))
-      ((fboundp 'make-overlay) (require 'span-overlay))
-      (t nil))
-
-(require 'proof-syntax)
-(require 'proof-indent)
-
+;; FIXME da: I think these should all be autoloaded!!
+;; (require 'cl)
+;; (require 'compile)
+;; (require 'comint)
+;; (require 'etags)			
+;; (require 'easymenu)
 
 ;; browse-url function doesn't seem to be autoloaded in
 ;; XEmacs 20.4, but it is in FSF Emacs 20.2.
@@ -42,6 +32,22 @@
     (autoload 'browse-url "browse-url"
       "Ask a WWW browser to load URL." t))
 
+;;; Autoloads for main code
+
+(autoload 'proof-mode "proof-script"
+  "Proof General major mode class for proof scripts.")
+
+(autoload 'proof-shell-mode "proof-shell"
+  "Proof General shell mode class for proof assistant processes")
+
+(if (featurep 'toolbar)
+    (autoload 'proof-toolbar-setup "proof-toolbar"
+      "Initialize Proof General and enable it for the current buffer" t))
+
+;;;
+;;; Utilities/macros used in several files
+;;;
+
 (defmacro deflocal (var value &optional docstring)
   "Define a buffer local variable VAR with default value VALUE."
  (list 'progn
@@ -49,15 +55,35 @@
    (list 'make-variable-buffer-local (list 'quote var))
    (list 'setq-default var value)))
 
+;;;
+;;; Global variables
+;;;
 
-;; Load toolbar code if toolbars available.
-(if (featurep 'toolbar)
-    (require 'proof-toolbar))
+(deflocal proof-buffer-type nil 
+  "Symbol indicating the type of this buffer: 'script, 'shell, or 'pbp.")
+
+(defvar proof-shell-busy nil 
+  "A lock indicating that the proof shell is processing.
+When this is non-nil, proof-shell-ready-prover will give
+an error.")
+
+(defvar proof-script-buffer-list nil
+  "Scripting buffers with locked regions.
+The first element is current and in scripting minor mode.
+The cdr of the list of corresponding file names is a subset of
+`proof-included-files-list'.")
+
+(defvar proof-shell-buffer nil
+  "Process buffer where the proof assistant is run.")
+
+(defvar proof-pbp-buffer nil
+  "The goals buffer (also known as the pbp buffer).")
 
-;; Main code is in these files
-(require 'proof-script)
-(require 'proof-shell)
+(defvar proof-response-buffer nil
+  "The response buffer.")
 
+(defvar proof-shell-proof-completed nil
+  "Flag indicating that a completed proof has just been observed.")
 
 (provide 'proof)
 ;; proof.el ends here
diff --git a/generic/span-extent.el b/generic/span-extent.el
index 91ad6ac9..db1a70cd 100644
--- a/generic/span-extent.el
+++ b/generic/span-extent.el
@@ -31,6 +31,10 @@
   "Set the end point of SPAN to VALUE."
   (set-extent-endpoints span (extent-start-position span) value))
 
+(defsubst set-span-property (span name value)
+  "Set SPAN's property NAME to VALUE."
+  (set-extent-property span name value))
+
 (defsubst span-read-only (span)
   "Set SPAN to be read only."
   (set-span-property span 'read-only t))
@@ -43,10 +47,6 @@
   "Return SPAN's value for property PROPERTY."
   (extent-property span name))
 
-(defsubst set-span-property (span name value)
-  "Set SPAN's property NAME to VALUE."
-  (set-extent-property span name value))
-
 (defsubst delete-span (span)
   "Delete SPAN."
   (delete-extent span))
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 93ad9758..07373805 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -9,7 +9,6 @@
 
 (require 'proof-syntax)
 
-
 ;;; Proof mode customization: how should it work?
 ;;;   Presently we have a bunch of variables in proof.el which are
 ;;;   set from a bunch of similarly named variables in <engine>-syntax.el.
diff --git a/isa/isa.el b/isa/isa.el
index 5bbde8fa..3c1d4ad8 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -9,11 +9,14 @@
 ;;
 
 
-(require 'isa-syntax)
-(require 'outline)
 (setq proof-tags-support nil)  ; we don't want it, no isatags prog.
 (require 'proof)
 
+(require 'isa-syntax)
+
+;; FIXME: outline should be autoloaded
+(require 'outline)			
+
 
 ;;;
 ;;; ======== User settings for Isabelle ========
diff --git a/isa/thy-mode.el b/isa/thy-mode.el
index 57568a63..641be424 100644
--- a/isa/thy-mode.el
+++ b/isa/thy-mode.el
@@ -10,6 +10,7 @@
 ;; NAMESPACE management: all functions and variables declared
 ;; in this file begin with isa-thy-
 
+(require 'proof-site)
 (require 'isa)
 
 ;;; ========== Theory File Mode User Options ==========
diff --git a/lego/lego.el b/lego/lego.el
index f0564857..2ea0594e 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -9,9 +9,11 @@
 ;; $Id$
 ;;
 
+(require 'proof)
 (require 'lego-syntax)
+
+;; FIXME: outline should be autoloaded
 (require 'outline)
-(require 'proof)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; User Configuration ;;;
diff --git a/todo b/todo
index f51f13d4..a82274ba 100644
--- a/todo
+++ b/todo
@@ -14,6 +14,13 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
+A byte-compilation: continue fixups for clean byte compile.
+  Need to compile from clean Emacs to see proper warnings.
+  Unfortunately I get odd Arithmetic Errors when comiling.
+  Check that byte compilation (and compiled code!) 
+  works for both varieties of Emacs.  Add instructions to INSTALL on 
+  how to byte compile.  Fill out Makefile.dist (2hr da)
+
 C  Remove "FIXME notes" which are just notes I've put in about old
    code in case something breaks   (da, 30mins).
 
@@ -26,9 +33,6 @@ A* Fixup for non-script buffer locking:
 
     proof-restart-script is now broken (2h da)
 
-A* Fixup for clean byte compile now that proof.el has been split.
-   (30min da)
-
 A* Fixup multiple files -- needs debugging.
 
    1. mark atomic makes some assumption about non-comment commands in
@@ -44,10 +48,6 @@ A* Fixup multiple files -- needs debugging.
 B Improve web pages after suggestions in doc/notes.txt
   (da, 1.5hrs)
 
-C byte-compilation: check that byte compilation (and compiled code!)
-  works for both varieties of Emacs.  Add instructions to INSTALL on 
-  how to byte compile.  (1hr)
-
 C Remove .gif, .jpg, .xpm, .xbm files from the CVS repository.  Add 
   .cvsignore's for them instead.  Disadvantage: developers will need
   to have the Gimp installed to build them via 'make images'