Renamed file

1 files changed, 659 insertions, 0 deletions

diff --git a/lib/proof-compat.el b/lib/proof-compat.el
new file mode 100644
index 00000000..f8222e40
--- /dev/null
+++ b/lib/proof-compat.el
@@ -0,0 +1,659 @@
+;; proof-compat.el   Operating system and Emacs version compatibility
+;;
+;; Copyright (C) 2000-2002 LFCS Edinburgh. 
+;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; $Id$
+;;
+;; This file collects together compatibility hacks for different
+;; operating systems and Emacs versions.  This is to help keep
+;; track of them.
+;;
+;; The development policy for Proof General is for the main codebase
+;; to be written for the latest stable version of XEmacs.  We follow
+;; XEmacs advice on removing obsolete function calls.
+;;
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Architecture flags
+;;;
+
+(eval-and-compile
+(defvar proof-running-on-XEmacs (string-match "XEmacs" emacs-version)
+  "Non-nil if Proof General is running on XEmacs.")
+(defvar proof-running-on-Emacs21 (and (not proof-running-on-XEmacs)
+				      (>= emacs-major-version 21))
+  "Non-nil if Proof General is running on GNU Emacs 21 or later.")
+;; rough test for XEmacs on win32, anyone know about GNU Emacs on win32?
+(defvar proof-running-on-win32 (fboundp 'win32-long-file-name)
+  "Non-nil if Proof General is running on a win32 system."))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Emacs and XEmacs modifications and adjustments
+;;;
+
+;; Remove a custom setting.  Needed to support dynamic reconfiguration.
+;; (We'd prefer that repeated defcustom calls acted like repeated
+;;  "defvar treated as defconst" in XEmacs)
+(defun pg-custom-undeclare-variable (symbol)
+  "Remove a custom setting SYMBOL.
+Done by `makunbound' and removing all properties mentioned by custom library."
+  (mapcar (lambda (prop) (remprop symbol prop))
+	  '(default 
+	     standard-value 
+	     force-value 
+	     variable-comment
+	     saved-variable-comment
+	     variable-documentation
+	     group-documentation
+	     custom-set
+	     custom-get
+	     custom-options
+	     custom-requests
+	     custom-group
+	     custom-prefix
+	     custom-tag
+	     custom-links
+	     custom-version
+	     saved-value
+	     theme-value
+	     theme-face))
+  (makunbound symbol))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; XEmacs compatibility
+;;;
+
+;; browse-url function isn't autoloaded in XEmacs 20.4
+(or (fboundp 'browse-url)
+    (autoload 'browse-url "browse-url"
+      "Ask a WWW browser to load URL." t))
+
+;; executable-find isn't autoloaded in XEmacs 21.4.6
+(or (fboundp 'executable-find)
+    (autoload 'executable-find "executable" "\
+Search for COMMAND in exec-path and return the absolute file name.
+Return nil if COMMAND is not found anywhere in `exec-path'." nil nil))
+
+
+;; Compatibility with XEmacs 20.3/4
+(or (boundp 'path-separator)
+    (setq path-separator (if proof-running-on-win32 ";" ":")))
+(or (fboundp 'split-path)
+    (defun split-path (path)
+      "Explode a search path into a list of strings.
+The path components are separated with the characters specified
+with `path-separator'."
+      (split-string path (regexp-quote path-separator))))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; XEmacs compatibility with GNU Emacs
+;;;
+
+(or (fboundp 'display-graphic-p)
+    (defun display-graphic-p ()
+      "Return non-nil if DISPLAY is a graphic display.
+Graphical displays are those which are capable of displaying several
+frames and several different fonts at once.  This is true for displays
+that use a window system such as X, and false for text-only terminals."
+      (or (eq (console-type) 'x)
+	  (eq (console-type) 'mswindows))))
+
+(or (fboundp 'subst-char-in-string)
+;; Code is taken from Emacs 21.2.1/subr.el 
+(defun subst-char-in-string (fromchar tochar string &optional inplace)
+  "Replace FROMCHAR with TOCHAR in STRING each time it occurs.
+Unless optional argument INPLACE is non-nil, return a new string."
+  (let ((i (length string))
+	(newstr (if inplace string (copy-sequence string))))
+    (while (> i 0)
+      (setq i (1- i))
+      (if (eq (aref newstr i) fromchar)
+	  (aset newstr i tochar)))
+    newstr)))
+
+;; Required by xmltok.el [not used at present], proof-shell.el
+(or (fboundp 'replace-regexp-in-string)
+;; Code is taken from Emacs 21.1.1/subr.el 
+(defun replace-regexp-in-string (regexp rep string &optional
+					fixedcase literal subexp start)
+  "Replace all matches for REGEXP with REP in STRING.
+
+Return a new string containing the replacements.
+
+Optional arguments FIXEDCASE, LITERAL and SUBEXP are like the
+arguments with the same names of function `replace-match'.  If START
+is non-nil, start replacements at that index in STRING.
+
+REP is either a string used as the NEWTEXT arg of `replace-match' or a
+function.  If it is a function it is applied to each match to generate
+the replacement passed to `replace-match'; the match-data at this
+point are such that match 0 is the function's argument.
+
+To replace only the first match (if any), make REGEXP match up to \\'
+and replace a sub-expression, e.g.
+  (replace-regexp-in-string \"\\(foo\\).*\\'\" \"bar\" \" foo foo\" nil nil 1)
+    => \" bar foo\"
+"
+
+  ;; To avoid excessive consing from multiple matches in long strings,
+  ;; don't just call `replace-match' continually.  Walk down the
+  ;; string looking for matches of REGEXP and building up a (reversed)
+  ;; list MATCHES.  This comprises segments of STRING which weren't
+  ;; matched interspersed with replacements for segments that were.
+  ;; [For a `large' number of replacments it's more efficient to
+  ;; operate in a temporary buffer; we can't tell from the function's
+  ;; args whether to choose the buffer-based implementation, though it
+  ;; might be reasonable to do so for long enough STRING.]
+  (let ((l (length string))
+	(start (or start 0))
+	matches str mb me)
+    (save-match-data
+      (while (and (< start l) (string-match regexp string start))
+	(setq mb (match-beginning 0)
+	      me (match-end 0))
+	;; If we matched the empty string, make sure we advance by one char
+	(when (= me mb) (setq me (min l (1+ mb))))
+	;; Generate a replacement for the matched substring.
+	;; Operate only on the substring to minimize string consing.
+	;; Set up match data for the substring for replacement;
+	;; presumably this is likely to be faster than munging the
+	;; match data directly in Lisp.
+	(string-match regexp (setq str (substring string mb me)))
+	(setq matches
+	      (cons (replace-match (if (stringp rep)
+				       rep
+				     (funcall rep (match-string 0 str)))
+				   fixedcase literal str subexp)
+		    (cons (substring string start mb) ; unmatched prefix
+			  matches)))
+	(setq start me))
+      ;; Reconstruct a string from the pieces.
+      (setq matches (cons (substring string start l) matches)) ; leftover
+      (apply #'concat (nreverse matches))))))
+
+
+;; The GNU Emacs implementation of easy-menu-define has a very handy
+;; :visible keyword.  To use that when it's available, we set a
+;; constant to be :visible or :active
+
+(defconst menuvisiblep (if proof-running-on-Emacs21 :visible :active)
+  ":visible (on GNU Emacs) or :active (otherwise). 
+The GNU Emacs implementation of easy-menu-define has a very handy
+:visible keyword.  To use that when it's available, we use this constant.")
+
+ 
+(or (fboundp 'frame-parameter)
+    (defalias 'frame-parameter 'frame-property))
+
+(or (boundp 'window-size-fixed)
+    (defvar window-size-fixed nil 
+      "Fudged version of GNU Emacs' setting.  Completely ignored."))
+
+(or (fboundp 'window-text-height)
+    (defalias 'window-text-height 'window-text-area-height))
+
+(or (fboundp 'set-window-text-height)
+(defun set-window-text-height (window height)
+  "Sets the height in lines of the text display area of WINDOW to HEIGHT.
+This doesn't include the mode-line (or header-line if any) or any
+partial-height lines in the text display area.
+
+If WINDOW is nil, the selected window is used.
+
+Note that the current implementation of this function cannot always set
+the height exactly, but attempts to be conservative, by allocating more
+lines than are actually needed in the case where some error may be present."
+  (let ((delta (- height (window-text-height window))))
+    (unless (zerop delta)
+      (let ((window-min-height 1))
+	(if (and window (not (eq window (selected-window))))
+	    (save-selected-window
+	      (select-window window)
+	      (enlarge-window delta))
+	  (enlarge-window delta)))))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; GNU Emacs compatibility with XEmacs
+;;;
+
+(unless (fboundp 'save-selected-frame)
+(defmacro save-selected-frame (&rest body)
+  "Execute forms in BODY, then restore the selected frame.
+The value returned is the value of the last form in BODY."
+  (let ((old-frame (gensym "ssf")))
+    `(let ((,old-frame (selected-frame)))
+       (unwind-protect
+           (progn ,@body)
+         (select-frame ,old-frame))))))
+
+;; Chars (borrowed from x-symbol-emacs.el compatability file)
+
+(unless (fboundp 'characterp) (defalias 'characterp 'integerp))
+(unless (fboundp 'int-to-char) (defalias 'int-to-char 'identity))
+(unless (fboundp 'char-to-int) (defalias 'char-to-int 'identity))
+
+;; Missing function, but anyway Emacs has no datatype for events...
+
+(unless (fboundp 'events-to-keys)
+  (defalias 'events-to-keys 'identity))
+
+(unless (fboundp 'region-exists-p)
+  (defun region-exists-p () mark-active))
+
+;; completion not autoloaded in GNU 20.6.1; we must call 
+;; dynamic-completion-mode after loading it.
+(or (fboundp 'complete)
+    (autoload 'complete "completion"))
+(unless proof-running-on-XEmacs
+  (eval-after-load "completion"
+    '(dynamic-completion-mode)))
+
+
+;; These days cl is dumped with XEmacs (20.4,21.1) but not GNU Emacs
+;; 20.2.  Would rather it was autoloaded but the autoloads are broken
+;; in GNU so we load it now.
+(require 'cl)				
+
+;; Give a warning,
+(or (fboundp 'warn)
+(defun warn (str &rest args)
+      "Issue a warning STR.  Defined by PG for GNU compatibility."
+      (apply 'message str args)
+      (sit-for 2)))
+
+;; Modeline redrawing (actually force-mode-line-update is alias on XEmacs)
+(or (fboundp 'redraw-modeline)
+(defun redraw-modeline (&rest args)
+  "Dummy function for Proof General on GNU Emacs."
+  (force-mode-line-update)))
+
+;; Interactive flag
+(or (fboundp 'noninteractive)
+    (defun noninteractive ()
+      "Dummy function for Proof General on GNU Emacs."
+      noninteractive))
+
+;; Replacing in string (useful function from subr.el in XEmacs 21.1.9)
+(or (fboundp 'replace-in-string)
+    (if (fboundp 'replace-regexp-in-string)
+      (defun replace-in-string (str regexp newtext &optional literal)
+        (replace-regexp-in-string regexp newtext str 'fixedcase literal))
+(defun replace-in-string (str regexp newtext &optional literal)
+  "Replace all matches in STR for REGEXP with NEWTEXT string,
+ and returns the new string.
+Optional LITERAL non-nil means do a literal replacement.
+Otherwise treat \\ in NEWTEXT string as special:
+  \\& means substitute original matched text,
+  \\N means substitute match for \(...\) number N,
+  \\\\ means insert one \\."
+  ;; Not present in GNU
+  ;; (check-argument-type 'stringp str)
+  ;; (check-argument-type 'stringp newtext)
+  (let ((rtn-str "")
+	(start 0)
+	(special)
+	match prev-start)
+    (while (setq match (string-match regexp str start))
+      (setq prev-start start
+	    start (match-end 0)
+	    rtn-str
+	    (concat
+	      rtn-str
+	      (substring str prev-start match)
+	      (cond (literal newtext)
+		    (t (mapconcat
+			(lambda (c)
+			  (if special
+			      (progn
+				(setq special nil)
+				(cond ((eq c ?\\) "\\")
+				      ((eq c ?&)
+				       (substring str
+						  (match-beginning 0)
+						  (match-end 0)))
+				      ((and (>= c ?0) (<= c ?9))
+				       (if (> c (+ ?0 (length
+						       (match-data))))
+					   ;; Invalid match num
+					   (error "Invalid match num: %c" c)
+					 (setq c (- c ?0))
+					 (substring str
+						    (match-beginning c)
+						    (match-end c))))
+				      (t (char-to-string c))))
+			    (if (eq c ?\\) (progn (setq special t) nil)
+			      (char-to-string c))))
+			 newtext ""))))))
+    (concat rtn-str (substring str start))))))
+
+;; An implemenation of buffer-syntactic-context for GNU Emacs
+(defun proof-buffer-syntactic-context-emulate (&optional buffer)
+  "Return the syntactic context of BUFFER at point.
+If BUFFER is nil or omitted, the current buffer is assumed.
+The returned value is one of the following symbols:
+
+	nil		; meaning no special interpretation
+	string		; meaning point is within a string
+	comment		; meaning point is within a line comment"
+  (save-excursion
+    (if buffer (set-buffer buffer))
+    (let ((pp (parse-partial-sexp (point-min) (point))))
+      (cond
+       ((nth 3 pp) 'string)
+       ;; ((nth 7 pp) 'block-comment)
+       ;; "Stefan Monnier" <monnier+misc/news@rum.cs.yale.edu> suggests
+       ;; distinguishing between block comments and ordinary comments
+       ;; is problematic: not what XEmacs claims and different to what
+       ;; (nth 7 pp) tells us in GNU Emacs.
+       ((nth 4 pp) 'comment)))))
+
+
+;; In case Emacs is not aware of the function read-shell-command,
+;; we duplicate some code adjusted from minibuf.el distributed 
+;; with XEmacs 21.1.9
+;;
+;; This code is still required as of GNU Emacs 20.6.1
+;;
+;; da: I think bothering with this just to give completion for
+;; when proof-prog-name-ask=t is rather a big overkill!
+;; Still, now it's here we'll leave it in as a pleasant surprise
+;; for GNU Emacs users.
+;;	
+(or (fboundp 'read-shell-command)
+(defvar read-shell-command-map
+  (let ((map (make-sparse-keymap 'read-shell-command-map)))
+    (if (not (fboundp 'set-keymap-parents))
+	(if (fboundp 'set-keymap-parent)
+	    ;; GNU Emacs 20.2
+	    (set-keymap-parent map minibuffer-local-map)
+	  ;; Earlier GNU Emacs
+	  (setq map (append minibuffer-local-map map)))
+      ;; XEmacs versions without read-shell-command?
+      (set-keymap-parents map minibuffer-local-map))
+    (define-key map "\t" 'comint-dynamic-complete)
+    (define-key map "\M-\t" 'comint-dynamic-complete)
+    (define-key map "\M-?" 'comint-dynamic-list-completions)
+    map)
+  "Minibuffer keymap used by `shell-command' and related commands."))
+
+
+(or (fboundp 'read-shell-command)
+(defun read-shell-command (prompt &optional initial-input history)
+      "Just like read-string, but uses read-shell-command-map:
+\\{read-shell-command-map}"
+      (let ((minibuffer-completion-table nil))
+        (read-from-minibuffer prompt initial-input read-shell-command-map
+                              nil (or history 'shell-command-history)))))
+
+
+;; Emulate a useful builtin from XEmacs.
+
+(or (fboundp 'remassq)
+;; NB: Emacs has assoc package with assq-delete-all function
+(defun remassq (key alist)
+  "Delete any elements of ALIST whose car is `eq' to KEY.
+The modified ALIST is returned."
+;; The builtin version deletes by side-effect, but don't bother here.
+  (let (newalist)
+    (while alist
+      (unless (eq key (caar alist))
+	(setq newalist (cons (car alist) newalist)))
+      (setq alist (cdr alist)))
+    (nreverse newalist))))
+
+(or (fboundp 'remassoc)
+(defun remassoc (key alist)
+  "Delete any elements of ALIST whose car is `equal' to KEY.
+The modified ALIST is returned."
+;; The builtin version deletes by side-effect, but don't bother here.
+  (let (newalist)
+    (while alist
+      (unless (equal key (caar alist))
+	(setq newalist (cons (car alist) newalist)))
+      (setq alist (cdr alist)))
+    (nreverse newalist))))
+
+(or (fboundp 'frames-of-buffer)
+;; From XEmacs 21.4.12, aliases expanded
+(defun frames-of-buffer (&optional buffer visible-only)
+  "Return list of frames that BUFFER is currently being displayed on.
+If the buffer is being displayed on the currently selected frame, that frame
+is first in the list.  VISIBLE-ONLY will only list non-iconified frames."
+  (let ((list (get-buffer-window-list buffer))
+	(cur-frame (selected-frame))
+	next-frame frames save-frame)
+
+    (while list
+      (if (memq (setq next-frame (window-frame (car list)))
+		frames)
+	  nil
+	(if (eq cur-frame next-frame)
+	    (setq save-frame next-frame)
+	  (and
+	   (or (not visible-only)
+	       (frame-visible-p next-frame))
+	   (setq frames (append frames (list next-frame))))))
+	(setq list (cdr list)))
+
+    (if save-frame
+	(append (list save-frame) frames)
+      frames))))
+
+;; These functions are used in the intricate logic around
+;; shrink-to-fit.  
+
+;; window-leftmost-p, window-rightmost-p: my implementations
+(or (fboundp 'window-leftmost-p)
+    (defun window-leftmost-p (window)
+      (zerop (car (window-edges window)))))
+
+(or (fboundp 'window-rightmost-p)
+    (defun window-rightmost-p (window)
+      (>= (nth 2 (window-edges window))
+	  (frame-width (window-frame window)))))
+
+;; with-selected-windown from XEmacs 21.4.12
+(or (fboundp 'with-selected-window)
+(defmacro with-selected-window (window &rest body)
+  "Execute forms in BODY with WINDOW as the selected window.
+The value returned is the value of the last form in BODY."
+  `(save-selected-window
+     (select-window ,window)
+     ,@body)))
+
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; A naughty hack to completion.el 
+;;;
+;;; At the moment IMO completion too eagerly adds stuff to
+;;; its database: the completion-before-command function
+;;; makes every suffix be added as a completion!
+
+(eval-after-load "completion"
+'(defun completion-before-command ()
+  (if (and (symbolp this-command) (get this-command 'completion-function))
+	(funcall (get this-command 'completion-function)))))
+      
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Attempt to harmonise pop-to-buffer behaviour 
+;;;
+
+(if proof-running-on-Emacs21
+    ;; NB: GNU Emacs version has fewer args
+    (defalias 'pg-pop-to-buffer 'pop-to-buffer))
+
+(if proof-running-on-XEmacs
+;; Version from XEmacs 21.4.12, with args to match GNU Emacs
+;; NB: GNU Emacs version has fewer args, we don't use ON-FRAME
+(defun pg-pop-to-buffer (bufname &optional not-this-window-p no-record on-frame)
+  "Select buffer BUFNAME in some window, preferably a different one.
+If BUFNAME is nil, then some other buffer is chosen.
+If `pop-up-windows' is non-nil, windows can be split to do this.
+If optional second arg NOT-THIS-WINDOW-P is non-nil, insist on finding
+another window even if BUFNAME is already visible in the selected window.
+If optional fourth arg is non-nil, it is the frame to pop to this
+buffer on.
+If optional third arg is non-nil, do not record this in switching history.
+(addition for PG).
+
+If `focus-follows-mouse' is non-nil, keyboard focus is left unchanged."
+  (let ((oldbuf (current-buffer))
+	buf window frame)
+    (if (null bufname)
+	(setq buf (other-buffer (current-buffer)))
+      (setq buf (get-buffer bufname))
+      (if (null buf)
+	  (progn
+	    (setq buf (get-buffer-create bufname))
+	    (set-buffer-major-mode buf))))
+    (push-window-configuration)
+    (set-buffer buf)
+    (setq window (display-buffer buf not-this-window-p on-frame))
+    (setq frame (window-frame window))
+    ;; if the display-buffer hook decided to show this buffer in another
+    ;; frame, then select that frame, (unless obeying focus-follows-mouse -sb).
+    (if (and (not focus-follows-mouse)
+	     (not (eq frame (selected-frame))))
+	(select-frame frame))
+    (unless no-record (record-buffer buf))
+    (if (and focus-follows-mouse
+	     on-frame
+	     (not (eq on-frame (selected-frame))))
+	(set-buffer oldbuf)
+      ;; select-window will modify the internal keyboard focus of XEmacs
+      (select-window window))
+    buf))
+);;; End XEmacs only
+
+  
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Old Emacs version compatibility
+;;;
+
+;; Create a menu from a customize group, for older/non-existent customize
+
+(or (fboundp 'process-live-p)
+(defun process-live-p (obj)
+  "Return t if OBJECT is a process that is alive"
+  (and (processp obj)
+       (memq (process-status obj) '(open run stop)))))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Compatibility with Custom library function to create a menu
+;;
+;; For some unfathomable reason, customize-menu-create goes
+;; wrong with PG groups on Emacs 21.  (It works with 'customize
+;; though).  We just disable it there. It's not worth this hassle.
+;;
+;; PG 3.5: this was used in proof-menu.el.  Things seem okay again 
+;; as of GNU Emacs 21.3.1.
+;; (cond
+;;  (proof-running-on-XEmacs
+;;   (defun pg-customize-menu-create (grp &optional name)
+;;     (list (customize-menu-create grp name))))
+;;  (t
+;;   (defun pg-customize-menu-create (grp &optional name)
+;;     nil)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; General Emacs version compatibility
+;;;
+
+
+;; These are internal functions of font-lock, autoload policy
+;; differs between Emacs versions
+
+;; Beware: font-lock-set-defaults does completely different things
+;; in Emacs from what it does in XEmacs.
+(or (fboundp 'font-lock-set-defaults)
+    (autoload 'font-lock-set-defaults "font-lock"))
+(or (fboundp 'font-lock-fontify-region)
+    (autoload 'font-lock-fontify-region "font-lock"))
+(or (fboundp 'font-lock-append-text-property)
+    (autoload 'font-lock-append-text-property "font-lock"))
+
+
+;; font-lock-preprocessor-face
+;; This face is missing from Emacs 21.2's font-lock,
+;; but used in Isabelle highlighting, at least.
+(eval-after-load "font-lock"
+(unless (boundp 'font-lock-preprocessor-face)
+  ;; Taken from font-lock.el in XEmacs 21.4.8 (V 1.52)
+  (defvar font-lock-preprocessor-face 'font-lock-preprocessor-face
+  "This variable should not be set.
+The corresponding face should be set using `edit-faces' or the
+`set-face-*' functions.")
+
+  (defface font-lock-preprocessor-face
+  '((((class color) (background dark)) (:foreground "steelblue1"))
+    (((class color) (background light)) (:foreground "blue3"))
+    (t (:underline t)))
+  "Font Lock Mode face used to highlight preprocessor conditionals."
+  :group 'font-lock-faces)))
+
+
+;; Handle buggy buffer-syntactic-context workaround in XEmacs 21.1,
+;; and GNU non-implementation.
+
+(cond
+ ((not (fboundp 'buffer-syntactic-context))
+  (defalias 'proof-buffer-syntactic-context 
+    'proof-buffer-syntactic-context-emulate))
+ ((or
+   (string-match "21\.1 .*XEmacs" emacs-version)
+   (string-match "21\.4 .*XEmacs" emacs-version)) ;; still buggy in 21.4
+  (defalias 'proof-buffer-syntactic-context 
+    'proof-buffer-syntactic-context-emulate))
+ (t
+  ;; Rashly assume this version has a good implementation
+  (defalias 'proof-buffer-syntactic-context
+    'buffer-syntactic-context)))
+   
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Nasty: Emacs bug/problem fix section
+;;;
+
+;; NB: customize-menu-create is buggy in some versions of GNU Emacs
+;; (bad in 21.1.0, good in 21.1.1, bad in 21.2.1, ...).  Comment
+;; these next lines out if you must use one of these versions.
+;; PG 3.5.1: add hack in proof-compat.el to deal with this
+(if
+    (and
+     proof-running-on-Emacs21
+     (or
+      (string-equal emacs-version "21.2.1")
+      (string-equal emacs-version "21.1.0")))
+    (defun customize-menu-create (symbol &optional name)
+      (cons 
+       (or name "Customize")
+       (list 
+	["Your version of Emacs is buggy; update to get this menu" 
+	 '(w3-goto-url "http://www.gnu.org/software/emacs/")
+	 t]))))
+
+
+;; End of proof-compat.el
+(provide 'proof-compat)