Added todo for clean byte compile

5 files changed, 166 insertions, 99 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index f5fb761d..5c82946e 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -9,22 +9,65 @@
 ;; $Id$
 ;;
 ;; 
-;; This file declares all prover-specific configuration variables.
-;; These are used variously by the proof script mode and the proof
-;; shell mode.
+;; This file declares all user options and prover-specific
+;; configuration variables for Proof General.  The variables
+;; are used variously by the proof script mode and the 
+;; proof shell mode, menus, and toolbar.
 ;; 
 ;; To customize Proof General for a new proof assistant, you
 ;; should read this file carefully! 
 ;;
-;;  0. Major modes
-;;  1. Menus, user-level commands.
-;;  2. Script mode configuration 
-;;  3. Shell mode configuration
-;;     3a. commands
-;;     3b. regexps
-;;     3c. hooks
+;;  1. User options 
+;;  2. Major modes
+;;  3. Menus, user-level commands.
+;;  4. Script mode configuration 
+;;  5. Shell mode configuration
+;;     5a. commands
+;;     5b. regexps
+;;     5c. hooks
 ;;
+;; The user options don't need to be set on a per-prover basis.
+;; The remaining variables in sections 2-5 do.
+;;
+
 
+;; A global constant that's convenient to keep here.
+(defconst proof-mode-name "Proof-General"
+  "Root name for proof script mode.  
+Used internally and in menu titles.")
+
+
+
+;;
+;; 1. User options for proof mode
+;;
+;; The following variables are user options for Proof General.
+;; They appear in the 'proof' customize group and should
+;; *not* normally be touched by prover specific code.
+;;
+
+(defcustom proof-prog-name-ask-p nil
+  "*If non-nil, query user which program to run for the inferior process."
+  :type 'boolean
+  :group 'proof)
+
+(defcustom proof-one-command-per-line nil
+  "*If non-nil, format for newlines after each proof command in a script."
+  :type 'boolean
+  :group 'proof)
+
+(defcustom proof-general-home-page
+  "http://www.dcs.ed.ac.uk/home/proofgen"
+  "*Web address for Proof General"
+  :type 'string
+  :group 'proof-internal)
+
+
+
+;;
+;; CONFIGURATION VARIABLES
+;;
+;;
 
 (defgroup prover-config nil
   "Configuration of Proof General for the prover in use."
@@ -59,9 +102,10 @@ from the name given in proof-internal-assistant-table."
 
 
 
+
 
 ;;
-;; 0. The major modes used by Proof General.
+;; 2. The major modes used by Proof General.
 ;;
 
 (defcustom proof-mode-for-shell nil
@@ -85,8 +129,9 @@ Suggestion: this can be set in proof-pre-shell-start-hook."
 
 
 
+
 ;;
-;; 1. Configuration for menus, user-level commands, etc.
+;; 3. Configuration for menus, user-level commands, etc.
 ;;
 
 (defcustom proof-www-home-page ""
@@ -136,7 +181,7 @@ This variable should be set before requiring proof.el"
 
 
 ;;
-;; 2. Configuration for proof script mode
+;; 4. Configuration for proof script mode
 ;;
 
 ;;
@@ -289,7 +334,7 @@ assistant, for example, to switch to a new theory."
 
 
 ;;
-;;  3. Configuration for proof shell	                            
+;;  5. Configuration for proof shell	                            
 ;;
 ;; The variables in this section concern the proof shell mode.
 ;; The first group of variables are hooks invoked at various points.
@@ -308,7 +353,7 @@ assistant, for example, to switch to a new theory."
 
 
 ;; 
-;; 3a. commands
+;; 5a. commands
 ;;
 
 (defcustom proof-prog-name nil
@@ -329,7 +374,7 @@ Suggestion: this can be set in proof-pre-shell-start-hook."
 
 
 ;;
-;; 3b. Regexp variables for matching output from proof process.
+;; 5b. Regexp variables for matching output from proof process.
 ;;
 
 (defcustom proof-shell-prompt-pattern nil 
@@ -406,7 +451,7 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
   :group 'proof-shell)
 
 ;;
-;; 3c. hooks 
+;; 5c. hooks 
 ;;
 
 (defcustom proof-shell-insert-hook nil 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 453b18db..3a799252 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -9,6 +9,8 @@
 ;; $Id$
 ;;
 
+(require 'proof-config)
+
 ;;
 ;;  Internal variables used by script mode
 ;;
@@ -316,6 +318,89 @@ buffer is closed off atomically."
 	      (not buffer)
 	      (proof-mark-buffer-atomic buffer))))))
 
+;; NEW utility functions, use them!
+
+(defun proof-locked-region-full-p ()
+  "Non-nil if the locked region covers all the buffer's non-whitespace.
+Should be called from a proof script buffer."
+  (save-excursion
+    (goto-char (point-max))
+    (skip-chars-backward " \t\n")
+    (>= (proof-unprocessed-begin) (point))))
+
+(defun proof-locked-region-empty-p ()
+  "Non-nil if the locked region is empty.
+Should be called from a proof script buffer."
+  (eq (proof-unprocessed-begin) (point-min)))
+
+
+(defun proof-check-process-available (&optional relaxed)
+  "Adjust internal variables for scripting of current buffer.
+
+Signals an error if current buffer is not a proof script or if the
+proof process is not idle. If RELAXED is set, nothing more is done. No
+changes are necessary if the current buffer is already in Scripting
+minor mode. Otherwise, the current buffer will become the current
+scripting buffer provided the current scripting buffer has either no
+locked region or everything in it has been processed."
+  (proof-start-shell)
+  (cond
+   ((not (or relaxed (eq proof-buffer-type 'script)))
+    (error "Must be running in a script buffer"))
+   (proof-shell-busy (error "Proof Process Busy!"))
+   (relaxed ())			;exit cond
+
+   ;; No buffer is in Scripting minor mode.
+   ;; We assume the setup is done somewhere else
+   ;; so this should never happen
+   ((null proof-script-buffer-list) (assert nil))
+
+   ;; The current buffer is in Scripting minor mode
+   ;; so there's nothing to do
+   ((equal (current-buffer) (car proof-script-buffer-list)))
+
+   (t
+    (let ((script-buffer (car proof-script-buffer-list))
+	  (current-buffer (current-buffer)))
+      (save-excursion
+	(set-buffer script-buffer)
+	;; We only allow switching of the Scripting buffer if the
+	;; locked region is either empty or full for all buffers.
+	;; Here we check the current Scripting buffer's status.
+	(if (proof-locked-region-full-p)
+	    ;; We're switching from a buffer which has been
+	    ;; completely processed.  Make sure that it's
+	    ;; registered on the included files list, in
+	    ;; case it has been processed piecemeal.
+	    (if buffer-file-name
+		(proof-register-possibly-new-processed-file 
+		 buffer-file-name)))
+
+	(if (or 
+	     (proof-locked-region-empty-p)
+	     (proof-locked-region-full-p))
+	    ;; we are changing the scripting buffer
+	    (progn
+	      (setq proof-active-buffer-fake-minor-mode nil)
+	      (set-buffer current-buffer)
+	      
+	      ;; does the current buffer contain locked regions already?
+	      (if (member current-buffer proof-script-buffer-list)
+		  (setq proof-script-buffer-list
+			(remove current-buffer proof-script-buffer-list))
+		(proof-init-segmentation))
+	      (setq proof-script-buffer-list
+		    (cons current-buffer proof-script-buffer-list))
+	      (setq proof-active-buffer-fake-minor-mode t)
+	      (run-hooks 'proof-activate-scripting-hook))
+	  ;; Locked region covers only part of the buffer
+	  ;; FIXME da: ponder alternative of trying to complete rest
+	  ;; of current scripting buffer?
+	  (error "Cannot deal with two unfinished script buffers!")))))))
+
+
+
+
 
 
 
@@ -646,15 +731,16 @@ Assumes that point is at the end of a command."
 (defun proof-assert-until-point
   (&optional unclosed-comment-fun ignore-proof-process-p)
   "Process the region from the end of the locked-region until point.
-   Default action if inside a comment is just to go until the start of
-   the comment. If you want something different, put it inside
-   unclosed-comment-fun. If ignore-proof-process-p is set, no commands
-   will be added to the queue."
+Default action if inside a comment is just process as far as the start of
+the comment. If you want something different, put it inside
+unclosed-comment-fun. If ignore-proof-process-p is set, no commands
+will be added to the queue."
   (interactive)
   (let ((pt (point))
 	(crowbar (or ignore-proof-process-p (proof-check-process-available)))
 	semis)
     (save-excursion
+      ;; Give error if no non-whitespace between point and end of locked region.
       (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t))
 	  (progn (goto-char pt)
 		 (error "I don't know what I should be doing in this buffer!")))
@@ -689,10 +775,9 @@ Assumes that point is at the end of a command."
   (&optional unclosed-comment-fun ignore-proof-process-p
 	     dont-move-forward for-new-command)
   "Process until the end of the next unprocessed command after point.
-If inside a comment, just to go the start of
-the comment.  If you want something different, put it inside
-UNCLOSED-COMMENT-FUN. If IGNORE-PROOF-PROCESS-P is set, no commands
-will be added to the queue.
+If inside a comment, just process until the start of the comment.  
+If you want something different, put it inside UNCLOSED-COMMENT-FUN. 
+If IGNORE-PROOF-PROCESS-P is set, no commands will be added to the queue.
 Afterwards, move forward to near the next command afterwards, unless
 DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil,
 a space or newline will be inserted automatically."
@@ -700,6 +785,8 @@ a space or newline will be inserted automatically."
   (let ((pt (point))
 	(crowbar (or ignore-proof-process-p (proof-check-process-available)))
 	semis)
+    (if (proof-locked-region-full-p)
+	(error "Locked region is full, no more commands to do!"))
     (save-excursion
       ;; CHANGE from old proof-assert-until-point: don't bother check
       ;; for non-whitespace between locked region and point.
@@ -711,12 +798,10 @@ a space or newline will be inserted automatically."
     ;;	  (progn (goto-char pt)
     ;;       (error "I don't know what I should be doing in this buffer!")))
     ;; (setq semis (proof-segment-up-to (point))))
-    (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis)))
+    (if (and unclosed-comment-fun (eq 'unclosed-comment (car-safe semis)))
 	(funcall unclosed-comment-fun)
-      (if (eq 'unclosed-comment (car semis))
-	  ;; CHANGE: if inside a comment, do as the documentation
-	  ;; suggests.
-	  (setq semis nil))
+      (if (eq 'unclosed-comment (car-safe semis))
+	  (setq semis (cdr semis)))
       (if (and (not ignore-proof-process-p) (not crowbar) (null semis))
 	  (error "I don't know what I should be doing in this buffer!"))
       (goto-char (nth 2 (car semis)))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 1657b049..eab8dc17 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -9,6 +9,8 @@
 ;; $Id$
 ;;
 
+(require 'proof-config)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;  Starting and stopping the proof-system shell                    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -536,75 +538,6 @@ assistant."
       (incf i)))
   (save-excursion (proof-shell-insert string)))
 
-(defun proof-check-process-available (&optional relaxed)
-  "Adjust internal variables for scripting of current buffer.
-
-Signals an error if current buffer is not a proof script or if the
-proof process is not idle. If RELAXED is set, nothing more is done. No
-changes are necessary if the current buffer is already in Scripting
-minor mode. Otherwise, the current buffer will become the current
-scripting buffer provided the current scripting buffer has either no
-locked region or everything in it has been processed."
-  (proof-start-shell)
-  (cond
-   ((not (or relaxed (eq proof-buffer-type 'script)))
-    (error "Must be running in a script buffer"))
-   (proof-shell-busy (error "Proof Process Busy!"))
-   (relaxed ())			;exit cond
-
-   ;; No buffer is in Scripting minor mode.
-   ;; We assume the setup is done somewhere else
-   ;; so this should never happen
-   ((null proof-script-buffer-list) (assert nil))
-
-   ;; The current buffer is in Scripting minor mode
-   ;; so there's nothing to do
-   ((equal (current-buffer) (car proof-script-buffer-list)))
-
-   (t
-    (let ((script-buffer (car proof-script-buffer-list))
-	  (current-buffer (current-buffer)))
-      (save-excursion
-	(set-buffer script-buffer)
-	;; We only allow switching of the Scripting buffer if the
-	;; locked region is either empty or full for all buffers.
-	;; Here we check the current Scripting buffer's status.
-	(let
-	    ((locked-is-empty (eq (proof-unprocessed-begin) (point-min)))
-	     (locked-is-full  (progn
-				(goto-char (point-max))
-				(skip-chars-backward " \t\n")
-				(>= (proof-unprocessed-begin) (point)))))
-	  (if locked-is-full
-	      ;; We're switching from a buffer which has been
-	      ;; completely processed.  Make sure that it's
-	      ;; registered on the included files list, in
-	      ;; case it has been processed piecemeal.
-	      (if buffer-file-name
-		  (proof-register-possibly-new-processed-file 
-		   buffer-file-name)))
-
-	  (if (or locked-is-full locked-is-empty)
-	      ;; we are changing the scripting buffer
-	      (progn
-		(setq proof-active-buffer-fake-minor-mode nil)
-		(set-buffer current-buffer)
-
-		;; does the current buffer contain locked regions already?
-		(if (member current-buffer proof-script-buffer-list)
-		    (setq proof-script-buffer-list
-			  (remove current-buffer proof-script-buffer-list))
-		  (proof-init-segmentation))
-		(setq proof-script-buffer-list
-		      (cons current-buffer proof-script-buffer-list))
-		(setq proof-active-buffer-fake-minor-mode t)
-		(run-hooks 'proof-activate-scripting-hook))
-	    ;; Locked region covers only part of the buffer
-	    ;; FIXME da: ponder alternative of trying to complete rest
-	    ;; of current scripting buffer?
-	    (error "Cannot deal with two unfinished script buffers!"))))))))
-
-
 (defun proof-grab-lock (&optional relaxed)
   (proof-start-shell)
   (proof-check-process-available relaxed)
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 31a70e9d..2795ea18 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -10,6 +10,8 @@
 ;; Toolbar is just for scripting buffer at  the moment.
 ;;
 
+(require 'proof-config)
+
 (defcustom proof-toolbar-wanted t
   "*Whether to use toolbar in proof mode."
   :type 'boolean
diff --git a/todo b/todo
index bedf88dc..8dc8b60e 100644
--- a/todo
+++ b/todo
@@ -14,6 +14,8 @@ X (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
+A* Fixup for clean byte compile now that proof.el has been split.
+
 A* Fixup multiple files -- needs debugging.
 
    1. mark atomic makes some assumption about non-comment commands in