rpms/pvs-sbcl/F-12 pvs-4.2-emacs.patch, 1.1, 1.2 pvs-4.2-sbcl.patch, 1.1, 1.2 pvs-sbcl.desktop, 1.1, 1.2 pvs-sbcl.spec, 1.1, 1.2 sources, 1.2, 1.3
Jerry James
jjames at fedoraproject.org
Fri Jan 29 22:12:53 UTC 2010
- Previous message: File pvs-4.2.tar.xz uploaded to lookaside cache by jjames
- Next message: rpms/pvs-sbcl/F-11 pvs-4.2-emacs.patch, 1.1, 1.2 pvs-4.2-sbcl.patch, 1.1, 1.2 pvs-sbcl.desktop, 1.1, 1.2 pvs-sbcl.spec, 1.1, 1.2 sources, 1.2, 1.3
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
Author: jjames
Update of /cvs/pkgs/rpms/pvs-sbcl/F-12
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv11217/F-12
Modified Files:
pvs-4.2-emacs.patch pvs-4.2-sbcl.patch pvs-sbcl.desktop
pvs-sbcl.spec sources
Log Message:
* Fri Jan 29 2010 Jerry James <loganjerry at gmail.com> - 4.2-2.20100126svn
- Update to 20100126 snapshot
- Fix several Emacs bugs, including bz 553023
pvs-4.2-emacs.patch:
Makefile.in | 4 ++
emacs/emacs-src/ilisp/completer.el | 10 ++----
emacs/emacs-src/ilisp/ilcompat.el | 6 ----
emacs/emacs-src/ilisp/ilfsf20.el | 1
emacs/emacs-src/ilisp/ilisp-bat.el | 2 +
emacs/emacs-src/ilisp/ilisp-cl-easy-menu.el | 1
emacs/emacs-src/ilisp/ilisp-cmp.el | 4 +-
emacs/emacs-src/ilisp/ilisp-cmu.el | 3 --
emacs/emacs-src/ilisp/ilisp-dia.el | 4 +-
emacs/emacs-src/ilisp/ilisp-hi.el | 2 +
emacs/emacs-src/ilisp/ilisp-hnd.el | 2 -
emacs/emacs-src/ilisp/ilisp-imenu.el | 6 ++--
emacs/emacs-src/ilisp/ilisp-menu.el | 5 ---
emacs/emacs-src/ilisp/ilisp-mod.el | 2 +
emacs/emacs-src/ilisp/ilisp-mov.el | 2 -
emacs/emacs-src/ilisp/ilisp-out.el | 6 ++--
emacs/emacs-src/ilisp/ilisp-prc.el | 1
emacs/emacs-src/ilisp/ilisp-rng.el | 4 +-
emacs/emacs-src/ilisp/ilisp-utl.el | 5 +++
emacs/emacs-src/ilisp/ilisp-xfr.el | 6 ++--
emacs/emacs-src/pvs-browser.el | 4 +-
emacs/emacs-src/pvs-byte-compile.el | 4 ++
emacs/emacs-src/pvs-cmds.el | 6 ++--
emacs/emacs-src/pvs-ilisp.el | 9 +++---
emacs/emacs-src/pvs-load.el | 10 +++---
emacs/emacs-src/pvs-macros.el | 4 +-
emacs/emacs-src/pvs-menu.el | 16 ++++------
emacs/emacs-src/pvs-mode.el | 7 ++--
emacs/emacs-src/pvs-prover-helps.el | 14 ++++-----
emacs/emacs-src/pvs-prover.el | 14 ++++-----
emacs/emacs-src/pvs-tcl.el | 7 ++--
emacs/emacs-src/pvs-utils.el | 41 ++++++++--------------------
emacs/emacs-src/tcl.el | 24 ++++++----------
pvs.in | 1
34 files changed, 111 insertions(+), 126 deletions(-)
Index: pvs-4.2-emacs.patch
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-12/pvs-4.2-emacs.patch,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- pvs-4.2-emacs.patch 4 Jan 2010 22:18:27 -0000 1.1
+++ pvs-4.2-emacs.patch 29 Jan 2010 22:12:52 -0000 1.2
@@ -1,6 +1,27 @@
+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 2010-01-04 13:30:39.919550709 -0700
-+++ pvs-4.2/emacs/emacs-src/ilisp/ilcompat.el 2010-01-04 13:30:18.847800402 -0700
+--- 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!")
@@ -14,9 +35,300 @@ diff -dur pvs-4.2.ORIG/emacs/emacs-src/i
'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$
+
++(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$
+
+ ;;;%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$
+
+-
++(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$
+
+
+-(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$
+
++(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 at ittc.ku.edu)
++ (cond ((featurep 'xemacs)
++ ;; This code is courtesy Jerry James (loganjerry at 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 2010-01-04 13:30:39.920550469 -0700
-+++ pvs-4.2/emacs/emacs-src/pvs-cmds.el 2010-01-04 13:30:18.848800418 -0700
+--- 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)
@@ -31,9 +343,451 @@ diff -dur pvs-4.2.ORIG/emacs/emacs-src/p
(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$")
+ (defconst tcl-maintainer "Tom Tromey <tromey at 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-04 13:30:39.921550486 -0700
-+++ pvs-4.2/Makefile.in 2010-01-04 13:30:18.849800438 -0700
+--- 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]\)')
@@ -53,8 +807,8 @@ diff -dur pvs-4.2.ORIG/Makefile.in pvs-4
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-04 13:30:39.922550544 -0700
-+++ pvs-4.2/pvs.in 2010-01-04 13:30:18.850800423 -0700
+--- 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
pvs-4.2-sbcl.patch:
Makefile.in | 6
ess/dist-ess.lisp | 4
ess/lang/sb-term/rel/access.lisp | 13 +
ess/lang/sb-term/rel/sb-parser.lisp | 2
ess/lang/sb-term/rel/top.lisp | 4
pvs.in | 13 +
src/WS1S/lisp/dfa-foreign-sbcl.lisp | 275 ++++++++++++++++++++++++++++++++++++
src/defsystem.lisp | 4
src/globals.lisp | 2
src/list-decls.lisp | 4
src/parse.lisp | 4
src/pvs.lisp | 7
src/rahd/cocoa.lisp | 3
src/rahd/opencad.lisp | 5
src/rahd/rahd.lisp | 6
src/status-cmds.lisp | 2
src/utils.lisp | 2
17 files changed, 325 insertions(+), 31 deletions(-)
Index: pvs-4.2-sbcl.patch
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-12/pvs-4.2-sbcl.patch,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- pvs-4.2-sbcl.patch 4 Jan 2010 22:18:27 -0000 1.1
+++ pvs-4.2-sbcl.patch 29 Jan 2010 22:12:52 -0000 1.2
@@ -1,6 +1,6 @@
diff -durN pvs-4.2.ORIG/ess/dist-ess.lisp pvs-4.2/ess/dist-ess.lisp
---- pvs-4.2.ORIG/ess/dist-ess.lisp 2006-09-12 13:46:53.000000000 -0600
-+++ pvs-4.2/ess/dist-ess.lisp 2010-01-01 17:37:56.808727140 -0700
+--- pvs-4.2.ORIG/ess/dist-ess.lisp 2010-01-28 14:02:29.253087714 -0700
++++ pvs-4.2/ess/dist-ess.lisp 2010-01-28 13:56:38.670112938 -0700
@@ -112,8 +112,8 @@
(defun save-ess-lisp (ess-filename features)
@@ -13,8 +13,8 @@ diff -durN pvs-4.2.ORIG/ess/dist-ess.lis
(format t "Now disksaving ... ")
(let ((in-reborn-image-p nil)
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp pvs-4.2/ess/lang/sb-term/rel/access.lisp
---- pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp 2004-12-08 16:07:08.000000000 -0700
-+++ pvs-4.2/ess/lang/sb-term/rel/access.lisp 2010-01-01 17:37:56.809721210 -0700
+--- pvs-4.2.ORIG/ess/lang/sb-term/rel/access.lisp 2010-01-28 14:02:29.253087714 -0700
++++ pvs-4.2/ess/lang/sb-term/rel/access.lisp 2010-01-28 13:56:38.671110580 -0700
@@ -22,11 +22,16 @@
;;(in-package "SB" :nicknames '("SYNTAX-BOX"))
@@ -37,8 +37,8 @@ diff -durN pvs-4.2.ORIG/ess/lang/sb-term
(defparameter *sb-package* (find-package :sb))
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp
---- pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp 2001-06-26 04:46:33.000000000 -0600
-+++ pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp 2010-01-01 17:37:56.810727318 -0700
+--- pvs-4.2.ORIG/ess/lang/sb-term/rel/sb-parser.lisp 2010-01-28 14:02:29.254040118 -0700
++++ pvs-4.2/ess/lang/sb-term/rel/sb-parser.lisp 2010-01-28 13:56:38.672110397 -0700
@@ -8,7 +8,7 @@
(export '( sb-parse ))
@@ -49,8 +49,8 @@ diff -durN pvs-4.2.ORIG/ess/lang/sb-term
(defun sb-parse (&key (nt 'meta-grammar) error-threshold ask-about-bad-tokens
(return-errors nil) (stream nil streamp) string file (exhaust-stream nil))
diff -durN pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp pvs-4.2/ess/lang/sb-term/rel/top.lisp
---- pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp 2009-01-23 14:03:38.000000000 -0700
-+++ pvs-4.2/ess/lang/sb-term/rel/top.lisp 2010-01-01 17:37:56.810727318 -0700
+--- pvs-4.2.ORIG/ess/lang/sb-term/rel/top.lisp 2010-01-28 14:02:29.255082752 -0700
++++ pvs-4.2/ess/lang/sb-term/rel/top.lisp 2010-01-28 13:56:38.673110286 -0700
@@ -29,9 +29,9 @@
(export '(sb sb-make))
@@ -64,8 +64,8 @@ diff -durN pvs-4.2.ORIG/ess/lang/sb-term
(defmacro string-empty? (s)
diff -durN pvs-4.2.ORIG/Makefile.in pvs-4.2/Makefile.in
---- pvs-4.2.ORIG/Makefile.in 2009-07-30 05:12:11.000000000 -0600
-+++ pvs-4.2/Makefile.in 2010-01-01 17:37:56.810727318 -0700
+--- pvs-4.2.ORIG/Makefile.in 2010-01-28 14:02:29.256085875 -0700
++++ pvs-4.2/Makefile.in 2010-01-28 14:02:12.136086081 -0700
@@ -94,7 +94,7 @@
ifneq ($(SBCLISP_HOME),)
@@ -87,8 +87,8 @@ diff -durN pvs-4.2.ORIG/Makefile.in pvs-
cp $(SBCLISPEXE) $(subst $(SYSTEM)-sbclisp,,$@)
cp $(PVSPATH)BDD/$(PLATFORM)/mu.$(LOAD-FOREIGN-EXTENSION) $(subst $(SYSTEM)-sbclisp,,$@)
diff -durN pvs-4.2.ORIG/pvs.in pvs-4.2/pvs.in
---- pvs-4.2.ORIG/pvs.in 2009-10-04 13:36:55.000000000 -0600
-+++ pvs-4.2/pvs.in 2010-01-01 17:37:56.811727227 -0700
+--- pvs-4.2.ORIG/pvs.in 2010-01-28 14:02:29.257083071 -0700
++++ pvs-4.2/pvs.in 2010-01-28 14:02:12.136086081 -0700
@@ -261,9 +261,9 @@
then PVSLISP=cmulisp
elif [ -x $binpath/runtime/pvs-cmulisp ]
@@ -128,8 +128,8 @@ diff -durN pvs-4.2.ORIG/pvs.in pvs-4.2/p
esac
diff -durN pvs-4.2.ORIG/src/defsystem.lisp pvs-4.2/src/defsystem.lisp
---- pvs-4.2.ORIG/src/defsystem.lisp 2009-02-10 14:34:14.000000000 -0700
-+++ pvs-4.2/src/defsystem.lisp 2010-01-01 17:37:56.812764439 -0700
+--- pvs-4.2.ORIG/src/defsystem.lisp 2010-01-28 14:02:29.259088978 -0700
++++ pvs-4.2/src/defsystem.lisp 2010-01-28 13:56:38.677110470 -0700
@@ -1783,6 +1783,10 @@
(push :case-sensitive common-lisp:*features*)
(push :case-insensitive common-lisp:*features*))))
@@ -142,8 +142,8 @@ diff -durN pvs-4.2.ORIG/src/defsystem.li
#+(and allegro case-sensitive ics)
(compiler-type-translation "excl 6.1" "excl-m")
diff -durN pvs-4.2.ORIG/src/globals.lisp pvs-4.2/src/globals.lisp
---- pvs-4.2.ORIG/src/globals.lisp 2009-10-04 12:51:41.000000000 -0600
-+++ pvs-4.2/src/globals.lisp 2010-01-01 17:37:56.813727247 -0700
+--- pvs-4.2.ORIG/src/globals.lisp 2010-01-28 14:02:29.259932686 -0700
++++ pvs-4.2/src/globals.lisp 2010-01-28 13:56:38.678129507 -0700
@@ -293,7 +293,7 @@
;; Used to keep track of which expression have already gone through
@@ -153,21 +153,9 @@ diff -durN pvs-4.2.ORIG/src/globals.lisp
;;; Associate old tcc names with new tccs, so that proofs may be restored.
(defvar *old-tcc-names* nil)
-diff -durN pvs-4.2.ORIG/src/ground-prover/prmacros.lisp pvs-4.2/src/ground-prover/prmacros.lisp
---- pvs-4.2.ORIG/src/ground-prover/prmacros.lisp 2009-10-04 13:18:01.000000000 -0600
-+++ pvs-4.2/src/ground-prover/prmacros.lisp 2010-01-01 17:37:56.813727247 -0700
-@@ -59,7 +59,7 @@
-
- (defconstant-if-unbound *eqarithrels* '(greatereqp lesseqp))
-
--(defconstant *ifops* '(if if*))
-+(defconstant-if-unbound *ifops* '(if if*))
-
- (defconstant-if-unbound *boolconstants* '(false true))
-
diff -durN pvs-4.2.ORIG/src/list-decls.lisp pvs-4.2/src/list-decls.lisp
---- pvs-4.2.ORIG/src/list-decls.lisp 2008-07-17 05:03:22.000000000 -0600
-+++ pvs-4.2/src/list-decls.lisp 2010-01-01 17:55:15.756471800 -0700
+--- pvs-4.2.ORIG/src/list-decls.lisp 2010-01-28 14:02:29.262087873 -0700
++++ pvs-4.2/src/list-decls.lisp 2010-01-28 13:56:38.679110647 -0700
@@ -103,7 +103,7 @@
(pvs-message "~a has not been typechecked" oname)))
@@ -186,10 +174,28 @@ diff -durN pvs-4.2.ORIG/src/list-decls.l
(ppe (let ((theory (get-theory name)))
(when theory
(values (ppe-form theory) (list theory)))))
+diff -durN pvs-4.2.ORIG/src/parse.lisp pvs-4.2/src/parse.lisp
+--- pvs-4.2.ORIG/src/parse.lisp 2010-01-05 02:06:15.000000000 -0700
++++ pvs-4.2/src/parse.lisp 2010-01-28 14:09:48.799985842 -0700
+@@ -1129,12 +1129,12 @@
+ (let ((pos? (is-sop 'POS (term-arg0 rat-term)))
+ (num (ds-number (term-arg1 rat-term))))
+ (when (zerop num)
+- (parse-error ))
++ (parse-error 0 "Ratio with 0 numerator is just 0"))
+ (if (is-sop 'NODEN (term-arg2 rat-term))
+ (if pos? num (- num))
+ (let ((den (ds-number (term-arg2 rat-term))))
+ (when (zerop den)
+- (parse-error ))
++ (parse-error 0 "Cannot have a ratio with 0 denominator"))
+ (if pos? (/ num den) (- (/ num den)))))))
+
+ (defun xt-var-decl (var-decl)
diff -durN pvs-4.2.ORIG/src/pvs.lisp pvs-4.2/src/pvs.lisp
---- pvs-4.2.ORIG/src/pvs.lisp 2009-10-01 03:25:19.000000000 -0600
-+++ pvs-4.2/src/pvs.lisp 2010-01-01 17:51:42.197846781 -0700
-@@ -2129,7 +2129,9 @@
+--- pvs-4.2.ORIG/src/pvs.lisp 2010-01-28 14:02:29.263960488 -0700
++++ pvs-4.2/src/pvs.lisp 2010-01-28 13:56:38.681109867 -0700
+@@ -2143,7 +2143,9 @@
(unproved? (pvs-message "No more unproved formulas below"))
(t (pvs-message
"Not at a formula declaration~@[ - ~a buffer may be invalid~]"
@@ -200,7 +206,7 @@ diff -durN pvs-4.2.ORIG/src/pvs.lisp pvs
(defun prove-formula (theoryname formname rerun?)
(let ((theory (get-typechecked-theory theoryname)))
-@@ -3251,7 +3253,8 @@
+@@ -3265,7 +3267,8 @@
(defun show-strategy (strat-name)
@@ -211,25 +217,28 @@ diff -durN pvs-4.2.ORIG/src/pvs.lisp pvs
(gethash strat-id *steps*)
(gethash strat-id *rules*))))
diff -durN pvs-4.2.ORIG/src/rahd/cocoa.lisp pvs-4.2/src/rahd/cocoa.lisp
---- pvs-4.2.ORIG/src/rahd/cocoa.lisp 2009-02-09 15:35:00.000000000 -0700
-+++ pvs-4.2/src/rahd/cocoa.lisp 2010-01-01 17:37:56.813727247 -0700
-@@ -56,6 +56,7 @@
+--- pvs-4.2.ORIG/src/rahd/cocoa.lisp 2010-01-28 14:02:29.264966823 -0700
++++ pvs-4.2/src/rahd/cocoa.lisp 2010-01-28 14:16:56.317109669 -0700
+@@ -56,7 +56,8 @@
(format cocoa-gb-in cocoa-gb-str))
(#+allegro excl:run-shell-command
#+cmu extensions:run-program
+- "./cocoa-gb.bash")
+ #+sbcl sb-ext:run-program
- "./cocoa-gb.bash")
++ "./cocoa-gb.bash" #+sbcl nil)
(let ((computed-gbasis-lst nil))
(with-open-file (cocoa-gb-out (work-pathify "cocoa-gb.out") :direction :input)
+ (do ((l (read-line cocoa-gb-out) (read-line cocoa-gb-out nil 'eof)))
diff -durN pvs-4.2.ORIG/src/rahd/opencad.lisp pvs-4.2/src/rahd/opencad.lisp
---- pvs-4.2.ORIG/src/rahd/opencad.lisp 2009-02-09 15:35:00.000000000 -0700
-+++ pvs-4.2/src/rahd/opencad.lisp 2010-01-01 17:37:56.814726781 -0700
+--- pvs-4.2.ORIG/src/rahd/opencad.lisp 2010-01-28 14:02:29.264966823 -0700
++++ pvs-4.2/src/rahd/opencad.lisp 2010-01-28 14:16:30.164986452 -0700
@@ -57,10 +57,11 @@
(let ((error-code
(#+allegro excl:run-shell-command
#+cmu extensions:run-program
+- "qepcad.bash")))
+ #+sbcl sb-ext:run-program
- "qepcad.bash")))
++ "qepcad.bash" #+sbcl nil)))
(fmt 10 "~% [CAD] :: Sys-call for QEPCAD.BASH successfull with exit code: ~A. ~%" error-code)
(if #+allegro (= error-code 0)
- #+cmu t ;; Need to learn how to get CMUCL error code here.
@@ -238,19 +247,31 @@ diff -durN pvs-4.2.ORIG/src/rahd/opencad
(let ((cad-decision (read-line cad-output nil)))
(fmt 10 "~% [CAD] :: CAD decision: ~A ; Generic? ~A. ~%" cad-decision generic)
diff -durN pvs-4.2.ORIG/src/rahd/rahd.lisp pvs-4.2/src/rahd/rahd.lisp
---- pvs-4.2.ORIG/src/rahd/rahd.lisp 2009-03-12 05:38:12.000000000 -0600
-+++ pvs-4.2/src/rahd/rahd.lisp 2010-01-01 17:37:56.814726781 -0700
-@@ -133,6 +133,7 @@
+--- pvs-4.2.ORIG/src/rahd/rahd.lisp 2010-01-28 14:02:29.265965379 -0700
++++ pvs-4.2/src/rahd/rahd.lisp 2010-01-28 14:19:29.177984615 -0700
+@@ -66,6 +66,9 @@
+ (defun compile-file-and-load (&rest fnames)
+ (mapcar #'(lambda (fname)
+ (let ((fname-full (format nil "~D.lisp" fname)))
++ #+sbcl
++ (load (compile-file fname-full :verbose t))
++ #-sbcl
+ (compile-file fname-full :load-after-compile t :verbose t)
+ (format t "~%[RAHD-REBOOT]: ~D compiled and loaded successfully." fname-full)))
+ fnames))
+@@ -132,8 +135,7 @@
+ build-name))
(fmt 0 "..... DONE.~%")
(fmt 0 " Marking executable +x .......")
- (#+allegro excl:run-shell-command #+cmu extensions:run-program
-+ #+sbcl sb-ext:run-program
- (format nil "chmod +x ~A.exec" build-name))
+- (#+allegro excl:run-shell-command #+cmu extensions:run-program
+- (format nil "chmod +x ~A.exec" build-name))
++ (pvs::chmod "+x" (format nil "~A.exec" build-name))
(fmt 0 "..... DONE.~%~% >> [RAHD-BUILD-STAND-ALONE]: Process complete.~%"))
t)
+
diff -durN pvs-4.2.ORIG/src/status-cmds.lisp pvs-4.2/src/status-cmds.lisp
---- pvs-4.2.ORIG/src/status-cmds.lisp 2009-10-01 03:21:49.000000000 -0600
-+++ pvs-4.2/src/status-cmds.lisp 2010-01-01 17:55:52.105472232 -0700
+--- pvs-4.2.ORIG/src/status-cmds.lisp 2010-01-28 14:02:29.266965505 -0700
++++ pvs-4.2/src/status-cmds.lisp 2010-01-28 13:56:38.685115340 -0700
@@ -1007,7 +1007,7 @@
(if (and (member origin '("ppe" "tccs") :test #'string=)
(not (get-theory bufname)))
@@ -261,9 +282,9 @@ diff -durN pvs-4.2.ORIG/src/status-cmds.
(decl (get-decl-at line t theories)))
(values (find-if #'(lambda (d) (and (declaration? d)
diff -durN pvs-4.2.ORIG/src/utils.lisp pvs-4.2/src/utils.lisp
---- pvs-4.2.ORIG/src/utils.lisp 2009-10-03 01:06:12.000000000 -0600
-+++ pvs-4.2/src/utils.lisp 2010-01-01 17:37:56.815722776 -0700
-@@ -322,7 +322,7 @@
+--- pvs-4.2.ORIG/src/utils.lisp 2010-01-28 14:02:29.267928254 -0700
++++ pvs-4.2/src/utils.lisp 2010-01-28 13:56:38.686110351 -0700
+@@ -324,7 +324,7 @@
#+sbcl
(defun working-directory ()
@@ -274,7 +295,7 @@ diff -durN pvs-4.2.ORIG/src/utils.lisp p
(defun set-working-directory (dir)
diff -durN pvs-4.2.ORIG/src/WS1S/lisp/dfa-foreign-sbcl.lisp pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp
--- pvs-4.2.ORIG/src/WS1S/lisp/dfa-foreign-sbcl.lisp 1969-12-31 17:00:00.000000000 -0700
-+++ pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp 2010-01-01 17:37:56.816479976 -0700
++++ pvs-4.2/src/WS1S/lisp/dfa-foreign-sbcl.lisp 2010-01-28 13:56:38.687110660 -0700
@@ -0,0 +1,275 @@
+;; --------------------------------------------------------------------
+;; PVS
Index: pvs-sbcl.desktop
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-12/pvs-sbcl.desktop,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- pvs-sbcl.desktop 4 Jan 2010 22:18:27 -0000 1.1
+++ pvs-sbcl.desktop 29 Jan 2010 22:12:52 -0000 1.2
@@ -6,6 +6,6 @@ GenericName=PVS
Comment=An interactive theorem prover
TryExec=pvs-sbcl
Exec=pvs-sbcl %F
-MimeType=image/x-pvs;
+MimeType=application/x-pvs;
Terminal=false
Categories=Application;Development
Index: pvs-sbcl.spec
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-12/pvs-sbcl.spec,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- pvs-sbcl.spec 4 Jan 2010 22:18:27 -0000 1.1
+++ pvs-sbcl.spec 29 Jan 2010 22:12:53 -0000 1.2
@@ -1,6 +1,6 @@
Name: pvs-sbcl
Version: 4.2
-Release: 2.20100104svn%{?dist}
+Release: 2.20100126svn%{?dist}
Summary: Interactive theorem prover from SRI
Group: Applications/Engineering
@@ -9,7 +9,7 @@ URL: http://pvs.csl.sri.com/
# SBCL support is only available in the post-4.2 release subversion repository.
# Use the following commands to generate the source tarball corresponding to
# this release:
-# svn export -r 5482 https://spartan.csl.sri.com/svn/public/pvs/trunk pvs-4.2
+# svn export -r 5502 https://spartan.csl.sri.com/svn/public/pvs/trunk pvs-4.2
# tar cf pvs-4.2.tar pvs-4.2
# xz pvs-4.2.tar
Source0: pvs-4.2.tar.xz
@@ -48,7 +48,7 @@ BuildRequires: autoconf, sbcl, texinfo-
BuildRequires: emacs, emacs-el, xemacs-devel, xemacs-packages-extra
BuildRequires: desktop-file-utils
Requires: sbcl = 1.0.30, tex(latex)
-Requires(postun): desktop-file-utils
+Requires(postun): desktop-file-utils, tex(tex)
Provides: pvs = %{version}-%{release}, pvsio = %{version}-%{release}
# Fedora SBCL is only available on Intel platforms
@@ -80,6 +80,17 @@ autoconf
%configure CFLAGS="$RPM_OPT_FLAGS -fPIC -fno-strict-aliasing"
make SBCLISP_HOME=%{_bindir}
+# We don't want the empty emacs19 directory
+rm -fr emacs/emacs19
+
+# And we also want to compile with XEmacs
+mkdir emacs/xemacs21
+pushd emacs/xemacs21
+ln -sf ../emacs-src/*.el .
+ln -sf ../emacs-src/ilisp/*.el .
+%{_bindir}/xemacs -batch -l pvs-byte-compile.el
+popd
+
# Now that we're done building, we don't want the devel version
rm -fr bin/*/devel
@@ -174,6 +185,10 @@ update-desktop-database %{_datadir}/appl
%{_datadir}/texmf/tex/latex/pvs
%changelog
+* Fri Jan 29 2010 Jerry James <loganjerry at gmail.com> - 4.2-2.20100126svn
+- Update to 20100126 snapshot
+- Fix several Emacs bugs, including bz 553023
+
* Mon Jan 4 2010 Jerry James <loganjerry at gmail.com> - 4.2-2.20100104svn
- Update to 20100104 snapshot.
- Fix mona patch.
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/pvs-sbcl/F-12/sources,v
retrieving revision 1.2
retrieving revision 1.3
diff -u -p -r1.2 -r1.3
--- sources 4 Jan 2010 22:18:28 -0000 1.2
+++ sources 29 Jan 2010 22:12:53 -0000 1.3
@@ -1,5 +1,5 @@
9646a3fa12ae6112c4ddd17e4a14c846 csl-93-9.ps.gz
6fd7d301fb569cacb8aa9fb6278498a8 csl-97-2.ps.gz
3c763226529517d39dfb962628492ec2 interpretations.pdf
-df79d45152a96953801ab2c5ca8d7741 pvs-4.2.tar.xz
+bb52e6b3dbf8bd4fbc58da635236de3e pvs-4.2.tar.xz
432c4e35d4b172b227c2c3dbe0afb6a6 pvs-prelude.pdf
- Previous message: File pvs-4.2.tar.xz uploaded to lookaside cache by jjames
- Next message: rpms/pvs-sbcl/F-11 pvs-4.2-emacs.patch, 1.1, 1.2 pvs-4.2-sbcl.patch, 1.1, 1.2 pvs-sbcl.desktop, 1.1, 1.2 pvs-sbcl.spec, 1.1, 1.2 sources, 1.2, 1.3
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the scm-commits
mailing list