From 646a53c46063e2af83293e1351a8dd55fa986141 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 25 Aug 2004 11:51:29 +0000 Subject: Renamed file --- generic/proof-compat.el | 659 ------------------------------------------------ lib/proof-compat.el | 659 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 659 insertions(+), 659 deletions(-) delete mode 100644 generic/proof-compat.el create mode 100644 lib/proof-compat.el diff --git a/generic/proof-compat.el b/generic/proof-compat.el deleted file mode 100644 index f8222e40..00000000 --- a/generic/proof-compat.el +++ /dev/null @@ -1,659 +0,0 @@ -;; proof-compat.el Operating system and Emacs version compatibility -;; -;; Copyright (C) 2000-2002 LFCS Edinburgh. -;; Author: David Aspinall 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" 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) 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 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" 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) -- cgit v1.2.3