diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/completer.el pvs-4.2/emacs/emacs-src/ilisp/completer.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/completer.el 2008-09-07 13:51:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/completer.el 2010-01-29 14:53:48.058988250 -0700
@@ -175,14 +175,10 @@
(inhibit-quit t))
(sit-for 2)
(delete-region point end)
- (if (and quit-flag
- ;; (not (eq 'lucid-19 ilisp-emacs-version-id))
- ;; (not (string-match "Lucid" emacs-version))
- (not (memq +ilisp-emacs-version-id+
- '(xemacs lucid-19 lucid-19-new)))
- )
+ (if quit-flag
(setq quit-flag nil)
- (push 7 unread-command-events))))
+ (push (if (featurep 'xemacs) (character-to-event 7) 7)
+ unread-command-events))))
;;;
(defun completer-deleter (regexp choices &optional keep)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilcompat.el pvs-4.2/emacs/emacs-src/ilisp/ilcompat.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilcompat.el 2007-09-25 01:46:25.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilcompat.el 2010-01-29 14:53:48.059984772 -0700
@@ -25,11 +25,7 @@
((string-match "XEmacs " (emacs-version))
(message "ILISP: Unknown XEmacs. Assuming XEmacs 20 - best of luck!")
'xemacs-20)
- ((string-match "Emacs 22" (emacs-version))
- 'fsf-20)
- ((string-match "Emacs 21" (emacs-version))
- 'fsf-20)
- ((string-match "Emacs 20" (emacs-version))
+ ((string-match "Emacs 2[[:digit:]]" (emacs-version))
'fsf-20)
((string-match "Emacs 19" (emacs-version))
'fsf-19)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilfsf20.el pvs-4.2/emacs/emacs-src/ilisp/ilfsf20.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilfsf20.el 2007-09-25 01:47:46.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilfsf20.el 2010-01-29 14:53:48.059984772 -0700
@@ -53,6 +53,7 @@
;;;============================================================================
;;; Epilogue
+(setq-default confirm-nonexistent-file-or-buffer nil)
(provide 'compat-fsf-20)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-bat.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-bat.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-bat.el 2005-11-24 21:48:47.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-bat.el 2010-01-29 14:53:48.060985635 -0700
@@ -12,6 +12,8 @@
;;;
;;; $Id: ilisp-bat.el 4504 2005-11-25 04:48:47Z owre $
+(require 'cl)
+
(defun mark-change-lisp (arg)
"Mark the current defun as being changed.
This is to make 'lisp-eval-changes' or 'lisp-compile-changes' work on
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-cl-easy-menu.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-cl-easy-menu.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-cl-easy-menu.el 2006-04-15 02:51:05.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-cl-easy-menu.el 2010-01-29 14:53:48.060985635 -0700
@@ -71,6 +71,7 @@
;> (member +ilisp-emacs-version-id+ '(xemacs lucid-19 lucid-19-new)))
;> (not (featurep 'ilisp-easy-menu)))
+(require 'cl)
(require 'easymenu)
;; (eval-when (load compile eval)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-cmp.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-cmp.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-cmp.el 2005-11-24 22:10:52.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-cmp.el 2010-01-29 14:53:48.062037214 -0700
@@ -147,8 +147,8 @@
"Only allow a paren if ilisp-paren is T."
(interactive)
(if ilisp-paren
- (if (or (eq last-input-char ?\() (eq (char-after (ilisp-minibuffer-prompt-end)) ?\())
- (insert last-input-char)
+ (if (or (eq (ilisp-last-input-char) ?\() (eq (char-after (ilisp-minibuffer-prompt-end)) ?\())
+ (insert (ilisp-last-input-char))
(beep))
(beep)))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-cmu.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-cmu.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-cmu.el 2006-04-15 02:51:05.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-cmu.el 2010-01-29 14:54:37.217926806 -0700
@@ -46,8 +46,7 @@
(setq ilisp-source-directory-fixup-alist
(list
(cons cmulisp-source-directory-regexp
- cmulisp-local-source-directory)))
- (message "cmulisp-local-source-directory not set."))
+ cmulisp-local-source-directory))))
(setq comint-prompt-regexp "^\\([0-9]+\\]+\\|\\*\\|[-a-zA-Z0-9]*\\[[0-9]+\\]:\\) "
ilisp-trace-command "(ILISP:cmulisp-trace \"%s\" \"%s\" \"%s\")"
comint-prompt-status
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-dia.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-dia.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-dia.el 2008-09-07 13:51:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-dia.el 2010-01-29 14:53:48.062037214 -0700
@@ -169,9 +169,9 @@
;; Comint defaults
(set-ilisp-input-ring-size 200)
(setq comint-prompt-regexp "^[^<> ]*>+:? *"
- comint-use-prompt-regexp-instead-of-fields t ; Emacs 21 fields don't seem to work with comint-ipc (?)
+ comint-use-prompt-regexp t ; Emacs 21 fields don't seem to work with comint-ipc (?)
comint-get-old-input 'ilisp-get-old-input
- comint-input-sentinel (function ignore)
+ comint-input-filter-functions nil
comint-input-filter 'ilisp-input-filter
comint-input-sender 'comint-default-send
comint-eol-on-send t)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-hi.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-hi.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-hi.el 2005-11-24 22:29:32.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-hi.el 2010-01-29 14:53:48.063926219 -0700
@@ -11,6 +11,8 @@
;;; $Id: ilisp-hi.el 4506 2005-11-25 05:29:32Z owre $
;;;%Eval/compile
+(require 'cl)
+
(defun lisp-send-region (start end switch message status format
&optional handler)
"Sends a region to the lisp buffer and execute a 'command' on it.
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-hnd.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-hnd.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-hnd.el 2005-11-24 22:29:32.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-hnd.el 2010-01-29 14:53:48.063926219 -0700
@@ -31,7 +31,7 @@
(if (and (not wait-p)
(setq output (comint-remove-whitespace output))
(or error-p (string-match "\n" output)))
- (let* ((buffer (ilisp-output-buffer ilisp-output t))
+ (let* ((buffer (ilisp-output-buffer t))
(out (if error-p
(funcall ilisp-error-filter output)
output))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-imenu.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-imenu.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-imenu.el 2007-09-25 02:53:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-imenu.el 2010-01-29 14:53:48.065029991 -0700
@@ -10,7 +10,7 @@
;;;
;;; $Id: ilisp-imenu.el,v 1.5 2002/01/31 14:56:45 mna Exp $
-
+(require 'cl)
(require 'imenu)
;;; modified for a better display of function+arglist!
@@ -27,7 +27,9 @@
((and name (imenu--in-alist name index-alist))
(setq prompt (format "Index item (default %s): " name)))
(t (setq prompt "Index item: ")))
- (if (eq imenu-always-use-completion-buffer-p 'never)
+ (if (if (featurep 'xemacs)
+ (eq imenu-always-use-completion-buffer-p 'never)
+ (null imenu-use-popup-menu))
(setq name (completing-read prompt
index-alist
nil t nil 'imenu--history-list name))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-menu.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-menu.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-menu.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-menu.el 2010-01-29 14:53:48.065029991 -0700
@@ -11,10 +11,7 @@
;;; $Id: ilisp-menu.el 4507 2005-11-25 06:03:15Z owre $
-(cond ((or (string-match "XEmacs" emacs-version)
- (string-match "Lucid" emacs-version)))
- (t
-
+(unless (featurep 'xemacs)
(require 'simple-menu)
(setplist 'lisp-command-menu nil)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-mod.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-mod.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-mod.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-mod.el 2010-01-29 14:53:48.065987967 -0700
@@ -13,6 +13,8 @@
;;;%ilisp-mode
+(require 'cl)
+
(defun ilisp-byte-code-to-list (function)
"Returns a list suitable for passing to make-byte-code from FUNCTION."
(let ((function-object
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-mov.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-mov.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-mov.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-mov.el 2010-01-29 14:53:48.065987967 -0700
@@ -148,7 +148,7 @@
(let ((point (point)))
(beginning-of-line)
(if comment-start (search-forward comment-start point t))))
- (progn (next-line 1) (indent-line-ilisp)))
+ (progn (forward-line 1) (indent-line-ilisp)))
(point))))
;;;
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-out.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-out.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-out.el 2007-09-25 01:47:10.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-out.el 2010-01-29 14:53:48.070174664 -0700
@@ -184,7 +184,7 @@
(save-excursion
(set-buffer buffer)
(let ((stdheight (1+ (count-screen-lines (point-min) (point-max)))))
- (if (string-match "XEmacs" emacs-version)
+ (if (featurep 'xemacs)
(1+ stdheight)
stdheight))))
@@ -256,7 +256,7 @@
window from which enlarge-window would steal lines."
(unless (window-live-p window)
(error "the window was not live"))
- (if (or (not (string-match "XEmacs" emacs-version))
+ (if (or (not (featurep 'xemacs))
(and (= emacs-major-version 19)
(< emacs-minor-version 12)))
(let* ((bottom (nth 3 (window-edges window)))
@@ -274,7 +274,7 @@
;; XEmacs change -- There is now a primitive to do this.
(defun ilisp-find-top-left-most-window ()
"Return the leftmost topmost window on the current screen."
- (if (or (not (string-match "XEmacs" emacs-version))
+ (if (or (not (featurep 'xemacs))
(and (= emacs-major-version 19)
(< emacs-minor-version 12)))
(let* ((window* (selected-window))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-prc.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-prc.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-prc.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-prc.el 2010-01-29 14:53:48.070174664 -0700
@@ -11,6 +11,7 @@
;;;
;;; $Id: ilisp-prc.el 4507 2005-11-25 06:03:15Z owre $
+(require 'cl)
(defun ilisp-process ()
"Return the current ILISP process."
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-rng.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-rng.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-rng.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-rng.el 2010-01-29 14:53:48.070927069 -0700
@@ -37,8 +37,8 @@
(setq point (point)))
(push-mark point)
(set-ilisp-input-ring-index n)
- (setq this-command 'comint-previous-similar-input
- comint-last-similar-string string)
+ (setq this-command 'comint-previous-matching-input
+ comint-matching-input-from-input-string string)
t)
(if (and string (not no-insert))
(progn (comint-kill-input) (insert string) t)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-utl.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-utl.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-utl.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-utl.el 2010-01-29 14:53:48.070927069 -0700
@@ -122,4 +122,9 @@
;; (ilisp-update-menu status))
(comint-update-status status))
+(defun ilisp-last-input-char ()
+ (if (featurep 'xemacs)
+ (event-to-character last-input-event)
+ last-input-event))
+
;;; end of file -- ilisp-utl.el --
diff -dur pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-xfr.el pvs-4.2/emacs/emacs-src/ilisp/ilisp-xfr.el
--- pvs-4.2.ORIG/emacs/emacs-src/ilisp/ilisp-xfr.el 2005-11-24 23:03:15.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/ilisp/ilisp-xfr.el 2010-01-29 14:53:48.071989431 -0700
@@ -37,7 +37,7 @@
(not (string= (ring-ref (ilisp-get-input-ring) 0)
input))))
(ilisp-ring-insert (ilisp-get-input-ring) input))
- (funcall comint-input-sentinel input)
+ (run-hook-with-args 'comint-input-filter-functions input)
;; Ugh, comint changing under my feet....
;; Note: This used to be
;; (eq ilisp-emacs-version-id 'gnu-19)
@@ -96,11 +96,11 @@
(interactive)
(when (ilisp-value 'ilisp-raw-echo t)
(goto-char (point-max))
- (insert last-input-char)
+ (insert (ilisp-last-input-char))
(set-marker (process-mark (ilisp-process)) (point))
(set-marker comint-last-input-end (point)))
(process-send-string (ilisp-process)
- (make-string 1 last-input-char))
+ (make-string 1 (ilisp-last-input-char)))
(message ilisp-raw-message))
;;;
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-browser.el pvs-4.2/emacs/emacs-src/pvs-browser.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-browser.el 2007-09-04 12:42:53.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-browser.el 2010-01-29 14:53:48.071989431 -0700
@@ -397,8 +397,8 @@
declaration. This command is useful to determine the type of a name,
or the resolution determined by the typechecker for an overloaded name."
(interactive "e")
- (cond ((string-match "XEmacs" (emacs-version))
- ;; This code is courtesy Jerry James (james@ittc.ku.edu)
+ (cond ((featurep 'xemacs)
+ ;; This code is courtesy Jerry James (loganjerry@gmail.com)
(if (and (mouse-event-p event) (event-over-text-area-p event))
(progn
(select-window (event-window event))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-byte-compile.el pvs-4.2/emacs/emacs-src/pvs-byte-compile.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-byte-compile.el 2008-09-07 13:51:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-byte-compile.el 2010-01-29 14:53:48.072961199 -0700
@@ -21,6 +21,8 @@
;; Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
;; --------------------------------------------------------------------
+(require 'cl)
+
(message "PVS: byte compilation starting")
; compile in the current directory
@@ -66,7 +68,7 @@
pvs-prelude-files-and-regions
pvs-set-prelude-info
)))
- (mapcar '(lambda (a) (pvs-compile a))
+ (mapc '(lambda (a) (pvs-compile a))
pvsfiles))
(message "PVS: byte compilation done")
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-cmds.el pvs-4.2/emacs/emacs-src/pvs-cmds.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-cmds.el 2009-10-04 13:28:46.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-cmds.el 2010-01-29 14:53:48.073925711 -0700
@@ -1353,9 +1353,11 @@
(comint-send (ilisp-process) "(exit-pvs t)")
(while (and (ilisp-process)
(eq (process-status (ilisp-process)) 'run))
- (sit-for 1)))
+ (if (null (accept-process-output nil 1))
+ (discard-input))))
(error
- (sleep-for 1)
+ (if (null (accept-process-output nil 1))
+ (discard-input))
(when (equal (process-status process) 'run)
(error "PVS Lisp process did not exit properly"))))))))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-ilisp.el pvs-4.2/emacs/emacs-src/pvs-ilisp.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-ilisp.el 2009-07-30 23:59:33.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-ilisp.el 2010-01-29 14:53:48.074959599 -0700
@@ -28,11 +28,12 @@
;; --------------------------------------------------------------------
(eval-when-compile (require 'comint))
+(require 'cl)
(require 'ilisp)
(eval-when-compile (require 'pvs-macros))
;;; FIXME - this may be related to changes in easymenu.el ???
-(when (string-match "XEmacs" (emacs-version))
+(when (featurep 'xemacs)
(add-hook 'ilisp-mode-hook
'(lambda ()
(add-submenu nil pvs-mode-menus ""))))
@@ -407,7 +408,7 @@
(princ-nl (remove-esc out)
'external-debugging-output)))
(t (message (remove-esc out))
- (if (string-match "XEmacs" (emacs-version))
+ (if (featurep 'xemacs)
(sit-for (/ pvs-message-delay 1000.0))
(sit-for 0 pvs-message-delay))
(pvs-log-message 'MSG (remove-esc out)))))
@@ -1205,7 +1206,7 @@
(or (ring-empty-p input-ring)
(not (string= (ring-ref input-ring 0) input))))
(ring-insert-new input-ring input))
- (funcall comint-input-sentinel input)
+ (run-hook-with-args 'comint-input-filter-functions input)
;; Nuke symbol table
(setq ilisp-original nil)
(funcall comint-input-sender proc input)
@@ -1303,7 +1304,7 @@
;;; DSC - I don't know what the bug is, but it can't do any
;;; harm to leave this here for the moment. Was in pvs-ilisp-mods.
-(when (and (string-match "GNU Emacs" (emacs-version))
+(when (and (not (featurep 'xemacs))
(boundp 'emacs-major-version)
(= emacs-major-version 19)
(< emacs-minor-version 31))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-load.el pvs-4.2/emacs/emacs-src/pvs-load.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-load.el 2008-09-07 13:51:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-load.el 2010-01-29 14:53:48.075963639 -0700
@@ -127,12 +127,12 @@
(load "pvs-print" nil noninteractive)
(load "pvs-prover" nil noninteractive)
(load "pvs-abbreviations" nil noninteractive)
-(if (or (and (string-match "GNU Emacs" (emacs-version))
+(if (or (and (not (featurep 'xemacs))
(boundp 'emacs-major-version)
(or (>= emacs-major-version 20)
(and (= emacs-major-version 19)
(>= emacs-minor-version 29))))
- (and (string-match "XEmacs" (emacs-version))
+ (and (featurep 'xemacs)
(boundp 'emacs-major-version)
(or (>= emacs-major-version 20)
(and (= emacs-major-version 19)
@@ -169,14 +169,14 @@
; fancy PVS logo for Emacs startup
-(when (and (string-match "GNU Emacs" (emacs-version))
+(when (and (not (featurep 'xemacs))
(boundp 'emacs-major-version)
(>= emacs-major-version 20)
(boundp 'image-types)
(memq 'xpm image-types))
(setq pvs-logo (create-image (concat pvs-path "/emacs/emacs-src/pvs.xpm"))))
-(when (and (string-match "XEmacs" (emacs-version))
+(when (and (featurep 'xemacs)
(boundp 'emacs-major-version)
(>= emacs-major-version 20)
(valid-image-instantiator-format-p 'xpm))
@@ -198,7 +198,7 @@
(if (boundp 'pvs-logo)
(progn
(insert "\n\n")
- (cond ((string-match "XEmacs" (emacs-version))
+ (cond ((featurep 'xemacs)
(indent-to (startup-center-spaces pvs-logo))
(set-extent-begin-glyph (make-extent (point) (point)) pvs-logo))
(t (insert " ")
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-macros.el pvs-4.2/emacs/emacs-src/pvs-macros.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-macros.el 2006-08-02 15:07:11.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-macros.el 2010-01-29 14:53:48.076959770 -0700
@@ -47,8 +47,8 @@
;; This is courtesy of Jerry James.
-(when (string-match "XEmacs" (emacs-version))
-
+(when (featurep 'xemacs)
+
(defun with-timeout-handler (tag)
(throw tag 'timeout))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-menu.el pvs-4.2/emacs/emacs-src/pvs-menu.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-menu.el 2009-10-04 12:49:26.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-menu.el 2010-01-29 14:53:48.077945626 -0700
@@ -206,7 +206,7 @@
["suspend-pvs" suspend-pvs t]
["exit-pvs" exit-pvs t])))
-(when (string-match "GNU Emacs" (emacs-version))
+(unless (featurep 'xemacs)
(defvar easy-menu-fast-menus nil)
@@ -253,7 +253,7 @@
(easy-menu-define PVS global-map "PVS menus" pvs-mode-menus))
)
-(when (string-match "XEmacs" (emacs-version))
+(when (featurep 'xemacs)
(add-submenu nil pvs-mode-menus "")
(add-hook 'pvs-mode-hook
'(lambda ()
@@ -293,7 +293,7 @@
(setq index (+ index 1))))
(format "\\b%s\\b" regexp)))
-(when (string-match "GNU Emacs" (emacs-version))
+(unless (featurep 'xemacs)
(add-hook 'pvs-mode-hook
'(lambda ()
(make-local-variable 'font-lock-defaults)
@@ -306,7 +306,7 @@
;;; facep works differently in XEmacs - always returns nil for a symbol
;;; find-face is used there instead, but red and blue faces are already
;;; defined anyway.
-(when (string-match "GNU Emacs" (emacs-version))
+(unless (featurep 'xemacs)
(unless (facep 'red)
(make-face 'red)
(set-face-foreground 'red "red"))
@@ -384,14 +384,12 @@
1 'font-lock-function-name-face)))
"Additional expressions to highlight in PVS mode.")
-(when (and (string-match "GNU Emacs" (emacs-version))
- (not (boundp 'font-lock-maximum-decoration)))
+(unless (or (featurep 'xemacs)
+ (boundp 'font-lock-maximum-decoration))
(defvar font-lock-maximum-decoration nil))
(defconst pvs-font-lock-keywords
- (if (if (string-match "GNU Emacs" (emacs-version))
- font-lock-maximum-decoration
- font-lock-use-maximal-decoration)
+ (if font-lock-maximum-decoration
pvs-font-lock-keywords-2
pvs-font-lock-keywords-1))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-mode.el pvs-4.2/emacs/emacs-src/pvs-mode.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-mode.el 2009-10-04 13:26:58.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-mode.el 2010-01-29 14:53:48.078961193 -0700
@@ -98,10 +98,9 @@
(define-key pvs-mode-map "\e\034" 'prettyprint-region)
(define-key pvs-mode-map "\e\C-q" 'prettyprint-declaration)
(define-key pvs-mode-map "\C-c\C-c" 'pvs-interrupt-subjob)
- (if (string-match "XEmacs" (emacs-version))
+ (if (featurep 'xemacs)
(define-key pvs-mode-map [(shift button2)] 'mouse-show-declaration)
- (if (string-match "GNU Emacs" (emacs-version))
- (define-key pvs-mode-map [S-mouse-2] 'mouse-show-declaration))))
+ (define-key pvs-mode-map [S-mouse-2] 'mouse-show-declaration)))
(defvar pvs-mode-syntax-table nil "Syntax table used while in pvs mode.")
(if pvs-mode-syntax-table ()
@@ -383,7 +382,7 @@
(select-frame (speedbar-current-frame))
(speedbar-with-writable
(dolist (declinfo declsinfo)
- (speedbar-make-tag-line 'statictag ?? nil nil
+ (speedbar-make-tag-line 'statictag ?? nil
declinfo
(car declinfo)
'pvs-speedbar-goto-file
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-prover.el pvs-4.2/emacs/emacs-src/pvs-prover.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-prover.el 2009-05-03 17:49:46.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-prover.el 2010-01-29 14:53:48.079965983 -0700
@@ -59,6 +59,7 @@
;; step-proof -
(eval-when-compile (require 'pvs-macros))
+(require 'cl)
(defvar pvs-in-checker nil
"Indicates whether the proof checker is currently running.
@@ -601,14 +602,13 @@
(save-excursion
(goto-char (point-min))
(while (search-forward "(checkpoint)" nil t)
- (cond ((string-match "GNU Emacs" (emacs-version))
- (replace-match "!!!" nil t)
- (overlay-put (make-overlay (- (point) 3) (point))
- 'face 'font-lock-pvs-checkpoint-face))
- ((string-match "XEmacs" (emacs-version))
+ (cond ((featurep 'xemacs)
(delete-region (match-beginning 0) (match-end 0))
(insert-face "!!!" 'font-lock-pvs-checkpoint-face))
- (t (replace-match "!!!" nil t)))))
+ (t
+ (replace-match "!!!" nil t)
+ (overlay-put (make-overlay (- (point) 3) (point))
+ 'face 'font-lock-pvs-checkpoint-face)))))
(fix-edit-proof-comments)
(setq buffer-modified-p nil)
(goto-char (point-min))
@@ -2078,7 +2078,7 @@
(if (eq (point) (point-max))
(error "At end of buffer")
(let ((start (point)))
- (cond ((string-match "XEmacs" (emacs-version))
+ (cond ((featurep 'xemacs)
(insert-face "!!!" 'font-lock-pvs-checkpoint-face))
(t (insert "!!!")
(overlay-put (make-overlay start (point))
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-prover-helps.el pvs-4.2/emacs/emacs-src/pvs-prover-helps.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-prover-helps.el 2009-02-09 16:14:06.000000000 -0700
+++ pvs-4.2/emacs/emacs-src/pvs-prover-helps.el 2010-01-29 14:53:48.080959872 -0700
@@ -730,7 +730,7 @@
(insert ")")
(return-ilisp)))
-(if (string-match "XEmacs" (emacs-version))
+(if (featurep 'xemacs)
(progn
(defun my-delete-extent (ext dummy)
(delete-extent ext))
@@ -937,11 +937,7 @@
(save-excursion
(set-buffer editprfbuf)
(unless (= (buffer-size) 0)
- (cond ((string-match "GNU Emacs" (emacs-version))
- (let ((beg (point))
- (end (save-excursion (forward-sexp 1) (point))))
- (hilit-proof-region beg end)))
- ((string-match "XEmacs" (emacs-version))
+ (cond ((featurep 'xemacs)
(let ((beg (point))
(end (save-excursion (forward-sexp 1) (point))))
(map-extents 'my-delete-extent (current-buffer) (point-min)
@@ -949,7 +945,11 @@
(set-extent-face (make-extent (point-min) (1- beg))
'completed-proof-steps-face)
(set-extent-face (make-extent beg end)
- 'current-proof-step-face))))))))
+ 'current-proof-step-face)))
+ (t
+ (let ((beg (point))
+ (end (save-excursion (forward-sexp 1) (point))))
+ (hilit-proof-region beg end))))))))
(defun hilit-proof-region (start end)
(delete-hilit-overlays)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-tcl.el pvs-4.2/emacs/emacs-src/pvs-tcl.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-tcl.el 2008-09-07 13:51:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-tcl.el 2010-01-29 14:53:48.080959872 -0700
@@ -35,9 +35,6 @@
(setq tcl-prompt-regexp "^% ")
-;; Set this less than 249 to work around a bug in GNU Emacs 19.24/25.
-(setq comint-input-chunk-size 200)
-
(defvar pvs-wish-cmd "wish"
"The name of the wish binary for PVS.")
@@ -59,7 +56,9 @@
(make-local-variable 'tcl-application)
(setq tcl-application pvs-wish-cmd)
(set-process-filter (get-process "tcl-pvs") 'pvs-tcl-process-filter)
- (process-kill-without-query (get-process "tcl-pvs"))
+ (if (featurep 'xemacs)
+ (process-kill-without-query (get-process "tcl-pvs"))
+ (set-process-query-on-exit-flag (get-process "tcl-pvs") nil))
(setq inferior-tcl-buffer "*tcl-pvs*")
(setq *pvs-tcl-partial-line* "")
;; (comint-setup-ipc)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/pvs-utils.el pvs-4.2/emacs/emacs-src/pvs-utils.el
--- pvs-4.2.ORIG/emacs/emacs-src/pvs-utils.el 2008-09-07 13:51:08.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/pvs-utils.el 2010-01-29 14:53:48.082962225 -0700
@@ -28,6 +28,7 @@
;; --------------------------------------------------------------------
(eval-when-compile (require 'pvs-macros))
+(require 'cl)
(require 'compare-w)
(defvar *pvs-theories* nil)
@@ -287,23 +288,6 @@
(when file
(mapcar 'car (theory-regions)))))
-(defun get-file-buffer (filename)
- "Modified get-file-buffer for correctly handling automount names"
- (if (file-exists-p filename)
- (let ((fbuf nil)
- (attr (file-attributes filename))
- (nname (file-name-nondirectory filename))
- (blist (buffer-list)))
- (while (and (null fbuf) blist)
- (let ((fname (buffer-file-name (car blist))))
- (if (and fname
- (file-exists-p fname)
- (equal (file-name-nondirectory fname) nname)
- (equal attr (file-attributes fname)))
- (setq fbuf (car blist)))
- (setq blist (cdr blist))))
- fbuf)))
-
(defun in-comment-or-string ()
(or (in-comment) (in-string)))
@@ -1221,7 +1205,7 @@
(if (listp abbrevs)
abbrevs
(list abbrevs)))))
- (mapcar '(lambda (a) (fset a cmd)) abbrs)
+ (mapc '(lambda (a) (fset a cmd)) abbrs)
(put cmd 'abbreviations abbrs)))
(defun pvs-get-abbreviation (cmd)
@@ -1448,7 +1432,7 @@
(define-key pvs-query-keymap "!" 'self-insert-and-exit)
(define-key pvs-query-keymap "q" 'self-insert-and-exit)
(define-key pvs-query-keymap "n" 'self-insert-and-exit)
- (unless (string-match "XEmacs" (emacs-version))
+ (unless (featurep 'xemacs)
(define-key pvs-query-keymap "\e" 'self-insert-and-exit))
;;(define-key pvs-query-keymap [help-char] 'self-insert-and-exit)
;;(define-key pvs-query-keymap "\C-g" 'keyboard-quit)
@@ -1831,7 +1815,8 @@
(end1 (save-excursion (set-buffer log1) (point-max)))
(end2 (save-excursion (set-buffer log2) (point-max)))
(dpos (compare-buffer-substrings log1 pos1 end1 log2 pos2 end2))
- (match t))
+ (match t)
+ ipos1 ipos2)
(while (and (/= dpos 0) match)
(setq pos1 (+ (abs dpos) pos1 -1) ipos1 pos1)
(setq pos2 (+ (abs dpos) pos2 -1) ipos2 pos2)
@@ -1981,20 +1966,18 @@
(defun pvs-title-string ()
nil)
-(cond ((string-match "GNU Emacs" (emacs-version))
+(cond ((featurep 'xemacs)
(defun pvs-update-window-titles ()
(let ((title (pvs-title-string)))
(when title
- (modify-frame-parameters (car (frame-list))
- (list (cons 'icon-name title)
- (cons 'title title)))))))
- ((string-match "XEmacs" (emacs-version))
+ (setq frame-title-format title)
+ (setq frame-icon-title-format title)))))
+ (t
(defun pvs-update-window-titles ()
(let ((title (pvs-title-string)))
(when title
- (setq frame-title-format title)
- (setq frame-icon-title-format title)))))
- (t (defun pvs-update-window-titles ()
- nil)))
+ (modify-frame-parameters (car (frame-list))
+ (list (cons 'icon-name title)
+ (cons 'title title))))))))
(add-hook 'change-context-hook 'pvs-update-window-titles)
diff -dur pvs-4.2.ORIG/emacs/emacs-src/tcl.el pvs-4.2/emacs/emacs-src/tcl.el
--- pvs-4.2.ORIG/emacs/emacs-src/tcl.el 2006-07-27 02:09:15.000000000 -0600
+++ pvs-4.2/emacs/emacs-src/tcl.el 2010-01-29 14:53:48.083925934 -0700
@@ -118,19 +118,11 @@
(string-match "^[2-9][0-9]\\." emacs-version))
"Non-nil if using Emacs 19-23 or later.")
-(defconst tcl-using-xemacs-19 (string-match "XEmacs" emacs-version)
+(defconst tcl-using-xemacs-19 (featurep 'xemacs)
"Non-nil if using XEmacs.")
(require 'comint)
-
-;; When compiling under Emacs, load imenu during compilation. If
-;; you have 19.22 or earlier, comment this out, or get imenu.
-(and (fboundp 'eval-when-compile)
- (eval-when-compile
- (if (and (not (string< emacs-version "19.23"))
- (not (string-match "XEmacs" emacs-version)))
- (require 'imenu))
- ()))
+(eval-when-compile (require 'imenu))
(defconst tcl-version "$Revision: 4745 $")
(defconst tcl-maintainer "Tom Tromey <tromey@drip.colorado.edu>")
@@ -828,6 +820,10 @@
(run-hooks 'tcl-mode-hook))
+(defun tcl-last-command-char ()
+ (if (featurep 'xemacs)
+ (event-to-character last-command-event)
+ last-command-event))
;; This is used for braces, brackets, and semi (except for closing
@@ -838,7 +834,7 @@
;; Indent line first; this looks better if parens blink.
(tcl-indent-line)
(self-insert-command arg)
- (if (and tcl-auto-newline (= last-command-char ?\;))
+ (if (and tcl-auto-newline (= (tcl-last-command-char) ?\;))
(progn
(newline)
(tcl-indent-line))))
@@ -862,7 +858,7 @@
;; In auto-newline case, must insert a newline after each
;; brace. So an explicit loop is needed.
(while (> arg 0)
- (insert last-command-char)
+ (insert (tcl-last-command-char))
(tcl-indent-line)
(newline)
(setq arg (1- arg))))
@@ -1970,9 +1966,7 @@
;; Bug reporting.
;;
-(and (fboundp 'eval-when-compile)
- (eval-when-compile
- (require 'reporter)))
+(eval-when-compile (require 'reporter))
(defun tcl-submit-bug-report ()
"Submit via mail a bug report on Tcl mode."
diff -dur pvs-4.2.ORIG/Makefile.in pvs-4.2/Makefile.in
--- pvs-4.2.ORIG/Makefile.in 2010-01-28 15:41:21.455971149 -0700
+++ pvs-4.2/Makefile.in 2010-01-29 14:53:48.084925561 -0700
@@ -132,6 +132,9 @@
: '[^X]*\(X*Emacs [0-9][0-9]\)')
+ifeq ($(emacsversion),Emacs 23)
+EMACSSUBDIR = emacs23
+else
ifeq ($(emacsversion),Emacs 22)
EMACSSUBDIR = emacs22
else
@@ -157,6 +160,7 @@
endif
endif
endif
+endif
endif # end of buildcmds check
diff -dur pvs-4.2.ORIG/pvs.in pvs-4.2/pvs.in
--- pvs-4.2.ORIG/pvs.in 2010-01-28 15:41:21.456969395 -0700
+++ pvs-4.2/pvs.in 2010-01-29 14:53:48.085926529 -0700
@@ -385,7 +385,6 @@
case $PVSEMACS in
*[xl]emacs*) \
- PVSEMACS="LD_ASSUME_KERNEL=${LD_ASSUME_KERNEL} ${PVSEMACS}"
if [ $nobg ] ; then
("$PVSEMACS" $flags -name pvs -in PVS@$HOST -wn PVS@$HOST \
$PVSXINIT $pvsemacsinit )
