Many rearrangements for compatibility, efficient/correct compilation, namespaces fixes.

pre-shell-start-hook: remove this, use default names for modes
proof-compat: simplify architecture flags, use standard (featurep 'xemacs).

1 files changed, 143 insertions, 169 deletions

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 1cb372fb..89f0b433 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -1,21 +1,29 @@
-;; proof-utils.el   Proof General utility functions
+;; proof-utils.el --- Proof General utility functions and macros
 ;;
-;; Copyright (C) 1998-2002 LFCS Edinburgh. 
+;; Copyright (C) 1998-2002 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
 ;; $Id$
 ;;
-;;
+;;; Commentary:
+;; 
 ;; Loading note: this file is required immediately from proof.el, so
-;; no autoloads are used here.
+;; no autoloads cookies are added here. To expand macros during
+;; compilation, use (eval-when-compile (require 'proof-utils)).  
+;; This needs care: it is safe for e.g., deflocal, but not for
+;; macros which evaluate proof-assistant symbol, e.g. proof-ass,
+;; unless proof-ready-for-assistant has been run.
+;;
 
-(require 'proof-compat)			;; for pg-defface-window-systems
+(require 'proof-site)			; basic vars
+(require 'proof-compat)		        ; for pg-defface-window-systems
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Handy macros
 
+;;; Code:
 (defmacro deflocal (var value &optional docstring)
   "Define a buffer local variable VAR with default value VALUE."
  `(progn
@@ -29,6 +37,9 @@
        (with-current-buffer ,buf
 	 ,@body)))
 
+(deflocal proof-buffer-type nil
+  "Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.")
+
 ;; Slightly specialized version of above.  This is used in commands
 ;; which work from different PG buffers (goals, response), typically
 ;; bound to toolbar commands.
@@ -53,29 +64,13 @@ Return nil if not a script buffer or if no active scripting buffer."
  `(intern (concat (symbol-name proof-assistant-symbol) "-" ,string)))
 
 
-(defun proof-try-require (symbol)
+(defsubst proof-try-require (symbol)
   "Try requiring SYMBOL.  No error if the file for SYMBOL isn't found."
   (condition-case ()
       (require symbol)
     (file-error nil))
   (featurep symbol))
 
-(defmacro proof-face-specs (bl bd ow)
-  "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
-  `(append
-    (apply 'append
-     (mapcar 
-     (lambda (ty) (list
-		     (list (list (list 'type ty) '(class color)
-			   (list 'background 'light))
-			   (quote ,bl))
-		     (list (list (list 'type ty) '(class color)
-				 (list 'background 'dark))
-			   (quote ,bd))))
-     ;; NOTE: see proof-compat.el for possible window-system values
-     pg-defface-window-systems))
-    (list (list t (quote ,ow)))))
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -102,39 +97,6 @@ Return nil if not a script buffer or if no active scripting buffer."
    buffers))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Function for taking action when dynamically adjusting customize values
-;;
-(defun proof-set-value (sym value)
-  "Set a customize variable using set-default and a function.
-We first call `set-default' to set SYM to VALUE.
-Then if there is a function SYM (i.e. with the same name as the
-variable SYM), it is called to take some dynamic action for the new
-setting.  
-
-If there is no function SYM, we try stripping 
-proof-assistant-symbol and adding \"proof-\" instead to get
-a function name.  This extends proof-set-value to work with
-generic individual settings.
-
-The dynamic action call only happens when values *change*: as an
-approximation we test whether proof-config is fully-loaded yet."
-  (set-default sym value)
-  (if (featurep 'proof-config)
-      (if (fboundp sym)
-	  (funcall sym)
-	(if (> (length (symbol-name sym)) 
-	       (+ 3 (length (symbol-name proof-assistant-symbol))))
-	    (let ((generic  
-		   (intern
-		    (concat "proof"
-			    (substring (symbol-name sym)
-				       (length (symbol-name
-						proof-assistant-symbol)))))))
-	      (if (fboundp generic)
-		  (funcall generic)))))))
-
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -154,7 +116,7 @@ approximation we test whether proof-config is fully-loaded yet."
 ;; previous approach.  It is also a big change to move all settings.
 ;;
 ;; NB: this mechanism is work in progress in 3.2.  It will
-;; be expanded, although we may leave most low-level 
+;; be expanded, although we may leave most low-level
 ;; settings to use the current mechanism.
 ;;
 ;; Notes:
@@ -163,40 +125,43 @@ approximation we test whether proof-config is fully-loaded yet."
 ;;
 ;; (proof-ass name)   or (proof-assistant-name)
 ;;
-;; Later is more efficient, though defining function
-;; for each setting seems wasteful?
-
-(defun proof-ass-symv (sym)
-  "Return the symbol for SYM for the current prover.  SYM is evaluated."
-  (intern (concat (symbol-name proof-assistant-symbol) "-" 
-		  (symbol-name sym))))
 
 (defmacro proof-ass-sym (sym)
-  "Return the symbol for SYM for the current prover.  SYM not evaluated."
-  `(proof-ass-symv (quote ,sym)))
+  "Return the symbol for SYM for the current prover.  SYM not evaluated.
+This macro should only be called once a specific prover is known."
+  `(intern (concat (symbol-name proof-assistant-symbol) "-"
+		   (symbol-name ',sym))))
+
+(defmacro proof-ass-symv (sym)
+  "Return the symbol for SYM for the current prover.  SYM evaluated.
+This macro should only be invoked once a specific prover is engaged."
+  `(intern (concat (symbol-name proof-assistant-symbol) "-"
+		   (symbol-name ,sym))))
+
+(defmacro proof-ass (sym)
+  "Return the value for SYM for the current prover.
+This macro should only be invoked once a specific prover is engaged."
+  `(symbol-value (intern (concat (symbol-name proof-assistant-symbol) "-"
+				 (symbol-name ',sym)))))
 
 (defun proof-defpgcustom-fn (sym args)
-  "Define a new customization variable <PA>-sym for the current proof assistant.
+  "Define a new customization variable <PA>-sym for current proof assistant.
 Helper for macro `defpgcustom'."
   (let ((specific-var (proof-ass-symv sym))
-	(generic-var  (intern (concat "proof-assistant-" (symbol-name sym)))))
+	 (generic-var  (intern (concat "proof-assistant-" (symbol-name sym)))))
     (eval
-     `(defcustom ,specific-var 
-	,@args
-	;; FIXME: would be nicer to grab group from @args here and
-	;; prefix it automatically.  For now, default to internals
-	;; setting for PA.
-	;; FIXME 2: would also be nice to grab docstring from args
-	;; and allow substitution for prover name, etc.  A bit too 
-	;; fancy perhaps!
-	:group ,(quote proof-assistant-internals-cusgrp)))
+     `(defcustom ,specific-var
+       ,@args
+       ;; We could grab :group from @args and prefix it.
+       :group ,(quote proof-assistant-internals-cusgrp)))
     ;; For functions, we could simply use defalias.  Unfortunately there
     ;; is nothing similar for values, so we define a new set/get function.
     (eval
-     `(defun ,generic-var (&optional newval) 
-	,(concat "Set or get value of " (symbol-name sym) " for current proof assistant.
+     `(defun ,generic-var (&optional newval)
+	,(concat "Set or get value of " (symbol-name sym) 
+		 " for current proof assistant.
 If NEWVAL is present, set the variable, otherwise return its current value.")
-	(if newval 
+	(if newval
 	    (setq ,specific-var newval)
 	  ,specific-var)))))
 
@@ -208,24 +173,21 @@ If NEWVAL is present, set the variable, otherwise return its current value.")
 
 (defmacro defpgcustom (sym &rest args)
   "Define a new customization variable <PA>-SYM for the current proof assistant.
-The function proof-assistant-<SYM> is also defined, which can be used in the 
+The function proof-assistant-<SYM> is also defined, which can be used in the
 generic portion of Proof General to set and retrieve the value for the current p.a.
 Arguments as for `defcustom', which see.
 
 Usage: (defpgcustom SYM &rest ARGS)."
   `(proof-defpgcustom-fn (quote ,sym) (quote ,args)))
 
-(defmacro proof-ass (sym)
-  "Return the value for SYM for the current prover."
-  ;; (eval `(proof-ass-sym ,sym))
-  `(symbol-value (proof-ass-symv ',sym))) ;; [Stefan Monnier]
+
 
 (defun proof-defpgdefault-fn (sym value)
   "Helper for `defpgdefault', which see.  SYM and VALUE are evaluated."
   ;; NB: we need this because nothing in customize library seems to do
   ;; the right thing.
   (let ((symbol  (proof-ass-symv sym)))
-    (set-default symbol 
+    (set-default symbol
 		 (cond
 		  ;; Use saved value if it's set
 		  ((get symbol 'saved-value)
@@ -250,10 +212,18 @@ Usage: (defpgdefault SYM VALUE)"
   `(defun ,(proof-ass-symv name) ,arglist
      ,@args))
 
-
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; End macros
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Evaluation once proof assistant is known
+;; 
+
+(defmacro proof-eval-when-ready-for-assistant (&rest body)
+  "Evaluate BODY once the proof assistant is determined (possibly now)."
+  `(if (and (boundp 'proof-assistant-symbol) proof-assistant-symbol)
+       (progn ,@body)
+     (add-hook 'proof-ready-for-assistant-hook (lambda () ,@body))))
+    
+
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -285,7 +255,7 @@ Usage: (defpgdefault SYM VALUE)"
 (defun proof-buffers-in-mode (mode &optional buflist)
   "Return a list of the buffers in the buffer list in major-mode MODE.
 Restrict to BUFLIST if it's set."
-  (let ((bufs-left (or buflist (buffer-list))) 
+  (let ((bufs-left (or buflist (buffer-list)))
 	bufs-got)
     (dolist (buf bufs-left bufs-got)
       (if (with-current-buffer buf (eq mode major-mode))
@@ -299,7 +269,7 @@ Restrict to BUFLIST if it's set."
 (defun pg-save-from-death ()
   "Prevent this associated buffer from being killed: merely erase it.
 A hook function for `kill-buffer-hook'.
-This is a fairly crude and not-entirely-robust way to prevent the 
+This is a fairly crude and not-entirely-robust way to prevent the
 user accidently killing an associated buffer."
   (if (and (proof-shell-live-buffer) proof-buffer-type)
       (progn
@@ -332,10 +302,10 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
 
 ;; Notes:
 ;;
-;; * Various mechanisms for setting defaults, different between 
+;; * Various mechanisms for setting defaults, different between
 ;;   Emacsen.  Old method(?) was to set "blah-mode-font-lock-keywords"
 ;;   and copy it into "font-lock-keywords" to engage font-lock.
-;;   Present method for XEmacs is to put a 'font-lock-defaults 
+;;   Present method for XEmacs is to put a 'font-lock-defaults
 ;;   property on the major-mode symbol, or use font-lock-defaults
 ;;   buffer local variable.  We use the latter.
 ;;
@@ -391,14 +361,14 @@ font-lock-mode."
     ;; 11.12.01: Emacs 21 is very eager about turning on font
     ;; lock and has hooks all over the place to do it.  To make
     ;; sure it doesn't happen we have to eradicate all sense of
-    ;; having any fontification ability.  
+    ;; having any fontification ability.
     (proof-font-lock-clear-font-lock-vars)
     ;; In fact, this still leaves font-lock switched on! But
     ;; hopefully in a useless way.  XEmacs has better control
     ;; over which modes not to enable it for (although annoying
     ;; that it's a custom setting)
-    (if proof-running-on-XEmacs
-	(setq font-lock-mode-disable-list 
+    (if (featurep 'xemacs)
+	(setq font-lock-mode-disable-list
 	      (cons major-mode font-lock-mode-disable-list)))))
 
 (defun proof-font-lock-clear-font-lock-vars ()
@@ -413,9 +383,9 @@ font-lock-mode."
   )
 
 (defun proof-font-lock-set-font-lock-vars ()
-  (setq font-lock-defaults 
-	`(proof-font-lock-keywords 
-	  nil 
+  (setq font-lock-defaults
+	`(proof-font-lock-keywords
+	  nil
 	  ,proof-font-lock-keywords-case-fold-search))
   (setq font-lock-keywords proof-font-lock-keywords))
 
@@ -442,10 +412,10 @@ Returns new END value."
 	(proof-font-lock-set-font-lock-vars)
 
 	;; Yukky hacks to immorally interface with font-lock
-	(unless proof-running-on-XEmacs
+	(unless (featurep 'xemacs)
 	  (font-lock-set-defaults))
 	(let ((font-lock-keywords proof-font-lock-keywords))
-	  (if (and proof-running-on-XEmacs
+	  (if (and (featurep 'xemacs)
 		   (>= emacs-major-version 21)
 		   (>= emacs-minor-version 4)
 		   (not font-lock-cache-position))
@@ -481,7 +451,7 @@ Returns new END value."
   "Remove special characters in region.  Default to whole buffer.
 Leave point at END."
   (save-restriction
-    (if (and start end) 
+    (if (and start end)
 	(narrow-to-region start end))
     (goto-char (or start (point-min)))
     (while (re-search-forward pg-special-char-regexp end t)
@@ -518,7 +488,7 @@ NB: may change the selected window."
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
     ;; THEN find somewhere nice to display it
-	  (if (and 
+	  (if (and
 	     ;; If we're in two-window mode and already displaying a
 	     ;; script/response/goals, try to just switch the buffer
 	     ;; instead of calling display-buffer which alters sizes.
@@ -530,18 +500,18 @@ NB: may change the selected window."
 		   ;; NB: 3.5: added rest of assoc'd buffers here
 		   (cons proof-script-buffer (proof-associated-buffers))))
 	    (if (eq (selected-window) (minibuffer-window))
-		;; 17.8.01: avoid switching the minibuffer's contents 
+		;; 17.8.01: avoid switching the minibuffer's contents
 		;; -- terrrible confusion -- use next-window after
 		;; script buffer instead.
 		;; (another hack which is mostly right)
-		(set-window-buffer 
-		 (next-window 
+		(set-window-buffer
+		 (next-window
 		  (car-safe (get-buffer-window-list proof-script-buffer))
 		  'ignoreminibuf) buffer)
 	      (if (eq (window-buffer (next-window nil 'ignoreminibuf))
-		      proof-script-buffer) 
+		      proof-script-buffer)
 		  ;; switch this window
-		  (set-window-buffer (selected-window) buffer) 
+		  (set-window-buffer (selected-window) buffer)
 		;; switch other window
 		(set-window-buffer (next-window nil 'ignoreminibuf) buffer)))
 	    ;; o/w: call display buffer to configure windows nicely.
@@ -565,7 +535,7 @@ NB: may change the selected window."
 
 (defun proof-display-and-keep-buffer (buffer &optional pos)
   "Display BUFFER and make window according to display mode.
-If optional POS is present, will set point to POS.  
+If optional POS is present, will set point to POS.
 Otherwise move point to the end of the buffer.
 Ensure that point is visible in window."
   (save-excursion
@@ -648,7 +618,7 @@ If proof-general-debug is nil, do nothing."
   "Switch to or display buffer BUF in other window unless already displayed.
 If optional arg NOSELECT is true, don't switch, only display it.
 No action if BUF is nil or killed."
-  ;; Maybe this needs to be more sophisticated, using 
+  ;; Maybe this needs to be more sophisticated, using
   ;; proof-display-and-keep-buffer ?
   (and (buffer-live-p buf)
        (unless (eq buf (window-buffer (selected-window)))
@@ -667,11 +637,11 @@ No action if BUF is nil or killed."
 ;; Originally based on `shrink-window-if-larger-than-buffer', which
 ;; has a pretty wierd implementation.
 ;; TODO: desirable improvements would be to add some crafty history based
-;; on user resize-events.  E.g. user resizes window, that becomes the 
+;; on user resize-events.  E.g. user resizes window, that becomes the
 ;; new maximum size.
 ;; FIXME: GNU Emacs has useful "window-size-fixed" which we use
 ;; HOWEVER, it's still not quite the right thing, it seems to me.
-;; We'd like to specifiy a *minimum size* for a given buffer, 
+;; We'd like to specifiy a *minimum size* for a given buffer,
 ;; not a maximum.  With a frame split with just goals/response
 ;; we'd still get resize errors here using window-size-fixed.
 ;; FIXME: shrink-to-fit doesn't really work in three-buffer mode,
@@ -782,12 +752,12 @@ or if the window is the only window of its frame."
   (interactive)
   (require 'reporter)
   (let
-      ((reporter-prompt-for-summary-p 
+      ((reporter-prompt-for-summary-p
 	"(Very) brief summary of problem or suggestion: "))
     (reporter-submit-bug-report
      "da+pg-bugs@inf.ed.ac.uk"
-     "Proof General" 
-     (list 'proof-general-version 'proof-assistant 
+     "Proof General"
+     (list 'proof-general-version 'proof-assistant
 	   'x-symbol-version)
      nil nil
      "*** Proof General now uses Trac for project management and bug reporting, please go to:
@@ -798,13 +768,13 @@ or if the window is the only window of its frame."
 *** To report a bug, either register yourself as a user, or use the generic account
 *** username \"pgemacs\" with password \"pgemacs\"
 ***
-*** Please only continue with this email mechanism instead IF YOU REALLY MUST.  
-*** The address is not monitored very often and quite possibly will be ignored.  
+*** Please only continue with this email mechanism instead IF YOU REALLY MUST.
+*** The address is not monitored very often and quite possibly will be ignored.
 ***
 *** When reporting a bug, please include a small test case for us to repeat it.
 *** Please also check that it is not already covered in the BUGS or FAQ files that came with
-*** the distribution, or the latest versions at 
-***    http://proofgeneral.inf.ed.ac.uk/BUGS  and 
+*** the distribution, or the latest versions at
+***    http://proofgeneral.inf.ed.ac.uk/BUGS  and
 ***    http://proofgeneral.inf.ed.ac.uk/FAQ ")))
 
 
@@ -817,13 +787,13 @@ or if the window is the only window of its frame."
   "Define a function <VAR>-toggle for toggling a boolean customize setting VAR.
 Args as for the macro `proof-deftoggle', except will be evaluated."
   (eval
-   `(defun ,(if othername othername 
+   `(defun ,(if othername othername
 	      (intern (concat (symbol-name var) "-toggle"))) (arg)
 	      ,(concat "Toggle `" (symbol-name var) "'. With ARG, turn on iff ARG>0.
 This function simply uses customize-set-variable to set the variable.
 It was constructed with `proof-deftoggle-fn'.")
 	      (interactive "P")
-	      (customize-set-variable 
+	      (customize-set-variable
 	       (quote ,var)
 	       (if (null arg) (not ,var)
 		 (> (prefix-numeric-value arg) 0))))))
@@ -839,14 +809,14 @@ The name of the defined function is returned."
   "Define a function <VAR>-intset for setting an integer customize setting VAR.
 Args as for the macro `proof-defintset', except will be evaluated."
   (eval
-   `(defun ,(if othername othername 
+   `(defun ,(if othername othername
 	      (intern (concat (symbol-name var) "-intset"))) (arg)
 	      ,(concat "Set `" (symbol-name var) "' to ARG.
 This function simply uses customize-set-variable to set the variable.
 It was constructed with `proof-defintset-fn'.")
-	      (interactive (list 
-			    (read-number 
-			     (format "Value for %s (int, currently %s): " 
+	      (interactive (list
+			    (read-number
+			     (format "Value for %s (int, currently %s): "
 				     (symbol-name (quote ,var))
 				     (symbol-value (quote ,var))))))
 	      (customize-set-variable (quote ,var) arg))))
@@ -862,7 +832,7 @@ The name of the defined function is returned."
   "Define a function <VAR>-toggle for setting an integer customize setting VAR.
 Args as for the macro `proof-defstringset', except will be evaluated."
   (eval
-   `(defun ,(if othername othername 
+   `(defun ,(if othername othername
 	      (intern (concat (symbol-name var) "-stringset"))) (arg)
 	      ,(concat "Set `" (symbol-name var) "' to ARG.
 This function simply uses customize-set-variable to set the variable.
@@ -881,6 +851,49 @@ The name of the defined function is returned."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
+;;; Macris for defining user-level functions (previously in proof-menu.el)
+;;;
+
+
+(defmacro proof-defshortcut (fn string &optional key)
+  "Define shortcut function FN to insert STRING, optional keydef KEY.
+This is intended for defining proof assistant specific functions.
+STRING is inserted using `proof-insert', which see.
+KEY is added onto proof-assistant map."
+  `(progn
+     (if ,key
+	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
+     (defun ,fn ()
+       ,(concat "Shortcut command to insert "
+		(replace-in-string  string "\\\\" "\\\\=") ;; for substitute-command-keys
+		" into the current buffer.\nThis simply calls `proof-insert', which see.")
+       (interactive)
+       (proof-insert ,string))))
+
+(defmacro proof-definvisible (fn string &optional key)
+  "Define function FN to send STRING to proof assistant, optional keydef KEY.
+This is intended for defining proof assistant specific functions.
+STRING is sent using proof-shell-invisible-command, which see.
+STRING may be a string or a function which returns a string.
+KEY is added onto proof-assistant map."
+  `(progn
+     (if ,key
+	 (define-key (proof-ass keymap) (quote ,key) (quote ,fn)))
+     (defun ,fn ()
+       ,(concat "Command to send "
+		(if (stringp string)
+		    (replace-in-string
+		     string "\\\\" "\\\\=") ;; for substitute-command-keys
+		  "an instruction")
+		" to the proof assistant.")
+       (interactive)
+       ,(if (stringp string)
+	    (list 'proof-shell-invisible-command string)
+	  (list 'proof-shell-invisible-command (eval string))))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
 ;;; Interface to custom lib
 ;;;
 
@@ -889,8 +902,8 @@ The name of the defined function is returned."
   "Save custom vars VARIABLES."
   (dolist (symbol variables)
     (let ((value (get symbol 'customized-value)))
-      ;; This code from customize-save-customized adjusts 
-      ;; properties so that custom-save-all will save 
+      ;; This code from customize-save-customized adjusts
+      ;; properties so that custom-save-all will save
       ;; the value.
       (when value
 	(put symbol 'saved-value value)
@@ -901,7 +914,7 @@ The name of the defined function is returned."
 
 ;; FIXME: this doesn't do quite same thing as reset button,
 ;; which *removes* a setting from `custom-set-variables' list
-;; in custom.el.  Instead, this adds something to a 
+;; in custom.el.  Instead, this adds something to a
 ;; custom-reset-variables list.
 (defun pg-custom-reset-vars (&rest variables)
   "Reset custom vars VARIABLES to their default values."
@@ -920,7 +933,7 @@ The name of the defined function is returned."
   "Search for PROGNAME on PATH.  Return the full path to PROGNAME, or nil.
 If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path.
 EXTRAPATH is a list of extra path components"
-  (or 
+  (or
    (cond
     ((fboundp 'executable-find)
      (let ((exec-path (append exec-path extrapath)))
@@ -932,44 +945,5 @@ EXTRAPATH is a list of extra path components"
 		  1)))
    (if returnnopath progname)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Stuff for developing PG, not needed for ordinary users really.
-;; [Could consider moving this to a new file `proof-devel.el']
-;;
-
-(put 'proof-if-setting-configured 'lisp-indent-function 1)
-(put 'proof-define-assistant-command 'lisp-indent-function 'defun)
-(put 'proof-define-assistant-command-witharg 'lisp-indent-function 'defun)
-(put 'defpgcustom 'lisp-indent-function 'defun)
-(put 'proof-map-buffers 'lisp-indent-function 'defun)
-(put 'proof-with-current-buffer-if-exists 'lisp-indent-function 'defun)
-
-(defconst proof-extra-fls
-  (list
-   (list "^(\\(proof-def\\"
-	 ;; Variable like things
-	 "\\(asscustom)\\|"
-	 ;; Function like things
-	 "\\([^ \t\n\(\)]+\\)"
-	 ;; Any whitespace and declared object.
-	 "[ \t'\(]*"
-	 "\\([^ \t\n\)]+\\)?")
-   '(1 font-lock-keyword-face)
-   '(8 (cond ((match-beginning 3) 'font-lock-variable-name-face)
-	     ;; ((match-beginning 6) 'font-lock-type-face)
-	     (t 'font-lock-function-name-face))
-       nil t)))
-
-;; This doesn't work for FSF's font lock, developers should use
-;; XEmacs!  (unless edebug is broken, which it is in my 21.4.12)
-(if (boundp 'lisp-font-lock-keywords)	; compatibility hack
-    (setq lisp-font-lock-keywords 
-	  (append proof-extra-fls
-		  lisp-font-lock-keywords)))
-       
-(setq autoload-package-name "proof")
-(setq generated-autoload-file "proof-autoloads.el")
-	
-;; End of proof-utils.el
 (provide 'proof-utils)
+;;; proof-utils.el ends here