Continuing mods for cleaner byte compile

3 files changed, 110 insertions, 85 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index d3e1066c..207e06d7 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -385,48 +385,9 @@ This is used to handle nested goals allowed by some provers."
   :type 'function
   :group 'proof-script)
 
-(defcustom pbp-change-goal nil
-  "Command to change to the goal %s"
-  :type 'string
-  :group 'prover-config)
-
-(defcustom proof-shell-process-output-system-specific nil
-  "Set this variable to handle system specific output.
-Errors, start of proofs, abortions of proofs and completions of
-proofs are recognised in the function `proof-shell-process-output'.
-All other output from the proof engine is simply reported to the
-user in the RESPONSE buffer.
 
-To catch further special cases, set this variable to a pair of
-functions '(condf . actf). Both are given (cmd string) as arguments.
-`cmd' is a string containing the currently processed command.
-`string' is the response from the proof system. To change the
-behaviour of `proof-shell-process-output', (condf cmd string) must
-return a non-nil value. Then (actf cmd string) is invoked. See the
-documentation of `proof-shell-process-output' for the required
-output format."
-  :type '(cons (function function))
-  :group 'prover-config)
-
-(defcustom proof-activate-scripting-hook nil
-  "Hook run when a buffer is switched into scripting mode.
-The current buffer will be the newly active scripting buffer.
 
-This hook may be useful for synchronizing with the proof
-assistant, for example, to switch to a new theory."
-  :type '(repeat function)
-  :group 'prover-config)
 
-; FIXME: this could be used to replace eager-annotation-start and end.
-;(defcustom proof-shell-urgent-message-regexp nil
-;  "Regexp matching messages to be dealt with during process output.
-;Normally, process output is only dealt with when two successive
-;prompts are seen.  But Proof General can also process 'urgent' messages,
-;for example 'loading file...' or 'warning...' while output
-;before the second prompt is seen. 
-;Set to nil to disable this feature."
-;  :type '(choice nil regexp)
-;  :group 'prover-config)
 
 
 
@@ -563,6 +524,31 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'."
   :type 'regexp
   :group 'proof-shell)
 
+(defcustom proof-shell-eager-annotation-start nil
+  "Eager annotation field start.  A regular expression or nil.
+An eager annotation indicates to Emacs that some following output
+should be displayed immediately and not accumulated for parsing.
+Set to nil to disable this feature.
+
+The default value is \"\n\" to match up to the end of the line."
+  :type '(choice regexp nil)
+  :group 'proof-shell)
+
+(defcustom proof-shell-eager-annotation-end "\n"
+  "Eager annotation field end.  A regular expression or nil.
+An eager annotation indicates to Emacs that some following output
+should be displayed immediately and not accumulated for parsing.
+The default value is \"\n\" to match up to the end of the line."
+  :type '(choice regexp nil)
+  :group 'proof-shell)
+
+(defcustom proof-shell-assumption-regexp nil
+  "A regular expression matching the name of assumptions."
+  :type '(choice regexp nil)
+  :group 'proof-shell)
+
+
+
 ;;
 ;; 5c. hooks 
 ;;
@@ -635,6 +621,7 @@ data triggered by `proof-shell-retract-files-regexp'."
 
 
 
+
 
 ;;
 ;; 6. Global constants
@@ -669,6 +656,89 @@ where `k' is a keybinding (vector) and `f' the designated function."
 
 
 
+;;; 
+;;; FIXME: unsorted below here
+;;;
+
+(defcustom pbp-change-goal nil
+  "Command to change to the goal %s"
+  :type 'string
+  :group 'prover-config)
+
+(defcustom proof-shell-process-output-system-specific nil
+  "Set this variable to handle system specific output.
+Errors, start of proofs, abortions of proofs and completions of
+proofs are recognised in the function `proof-shell-process-output'.
+All other output from the proof engine is simply reported to the
+user in the RESPONSE buffer.
+
+To catch further special cases, set this variable to a pair of
+functions '(condf . actf). Both are given (cmd string) as arguments.
+`cmd' is a string containing the currently processed command.
+`string' is the response from the proof system. To change the
+behaviour of `proof-shell-process-output', (condf cmd string) must
+return a non-nil value. Then (actf cmd string) is invoked. See the
+documentation of `proof-shell-process-output' for the required
+output format."
+  :type '(cons (function function))
+  :group 'prover-config)
+
+(defcustom proof-activate-scripting-hook nil
+  "Hook run when a buffer is switched into scripting mode.
+The current buffer will be the newly active scripting buffer.
+
+This hook may be useful for synchronizing with the proof
+assistant, for example, to switch to a new theory."
+  :type '(repeat function)
+  :group 'prover-config)
+
+
+
+
+;;
+;; Proof script indentation
+;;
+
+;; FIXME: document this junk
+(defcustom proof-stack-to-indent nil
+  "Prover-specific code for indentation."
+  :type 'sexp
+  :group 'proof-script)
+
+(defcustom proof-parse-indent nil
+  "Proof-assistant specific function for parsing characters for
+  indentation which is invoked in `proof-parse-to-point.'. Must be a
+  function taking two arguments, a character (the current character)
+  and a stack reflecting indentation, and must return a stack. The
+  stack is a list of the form (c . p) where `c' is a character
+  representing the type of indentation and `p' records the column for
+  indentation. The generic `proof-parse-to-point.' function supports
+  parentheses and commands. It represents these with the characters
+  `?\(', `?\[' and `proof-terminal-char'. "
+  :type 'sexp
+  :group 'proof-script)
+
+
+;;
+;; More shell junk to sort out [maybe for pbp]
+;;
+
+(defvar proof-shell-first-special-char nil "where the specials start")
+(defvar proof-shell-goal-char nil "goal mark")
+(defvar proof-shell-start-char nil "annotation start")
+(defvar proof-shell-end-char nil "annotation end")
+(defvar proof-shell-field-char nil "annotated field end")
+
+
+(defvar proof-shell-goal-regexp nil
+  "A regular expression matching the identifier of a goal.")
+
+(defvar proof-shell-noise-regexp nil
+  "Unwanted information output from the proof process within
+  `proof-start-goals-regexp' and `proof-end-goals-regexp'.")
+
+(defvar proof-analyse-using-stack nil
+  "Are annotations sent by proof assistant local or global")
 
 
 ;; End of proof-config.el
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index 8506cf38..4fa130e7 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -23,20 +23,6 @@
 ;;;
 
 
-(defvar proof-stack-to-indent nil
-  "Prover-specific code for indentation.")
-
-(defvar proof-parse-indent nil
-  "Proof-assistant specific function for parsing characters for
-  indentation which is invoked in `proof-parse-to-point.'. Must be a
-  function taking two arguments, a character (the current character)
-  and a stack reflecting indentation, and must return a stack. The
-  stack is a list of the form (c . p) where `c' is a character
-  representing the type of indentation and `p' records the column for
-  indentation. The generic `proof-parse-to-point.' function supports
-  parentheses and commands. It represents these with the characters
-  `?\(', `?\[' and `proof-terminal-char'. ")
-
 ;; This is quite different from sml-mode, but borrows some bits of
 ;; code.  It's quite a lot less general, but works with nested
 ;; comments.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 476145b7..fac7305b 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -36,6 +36,7 @@
 	    proof-restart-buffers
 	    proof-dont-show-annotations)))
 
+;;
 ;; Internal variables used by shell mode
 ;;
 
@@ -304,39 +305,10 @@ Does nothing if proof assistant is already running."
 ;;          Turning annotated output into pbp goal set              ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defvar proof-shell-first-special-char nil "where the specials start")
-(defvar proof-shell-goal-char nil "goal mark")
-(defvar proof-shell-start-char nil "annotation start")
-(defvar proof-shell-end-char nil "annotation end")
-(defvar proof-shell-field-char nil "annotated field end")
-
-(defvar proof-shell-eager-annotation-start nil
-  "Eager annotation field start.  A regular expression or nil.
-An eager annotation indicates to Emacs that some following output
-should be displayed immediately and not accumulated for parsing.
-Set to nil to disable this feature.
-
-The default value is \"\n\" to match up to the end of the line.")
-
-(defvar proof-shell-eager-annotation-end "\n"
-  "Eager annotation field end.  A regular expression or nil.
-An eager annotation indicates to Emacs that some following output
-should be displayed immediately and not accumulated for parsing.
-The default value is \"\n\" to match up to the end of the line.")
-
-(defvar proof-shell-assumption-regexp nil
-  "A regular expression matching the name of assumptions.")
-
 ;; FIXME da: where is this variable used?  
 ;;	      dropped in favour of goal-char?
 ;; Answer: this is used in *specific* modes, see e.g.
 ;; lego-goal-hyp.  This stuff needs making more generic.
-(defvar proof-shell-goal-regexp nil
-  "A regular expression matching the identifier of a goal.")
-
-(defvar proof-shell-noise-regexp nil
-  "Unwanted information output from the proof process within
-  `proof-start-goals-regexp' and `proof-end-goals-regexp'.")
 
 (defun pbp-make-top-span (start end)
   (let (span name)
@@ -368,9 +340,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-analyse-using-stack nil
-  "Are annotations sent by proof assistant local or global")
-
 (defun proof-shell-analyse-structure (string)
   (save-excursion
     (let* ((ip 0) (op 0) ap (l (length string))