Fixed up proof-script.el for clean byte compile

4 files changed, 125 insertions, 83 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 73e11093..5a4f30a3 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -25,27 +25,14 @@
 ;;     5a. commands
 ;;     5b. regexps
 ;;     5c. hooks
+;;  6. Global constants 
 ;;
-;; The user options don't need to be set on a per-prover basis.
-;; The remaining variables in sections 2-5 do.
+;; The user options don't need to be set on a per-prover basis,
+;; and the global constants probably should not be touched.
+;; The remaining variables in sections 2-5 must be set for
+;; each proof assistant.
 ;;
 
-;;
-;; 0. Global constants
-;; 
-
-(defcustom proof-mode-name "Proof-General"
-  "Root name for proof script mode.  
-Used internally and in menu titles."
-  :type 'string
-  :group 'proof-internal)
-
-(defcustom proof-general-home-page
-  "http://www.dcs.ed.ac.uk/home/proofgen"
-  "*Web address for Proof General"
-  :type 'string
-  :group 'proof-internal)
-
 
 
 ;;
@@ -638,6 +625,37 @@ data triggered by `proof-shell-retract-files-regexp'."
 
 
 
+
+;;
+;; 6. Global constants
+;; 
+(defcustom proof-mode-name "Proof-General"
+  "Root name for proof script mode.  
+Used internally and in menu titles."
+  :type 'string
+  :group 'proof-internal)
+
+(defcustom proof-general-home-page
+  "http://www.dcs.ed.ac.uk/home/proofgen"
+  "*Web address for Proof General"
+  :type 'string
+  :group 'proof-internal)
+
+;; FIXME: da: could we put these into another keymap already?
+;; FIXME: da: it's offensive to experienced users to rebind global stuff
+;;        like meta-tab, this should be removed.
+(defcustom proof-universal-keys
+  (append
+   '(([(control c) (control c)] . proof-interrupt-process)
+    ([(control c) (control v)] . proof-execute-minibuffer-cmd))
+   (if proof-tags-support
+       '(([(meta tab)]	       . tag-complete-symbol))
+     nil))
+"List of keybindings which for the script and response buffer. 
+Elements of the list are tuples (k . f) 
+where `k' is a keybinding (vector) and `f' the designated function."
+  :type 'sexp
+  :group 'proof-internal)
 
 
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 0eb9ef16..fd8c4a6d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -23,34 +23,22 @@
   (require 'func-menu)
   (require 'comint))
 
+;; FIXME:
 ;; More autoloads for proof-shell (added to nuke warnings,
-;; maybe should be 'official' exported functions in proof.el)
-(autoload 'proof-shell-ready-prover "proof-shell")
-(autoload 'proof-start-queue "proof-shell")
-(autoload 'proof-shell-live-buffer "proof-shell")
-(autoload 'proof-shell-invisible-command "proof-shell")
-
+;; maybe some should be 'official' exported functions in proof.el)
+;; This helps see interface between proof-script / proof-shell.
+(eval-when-compile
+  (mapcar (lambda (f) 
+	    (autoload f "proof-script"))
+	  '(proof-shell-ready-prover
+	    proof-start-queue
+	    proof-shell-live-buffer
+	    proof-shell-invisible-command)))
 
 ;;
 ;;  Internal variables used by script mode
 ;;
 
-;; FIXME da: remove proof-terminal-string.  At the moment some
-;; commands need to have the terminal string, some don't.
-;; We should assume commands are terminated at the specific level.
-
-(defvar proof-terminal-string nil 
-  "End-of-line string for proof process.")
-
-
-(defvar proof-action-list nil "action list")
-
-(defvar proof-included-files-list nil 
-  "List of files currently included in proof process.
-Whenever a new file is being processed, it gets added to the front of
-the list. When the prover retracts across file boundaries, this list
-is resynchronised. It contains files in canonical truename format")
-
 (deflocal proof-active-buffer-fake-minor-mode nil
   "An indication in the modeline that this is the *active* script buffer")
 
@@ -87,29 +75,6 @@ This function coincides with `append-element' in the package
       (append ls (list elt))
     ls))
 
-(defun proof-define-keys (map kbl)
-  "Adds keybindings KBL in MAP.
-The argument KBL is a list of tuples (k . f) where `k' is a keybinding
-(vector) and `f' the designated function."
-  (mapcar
-   (lambda (kbl)
-     (let ((k (car kbl)) (f (cdr kbl)))
-         (define-key map k f)))
-   kbl))
-
-(defun proof-string-to-list (s separator) 
-  "Return the list of words in S separated by SEPARATOR."
-  (let ((end-of-word-occurence (string-match (concat separator "+") s)))
-    (if (not end-of-word-occurence)
-        (if (string= s "") 
-            nil
-          (list s))
-      (cons (substring s 0 end-of-word-occurence) 
-            (proof-string-to-list 
-             (substring s
-                        (string-match (concat "[^" separator "]")
-                                      s end-of-word-occurence)) separator)))))
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Basic code for the locked region and the queue region            ;;
@@ -1401,20 +1366,6 @@ sent to the assistant."
 	      (setq proof-script-buffer-list
 		    (remove (current-buffer) proof-script-buffer-list))))))
 
-;; FIXME: da: could we put these into another keymap already?
-;; FIXME: da: it's offensive to experienced users to rebind global stuff
-;;        like meta-tab, this should be removed.
-(defconst proof-universal-keys
-  (append
-   '(([(control c) (control c)] . proof-interrupt-process)
-    ([(control c) (control v)] . proof-execute-minibuffer-cmd))
-   (if proof-tags-support
-       '(([(meta tab)]	       . tag-complete-symbol))
-     nil))
-"List of keybindings which for the script and response buffer. 
-Elements of the list are tuples (k . f) 
-where `k' is a keybinding (vector) and `f' the designated function.")
-
 ;; Fixed definitions in proof-mode-map, which don't depend on
 ;; prover configuration.
 ;;; INDENT HACK: font-lock only recognizes define-key at start of line
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 82672328..12fb689d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -11,6 +11,35 @@
 
 (require 'proof)
 
+;; Nuke some byte compiler warnings.
+
+(eval-when-compile
+  (require 'comint)
+  (require 'font-lock))
+
+;; Spans are our abstraction of extents/overlays.
+(eval-when-compile
+  (cond ((fboundp 'make-extent) (require 'span-extent))
+	((fboundp 'make-overlay) (require 'span-overlay))))
+
+
+;; FIXME:
+;; Autoloads for proof-script (added to nuke warnings,
+;; maybe should be 'official' exported functions in proof.el)
+;; This helps see interface between proof-script / proof-shell.
+(eval-when-compile
+  (mapcar (lambda (f) 
+	    (autoload f "proof-script"))
+	  '(proof-goto-end-of-locked
+	    proof-insert-pbp-command
+	    proof-detach-queue 
+	    proof-locked-end 
+	    proof-set-queue-endpoints
+	    proof-file-to-buffer 
+	    proof-register-possibly-new-processed-file
+	    proof-restart-buffers
+	    proof-dont-show-annotations)))
+
 ;; Internal variables used by shell mode
 ;;
 
@@ -25,7 +54,7 @@ Set in proof-shell-mode.")
 (defvar proof-marker nil 
   "Marker in proof shell buffer pointing to previous command input.")
 
-
+(defvar proof-action-list nil "action list")
 
 
 
@@ -915,6 +944,7 @@ how far we've got."
 ;; OLD COMMENT: "This has to come after proof-mode is defined"
 
 ;;###autoload
+(eval-when-compile			; so that vars are defined
 (define-derived-mode proof-shell-mode comint-mode 
   "proof-shell" "Proof General shell mode class for proof assistant processes"
   (setq proof-buffer-type 'shell)
@@ -946,7 +976,7 @@ how far we've got."
   (setq proof-re-term-or-comment 
 	(concat proof-terminal-string "\\|" (regexp-quote proof-comment-start)
 		"\\|" (regexp-quote proof-comment-end)))
-  )
+  ))
 
 
 (easy-menu-define proof-shell-menu
@@ -980,14 +1010,17 @@ how far we've got."
       (error "Failed to initialise proof process")))
   )
 
+(eval-when-compile			; so that vars are defined
 (define-derived-mode pbp-mode fundamental-mode 
   proof-mode-name "Proof by Pointing"
   ;; defined-derived-mode pbp-mode initialises pbp-mode-map
   (setq proof-buffer-type 'pbp)
-  (suppress-keymap pbp-mode-map 'all)
 ;  (define-key pbp-mode-map [(button2)] 'pbp-button-action)
-  (proof-define-keys pbp-mode-map proof-universal-keys)
-  (erase-buffer))
+  (erase-buffer)))
+
+(suppress-keymap pbp-mode-map 'all)
+(proof-define-keys pbp-mode-map proof-universal-keys)
+
 
 
 
diff --git a/generic/proof.el b/generic/proof.el
index 2575cd2f..06af87dc 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -45,7 +45,7 @@
       "Initialize Proof General and enable it for the current buffer" t))
 
 ;;;
-;;; Utilities/macros used in several files
+;;; Utilities/macros used in several files  (proof-utils)
 ;;;
 
 (defmacro deflocal (var value &optional docstring)
@@ -55,6 +55,29 @@
    (list 'make-variable-buffer-local (list 'quote var))
    (list 'setq-default var value)))
 
+(defun proof-string-to-list (s separator) 
+  "Return the list of words in S separated by SEPARATOR."
+  (let ((end-of-word-occurence (string-match (concat separator "+") s)))
+    (if (not end-of-word-occurence)
+        (if (string= s "") 
+            nil
+          (list s))
+      (cons (substring s 0 end-of-word-occurence) 
+            (proof-string-to-list 
+             (substring s
+                        (string-match (concat "[^" separator "]")
+                                      s end-of-word-occurence)) separator)))))
+
+(defun proof-define-keys (map kbl)
+  "Adds keybindings KBL in MAP.
+The argument KBL is a list of tuples (k . f) where `k' is a keybinding
+(vector) and `f' the designated function."
+  (mapcar
+   (lambda (kbl)
+     (let ((k (car kbl)) (f (cdr kbl)))
+         (define-key map k f)))
+   kbl))
+
 ;;;
 ;;; Global variables
 ;;;
@@ -67,6 +90,12 @@
 When this is non-nil, proof-shell-ready-prover will give
 an error.")
 
+(defvar proof-included-files-list nil 
+  "List of files currently included in proof process.
+Whenever a new file is being processed, it gets added to the front of
+the list. When the prover retracts across file boundaries, this list
+is resynchronised. It contains files in canonical truename format")
+
 (defvar proof-script-buffer-list nil
   "Scripting buffers with locked regions.
 The first element is current and in scripting minor mode.
@@ -85,5 +114,16 @@ The cdr of the list of corresponding file names is a subset of
 (defvar proof-shell-proof-completed nil
   "Flag indicating that a completed proof has just been observed.")
 
+;; FIXME da: remove proof-terminal-string.  At the moment some
+;; commands need to have the terminal string, some don't.
+;; It's used variously in proof-script and proof-shell.
+;; We should assume commands are terminated at the specific level.
+
+(defvar proof-terminal-string nil 
+  "End-of-line string for proof process.")
+
+
+
+
 (provide 'proof)
 ;; proof.el ends here