Author: amdunn
Update of /cvs/pkgs/rpms/emacs-common-proofgeneral/F-10
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv11507/F-10
Modified Files:
.cvsignore sources
Added Files:
emacs-common-proofgeneral.spec import.log
pg-3.7.1-Makefile.patch pg-3.7.1-startscript.patch
pg-3.7.1-xemacs-display-table.patch
Log Message:
* Wed Jul 29 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-4
- Incorporated comments from Jerry James about applying his patch:
patch now applied unconditionally (regardless of Fedora version
which was used as a somewhat imperfect way to control XEmacs
version).
- Patch descriptions moved upward in spec file in accordance with
examples in guidelines.
* Thu Jul 09 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-3
- Added xemacs patch that fixes compilation problems for X-Symbol code.
* Thu Jul 02 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-2
- Excluded bundled X-symbol, mmm-mode.
- Changed requires for these bundled packages.
* Tue Apr 07 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-1
- Initial Fedora RPM.
--- NEW FILE emacs-common-proofgeneral.spec ---
# Patches described below with the patch commands
%define pkg proofgeneral
# Check version defaults
# If the emacs-el package has installed a pkgconfig file, use that to
# determine install locations and Emacs version at build time, otherwise
# set defaults.
%if %($(pkg-config emacs) ; echo $?)
%define emacs_version 22.1
%define emacs_lispdir %{_datadir}/emacs/site-lisp
%define emacs_startdir %{_datadir}/emacs/site-lisp/site-start.d
%else
%define emacs_version %(pkg-config emacs --modversion)
%define emacs_lispdir %(pkg-config emacs --variable sitepkglispdir)
%define emacs_startdir %(pkg-config emacs --variable sitestartdir)
%endif
# If the xemacs-devel package has installed a pkgconfig file, use that
# to determine install locations and Emacs version at build time,
# otherwise set defaults.
%if %($(pkg-config xemacs) ; echo $?)
%define xemacs_version 21.5
%define xemacs_lispdir %{_datadir}/xemacs/site-packages/lisp
%define xemacs_startdir %{_datadir}/xemacs/site-packages/lisp/site-start.d
%else
%define xemacs_version %(pkg-config xemacs --modversion)
%define xemacs_lispdir %(pkg-config xemacs --variable sitepkglispdir)
%define xemacs_startdir %(pkg-config xemacs --variable sitestartdir)
%endif
Name: emacs-common-%{pkg}
Version: 3.7.1
Release: 4%{?dist}
Summary: Emacs mode for standard interaction interface for proof assistants
Group: Applications/Editors
License: GPLv2
URL: http://proofgeneral.inf.ed.ac.uk/
Source0: http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-%{version}.tgz
# Patch 0 - Fedora specific, don't do an "install-info" in the make process
# (which would occur at build time), but instead put it into a scriptlet
Patch0: pg-3.7.1-Makefile.patch
# Patch 1 - Somewhat Fedora specific, patches Proof General starting
# script to include values of build time generated variables (which
# are inserted in the build process with sed) instead of its way of
# getting this information. Also moves around some script parts related
# to emacs version detection.
Patch1: pg-3.7.1-startscript.patch
# Patch 2 - Display tables were changed in XEmacs 21.5.29 in a way
# that breaks ProofGeneral's X-Symbol code unless changes are made
# Incorporating a patch here from Jerry James. (Of course, right now
# the X-Symbol code is disabled as X-Symbol isn't packaged and
# ProofGeneral makes changes to the X-Symbol code that would have to
# be included somehow anyway, but ProofGeneral's X-Symbol code could
# be activated in the future and the change is necessary to allow the
# code to be byte-compiled).
Patch2: pg-3.7.1-xemacs-display-table.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildArch: noarch
BuildRequires: emacs emacs-el xemacs xemacs-devel texinfo-tex xemacs-packages-extra
%description
Proof General is a generic front-end for proof assistants (also known
as interactive theorem provers) based on Emacs.
Proof General allows one to edit and submit a proof script to a proof
assistant in an interactive manner:
- It tracks the goal state, and the script as it is submitted, and
allows for easy backtracking and block execution.
- It adds toolbars and menus to Emacs for easy access to proof
assistant features.
- It integrates with X-Symbol for some provers to provide output using
proper mathematical symbols.
- It includes utilities for generating Emacs tags for proof scripts,
allowing for easy navigation.
Proof General supports a number of different proof assistants
(Isabelle, Coq, PhoX, and LEGO to name a few) and is designed to be
easily extendable to work with others.
%package -n emacs-%{pkg}
Summary: Compiled elisp files to run Proof General under GNU Emacs
Group: Applications/Editors
Requires: emacs(bin) >= %{emacs_version}
Requires: emacs-common-%{pkg} = %{version}-%{release}
# MMM Mode is separately packaged for emacs (but not for XEmacs)
Requires: emacs-mmm
%description -n emacs-%{pkg}
Proof General is a generic front-end for proof assistants based on Emacs.
This package contains the byte compiled elisp packages to run Proof
General with GNU Emacs.
%package -n emacs-%{pkg}-el
Summary: Elisp source files for Proof General under GNU Emacs
Group: Applications/Editors
Requires: emacs-%{pkg} = %{version}-%{release}
%description -n emacs-%{pkg}-el
This package contains the elisp source files for Proof General under
GNU Emacs. You do not need to install this package to run Proof
General. Install the emacs-%{pkg} package to use Proof General with
GNU Emacs.
%package -n xemacs-%{pkg}
Summary: Compiled elisp files to run Proof General under XEmacs
Group: Applications/Editors
Requires: xemacs(bin) >= %{xemacs_version}
Requires: emacs-common-%{pkg} = %{version}-%{release}
# For MMM mode (and X-Symbol, whose use in this package currently
# doesn't work - disabled until X-Symbol can be separately packaged)
Requires: xemacs-packages-extra
%description -n xemacs-%{pkg}
Proof General is a generic front-end for proof assistants based on Emacs.
This package contains the byte compiled elisp packages to run Proof
General with XEmacs.
%package -n xemacs-%{pkg}-el
Summary: Elisp source files for Proof General under XEmacs
Group: Applications/Editors
Requires: emacs-%{pkg} = %{version}-%{release}
%description -n xemacs-%{pkg}-el
This package contains the elisp source files for Proof General under
XEmacs. You do not need to install this package to run Proof
General. Install the xemacs-%{pkg} package to use Proof General with
XEmacs.
%prep
%setup -q -n ProofGeneral-%{version}
%patch0
%patch1
%patch2 -p1
%build
# Fix rpmlint complaints:
# Correct permissions for isartags script
chmod 755 isar/isartags
# Correct permissions for x-symbol ChangeLog
chmod 644 x-symbol/lisp/ChangeLog
# Correct permissions for x-symbol Makefile
chmod 644 x-symbol/etc/fonts/Makefile
# Remove .cvsignore file
rm images/gimp/.cvsignore
# Fix non UTF-8 documentation and theory files
# File listing taken from the Makefile
%define doc_files AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
for f in `find %{doc_files}`; do mv $f $f.old && iconv -f iso-8859-1 -t utf8 < $f.old > $f && rm $f.old; done
# Make full copies of emacs and xemacs versions, set options in the proofgeneral start script
make clean
make EMACS=emacs compile bashscripts perlscripts doc
sed -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{emacs_lispdir}|' -e 's|^XEMACS_LISPDIR=.*$|XEMACS_LISPDIR=%{xemacs_lispdir}|' -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' < bin/proofgeneral > .tmp && cat .tmp > bin/proofgeneral
mkdir emacs
for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs`; do cp -pr $f emacs/$f; done
make clean
make EMACS=xemacs compile bashscripts perlscripts doc
sed -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{emacs_lispdir}|' -e 's|^XEMACS_LISPDIR=.*$|XEMACS_LISPDIR=%{xemacs_lispdir}|' -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' < bin/proofgeneral > .tmp && cat .tmp > bin/proofgeneral
mkdir xemacs
for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs ! -name xemacs`; do cp -pr $f xemacs/$f; done
%install
rm -rf %{buildroot}
%define full_doc_dir %{_datadir}/doc/%{pkg}
%define full_man_dir %{_mandir}/man1
%define full_data_dir %{_datadir}/%{pkg}
%define doc_options DOCDIR=%{buildroot}%{full_doc_dir} MANDIR=%{buildroot}%{full_man_dir} INFODIR=%{buildroot}%{_infodir}
%define common_options PREFIX=%{buildroot}%{_prefix} DEST_PREFIX=%{_prefix} DESKTOP=%{buildroot}%{full_data_dir} BINDIR=%{buildroot}%{_bindir} %{doc_options}
%define emacs_options ELISP_START=%{buildroot}%{emacs_startdir} ELISP=%{buildroot}%{emacs_lispdir}/%{pkg} DEST_ELISP=%{emacs_lispdir}/%{pkg}
%define xemacs_options ELISP_START=%{buildroot}%{xemacs_startdir} ELISP=%{buildroot}%{xemacs_lispdir}/%{pkg} DEST_ELISP=%{xemacs_lispdir}/%{pkg}
cp -pr `find xemacs/ -maxdepth 1 -mindepth 1` .
make EMACS=xemacs %{common_options} %{xemacs_options} install install-doc
cp -pr `find emacs/ -maxdepth 1 -mindepth 1` .
make EMACS=emacs %{common_options} %{emacs_options} install install-doc
# Don't accidentally install an infodir file over an existing one
rm -f %{buildroot}%{_infodir}/dir
%clean
rm -rf %{buildroot}
%post
/sbin/install-info %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
/sbin/install-info %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
%preun
if [ $1 -eq 0 ]; then
/sbin/install-info --delete %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
/sbin/install-info --delete %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
fi
%files
%defattr(-,root,root,-)
%{full_doc_dir}
%{full_data_dir}
%{full_man_dir}/*
%{_infodir}/*
%{_bindir}/*
%files -n emacs-%{pkg}
%defattr(-,root,root,-)
%{emacs_lispdir}/%{pkg}/*
# Exclude bundled X-symbol, which should be separately packaged but
# is not critical for the core functionality of the package
%exclude %{emacs_lispdir}/%{pkg}/x-symbol
# Exclude bundled mmm-mode, packaged separately
%exclude %{emacs_lispdir}/%{pkg}/mmm
%exclude %{emacs_lispdir}/%{pkg}/*/*.el
%{emacs_startdir}/*.el
%dir %{emacs_lispdir}/%{pkg}
%files -n emacs-%{pkg}-el
%defattr(-,root,root,-)
%{emacs_lispdir}/%{pkg}/*/*.el
%files -n xemacs-%{pkg}
%defattr(-,root,root,-)
%{xemacs_lispdir}/%{pkg}/*
# Exclude bundled X-symbol, which should be separately packaged but
# is not critical for the core functionality of the package
%exclude %{xemacs_lispdir}/%{pkg}/x-symbol
# Exclude bundled mmm-mode, packaged separately
%exclude %{xemacs_lispdir}/%{pkg}/mmm
%exclude %{xemacs_lispdir}/%{pkg}/*/*.el
%{xemacs_startdir}/*.el
%dir %{xemacs_lispdir}/%{pkg}
%files -n xemacs-%{pkg}-el
%defattr(-,root,root,-)
%{xemacs_lispdir}/%{pkg}/*/*.el
%changelog
* Wed Jul 29 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-4
- Incorporated comments from Jerry James about applying his patch:
patch now applied unconditionally (regardless of Fedora version
which was used as a somewhat imperfect way to control XEmacs
version).
- Patch descriptions moved upward in spec file in accordance with
examples in guidelines.
* Thu Jul 09 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-3
- Added xemacs patch that fixes compilation problems for X-Symbol code.
* Thu Jul 02 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-2
- Excluded bundled X-symbol, mmm-mode.
- Changed requires for these bundled packages.
* Tue Apr 07 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-1
- Initial Fedora RPM.
--- NEW FILE import.log ---
emacs-common-proofgeneral-3_7_1-4_fc10:F-10:emacs-common-proofgeneral-3.7.1-4.fc10.src.rpm:1249079805
pg-3.7.1-Makefile.patch:
Makefile | 2 --
1 file changed, 2 deletions(-)
--- NEW FILE pg-3.7.1-Makefile.patch ---
--- Makefile 2009-01-27 21:22:49.000000000 -0500
+++ Makefile 2009-01-27 21:23:26.000000000 -0500
@@ -215,8 +215,6 @@
cp -pf doc/proofgeneral.1 ${MANDIR}
mkdir -p ${INFODIR}
cp -pf doc/*.info ${INFODIR}
- /sbin/install-info ${INFODIR}/ProofGeneral.info* ${INFODIR}/dir
- /sbin/install-info ${INFODIR}/PG-adapting.info* ${INFODIR}/dir
mkdir -p ${DOCDIR}
for f in ${DOC_FILES}; do cp -pf $$f ${DOCDIR}; done
for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; cp -pf $$f ${DOCDIR}/$$f; done
pg-3.7.1-startscript.patch:
proofgeneral | 50 +++++++++++++++++++++++++++++---------------------
1 file changed, 29 insertions(+), 21 deletions(-)
--- NEW FILE pg-3.7.1-startscript.patch ---
--- bin/proofgeneral 2009-02-04 06:03:47.000000000 -0500
+++ bin/proofgeneral 2009-02-04 07:24:42.000000000 -0500
@@ -15,31 +15,18 @@
#
# proofgeneral,v 9.6 2008/07/19 16:10:12 da Exp
#
+# Additional edits for Fedora made by Alan Dunn (parts of script
+# also rearranged)
+
+# Fedora extra variables
+EMACS_LISPDIR=
+XEMACS_LISPDIR=
+PACKAGE=
# The default path should work if you are using the Proof General RPM
# or unpack Proof General in your home directory. Otherwise edit below.
# NB: no trailing backslash here!
-PGHOMEDEFAULT=$HOME/ProofGeneral
-
-# Try to find a default Emacs executable
-if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
- if which emacs > /dev/null; then
- EMACS=`which emacs`
- else
- EMACS=`which xemacs`
- fi
-fi
-
-# Try to find Proof General directory
-if [ -d $PGHOMEDEFAULT ]; then
- PGHOME=$PGHOMEDEFAULT
-elif [ -d /usr/share/${EMACSVERSION}/site-lisp/proofgeneral ]; then
- PGHOME=/usr/share/${EMACSVERSION}/site-lisp/proofgeneral
-else
- echo "Cannot find the Proof General lisp files: please edit script to set PGHOMEDEFAULT correctly."
- exit 1
-fi
-
+PGHOMEDEFAULT=/usr/share/emacs/site-lisp/${PACKAGE}
NAME=`basename $0`
@@ -98,6 +85,15 @@
esac
do shift; done
+# Try to find a default Emacs executable
+if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
+ if which emacs > /dev/null; then
+ EMACS=`which emacs`
+ else
+ EMACS=`which xemacs`
+ fi
+fi
+
if [ ! -x "$EMACS" ]; then
echo "$NAME: cannot find an Emacs or XEmacs executable. Set EMACS or your PATH." 1>&2
exit 1
@@ -105,6 +101,18 @@
EMACSVERSION=`basename $EMACS`
+# Try to find Proof General directory
+if [ -d $PGHOMEDEFAULT ]; then
+ PGHOME=$PGHOMEDEFAULT
+elif [[ $EMACSVERSION == emacs && -d ${EMACS_LISPDIR}/${PACKAGE} ]]; then
+ PGHOME=${EMACS_LISPDIR}/${PACKAGE}
+elif [[ $EMACSVERSION == xemacs && -d ${XEMACS_LISPDIR}/${PACKAGE} ]]; then
+ PGHOME=${XEMACS_LISPDIR}/${PACKAGE}
+else
+ echo "Cannot find the Proof General lisp files: please edit script to set PGHOMEDEFAULT correctly."
+ exit 1
+fi
+
# Deal with UTF issue
if [ `locale | grep LC_CTYPE | grep UTF` ]; then
echo "Warning: detected Unicode LC_CTYPE setting, switched back to C"
pg-3.7.1-xemacs-display-table.patch:
Makefile | 2 -
generic/pg-display-table.el | 46 +++++++++++++++++++++++++++++++++++++++
generic/proof-shell.el | 3 +-
phox/phox-sym-lock.el | 10 +++++---
x-symbol/lisp/x-symbol-nomule.el | 6 ++---
x-symbol/lisp/x-symbol.el | 3 +-
6 files changed, 59 insertions(+), 11 deletions(-)
--- NEW FILE pg-3.7.1-xemacs-display-table.patch ---
diff -durN ProofGeneral-3.7.1.ORIG/generic/pg-display-table.el ProofGeneral-3.7.1/generic/pg-display-table.el
--- ProofGeneral-3.7.1.ORIG/generic/pg-display-table.el 1969-12-31 19:00:00.000000000 -0500
+++ ProofGeneral-3.7.1/generic/pg-display-table.el 2009-07-09 12:49:34.923843082 -0400
@@ -0,0 +1,46 @@
+;; pg-display-table.el --- Wrapper functions for display-table vectors and
+;; objects.
+;;
+;; Copyright (C) 2009 LFCS Edinburgh.
+;; Author: Jerry James
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; pg-display-table.el,v 1.0 2009/07/06 16:07:09 da Exp
+;;
+;;
+;;; Commentary:
+;;
+;; This file hides the differences between display-tables that are represented
+;; as vectors and recent XEmacs display-tables, which are objects.
+
+;;; Code:
+
+(require 'disp-table)
+
+(defmacro defun-when-void (&rest args)
+ "Define a function, just like `defun', unless it's already defined.
+Used for compatibility among different emacs variants."
+ `(if (fboundp ',(car args))
+ nil
+ (defun ,@args)))
+
+(defun-when-void put-display-table (range value display-table)
+ "Set the value for char RANGE to VALUE in DISPLAY-TABLE."
+ (if (sequencep display-table)
+ (aset display-table range value)
+ (put-char-table range value display-table)))
+
+(defun-when-void get-display-table (character display-table)
+ "Find value for CHARACTER in DISPLAY-TABLE."
+ (if (sequencep display-table)
+ (aref display-table character)
+ (get-char-table character display-table)))
+
+(defun-when-void fill-display-table (value display-table)
+ "Map every entry in the table to VALUE."
+ (if (sequencep display-table)
+ (fillarray display-table value)
+ (put-char-table t value display-table)))
+
+(provide 'pg-display-table)
+;;; pg-display-table.el ends here
diff -durN ProofGeneral-3.7.1.ORIG/generic/proof-shell.el ProofGeneral-3.7.1/generic/proof-shell.el
--- ProofGeneral-3.7.1.ORIG/generic/proof-shell.el 2008-07-10 08:49:32.000000000 -0400
+++ ProofGeneral-3.7.1/generic/proof-shell.el 2009-07-09 12:49:34.948238190 -0400
@@ -16,6 +16,7 @@
(require 'proof-utils))
(require 'proof-autoloads)
+(require 'pg-display-table)
(require 'pg-response)
(require 'pg-goals)
(require 'proof-script)
@@ -1695,7 +1696,7 @@
(let ((disp (make-display-table))
(i 128))
(while (< i 256)
- (aset disp i [])
+ (put-display-table i [] disp)
(incf i))
(cond ((featurep 'xemacs)
(add-spec-to-specifier current-display-table disp (current-buffer)))
diff -durN ProofGeneral-3.7.1.ORIG/Makefile ProofGeneral-3.7.1/Makefile
--- ProofGeneral-3.7.1.ORIG/Makefile 2008-01-31 08:06:38.000000000 -0500
+++ ProofGeneral-3.7.1/Makefile 2009-07-09 13:16:35.366276826 -0400
@@ -86,8 +86,6 @@
@echo " Byte compiling... "
@echo "****************************************************************"
make elc
- @echo " Byte compiling X-Symbol..."
- (cd x-symbol/lisp; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
echo $(EMACS) > $(@)
@echo "****************************************************************"
@echo " Finished."
diff -durN ProofGeneral-3.7.1.ORIG/phox/phox-sym-lock.el ProofGeneral-3.7.1/phox/phox-sym-lock.el
--- ProofGeneral-3.7.1.ORIG/phox/phox-sym-lock.el 2008-01-30 10:22:21.000000000 -0500
+++ ProofGeneral-3.7.1/phox/phox-sym-lock.el 2009-07-09 12:49:35.065515654 -0400
@@ -28,6 +28,7 @@
;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*'
(require 'font-lock)
+(require 'pg-display-table)
(if (featurep 'xemacs)
(require 'atomic-extents)) ;; not available on GNU Emacs
@@ -223,9 +224,10 @@
(let* ((name (phox-sym-lock-gen-symbol "face"))
(table (make-display-table))
(tface (make-face name "phox-sym-lock-remap-face" t)))
- (fillarray table "")
- (aset table (string-to-char (substring pat (1- pos) pos))
- (phox-sym-lock-translate-char-or-string obj))
+ (fill-display-table "" table)
+ (put-display-table (string-to-char (substring pat (1- pos) pos))
+ (phox-sym-lock-translate-char-or-string obj)
+ table)
(set-face-foreground tface (if (and (boundp 'font-lock-use-fonts)
font-lock-use-fonts)
(face-foreground 'default) phox-sym-lock-color))
@@ -240,7 +242,7 @@
(let* ((name (phox-sym-lock-gen-symbol "face"))
(table (make-display-table))
(tface (make-face name "phox-sym-lock-remap-face" t)))
- (fillarray table "")
+ (fill-display-table "" table)
(set-face-property tface 'display-table table)
(set-face-property tface 'phox-sym-lock-remap 1) ; mark it
tface
diff -durN ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol.el ProofGeneral-3.7.1/x-symbol/lisp/x-symbol.el
--- ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol.el 2008-07-18 12:10:30.000000000 -0400
+++ ProofGeneral-3.7.1/x-symbol/lisp/x-symbol.el 2009-07-09 12:49:35.115921558 -0400
@@ -39,6 +39,7 @@
(provide 'x-symbol)
;;(require 'x-symbol-hooks)
(require 'x-symbol-vars)
+(require 'pg-display-table)
(require (if (featurep 'mule) 'x-symbol-mule 'x-symbol-nomule))
(eval-when-compile (require 'x-symbol-macs))
(eval-when-compile (require 'cl))
@@ -1612,7 +1613,7 @@
(let ((table (make-display-table))
(i 0))
(while (< i 256)
- (aset table i "")
+ (put-display-table i "" table)
(setq i (1+ i)))
table)
"Internal variable. Display table for `x-symbol-invisible-face'.")
diff -durN ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol-nomule.el ProofGeneral-3.7.1/x-symbol/lisp/x-symbol-nomule.el
--- ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol-nomule.el 2008-01-30 10:22:26.000000000 -0500
+++ ProofGeneral-3.7.1/x-symbol/lisp/x-symbol-nomule.el 2009-07-09 12:49:35.156890261 -0400
@@ -33,6 +33,7 @@
(error "This file is meant to be used with XEmacs/no-Mule"))
(provide 'x-symbol-nomule)
(require 'x-symbol-hooks)
+(require 'pg-display-table)
(eval-when-compile (require 'x-symbol)) ; x-symbol also requires this file
;;(eval-when-compile
;; (defvar x-symbol-encode-rchars)
@@ -80,11 +81,10 @@
"Internal. Face to fontify current font-lock match.")
(defvar x-symbol-nomule-display-table
- ;; display-table via characters table is not implemented in XEmacs yet...
- (let ((table (make-vector 256 nil))
+ (let ((table (make-display-table))
(i 128))
(while (< i 160)
- (aset table i "")
+ (put-display-table i "" table)
(incf i))
table)
"Display table in faces with non-standard charset registry.
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/emacs-common-proofgeneral/F-10/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- .cvsignore 31 Jul 2009 21:14:21 -0000 1.1
+++ .cvsignore 31 Jul 2009 22:50:22 -0000 1.2
@@ -0,0 +1 @@
+ProofGeneral-3.7.1.tgz
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/emacs-common-proofgeneral/F-10/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- sources 31 Jul 2009 21:14:21 -0000 1.1
+++ sources 31 Jul 2009 22:50:23 -0000 1.2
@@ -0,0 +1 @@
+eebfff672b5941823fe893075316b02e ProofGeneral-3.7.1.tgz
Author: amdunn
Update of /cvs/pkgs/rpms/emacs-common-proofgeneral/F-11
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv9951/F-11
Modified Files:
.cvsignore sources
Added Files:
emacs-common-proofgeneral.spec import.log
pg-3.7.1-Makefile.patch pg-3.7.1-startscript.patch
pg-3.7.1-xemacs-display-table.patch
Log Message:
* Wed Jul 29 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-4
- Incorporated comments from Jerry James about applying his patch:
patch now applied unconditionally (regardless of Fedora version
which was used as a somewhat imperfect way to control XEmacs
version).
- Patch descriptions moved upward in spec file in accordance with
examples in guidelines.
* Thu Jul 09 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-3
- Added xemacs patch that fixes compilation problems for X-Symbol code.
* Thu Jul 02 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-2
- Excluded bundled X-symbol, mmm-mode.
- Changed requires for these bundled packages.
* Tue Apr 07 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-1
- Initial Fedora RPM.
--- NEW FILE emacs-common-proofgeneral.spec ---
# Patches described below with the patch commands
%define pkg proofgeneral
# Check version defaults
# If the emacs-el package has installed a pkgconfig file, use that to
# determine install locations and Emacs version at build time, otherwise
# set defaults.
%if %($(pkg-config emacs) ; echo $?)
%define emacs_version 22.1
%define emacs_lispdir %{_datadir}/emacs/site-lisp
%define emacs_startdir %{_datadir}/emacs/site-lisp/site-start.d
%else
%define emacs_version %(pkg-config emacs --modversion)
%define emacs_lispdir %(pkg-config emacs --variable sitepkglispdir)
%define emacs_startdir %(pkg-config emacs --variable sitestartdir)
%endif
# If the xemacs-devel package has installed a pkgconfig file, use that
# to determine install locations and Emacs version at build time,
# otherwise set defaults.
%if %($(pkg-config xemacs) ; echo $?)
%define xemacs_version 21.5
%define xemacs_lispdir %{_datadir}/xemacs/site-packages/lisp
%define xemacs_startdir %{_datadir}/xemacs/site-packages/lisp/site-start.d
%else
%define xemacs_version %(pkg-config xemacs --modversion)
%define xemacs_lispdir %(pkg-config xemacs --variable sitepkglispdir)
%define xemacs_startdir %(pkg-config xemacs --variable sitestartdir)
%endif
Name: emacs-common-%{pkg}
Version: 3.7.1
Release: 4%{?dist}
Summary: Emacs mode for standard interaction interface for proof assistants
Group: Applications/Editors
License: GPLv2
URL: http://proofgeneral.inf.ed.ac.uk/
Source0: http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-%{version}.tgz
# Patch 0 - Fedora specific, don't do an "install-info" in the make process
# (which would occur at build time), but instead put it into a scriptlet
Patch0: pg-3.7.1-Makefile.patch
# Patch 1 - Somewhat Fedora specific, patches Proof General starting
# script to include values of build time generated variables (which
# are inserted in the build process with sed) instead of its way of
# getting this information. Also moves around some script parts related
# to emacs version detection.
Patch1: pg-3.7.1-startscript.patch
# Patch 2 - Display tables were changed in XEmacs 21.5.29 in a way
# that breaks ProofGeneral's X-Symbol code unless changes are made
# Incorporating a patch here from Jerry James. (Of course, right now
# the X-Symbol code is disabled as X-Symbol isn't packaged and
# ProofGeneral makes changes to the X-Symbol code that would have to
# be included somehow anyway, but ProofGeneral's X-Symbol code could
# be activated in the future and the change is necessary to allow the
# code to be byte-compiled).
Patch2: pg-3.7.1-xemacs-display-table.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildArch: noarch
BuildRequires: emacs emacs-el xemacs xemacs-devel texinfo-tex xemacs-packages-extra
%description
Proof General is a generic front-end for proof assistants (also known
as interactive theorem provers) based on Emacs.
Proof General allows one to edit and submit a proof script to a proof
assistant in an interactive manner:
- It tracks the goal state, and the script as it is submitted, and
allows for easy backtracking and block execution.
- It adds toolbars and menus to Emacs for easy access to proof
assistant features.
- It integrates with X-Symbol for some provers to provide output using
proper mathematical symbols.
- It includes utilities for generating Emacs tags for proof scripts,
allowing for easy navigation.
Proof General supports a number of different proof assistants
(Isabelle, Coq, PhoX, and LEGO to name a few) and is designed to be
easily extendable to work with others.
%package -n emacs-%{pkg}
Summary: Compiled elisp files to run Proof General under GNU Emacs
Group: Applications/Editors
Requires: emacs(bin) >= %{emacs_version}
Requires: emacs-common-%{pkg} = %{version}-%{release}
# MMM Mode is separately packaged for emacs (but not for XEmacs)
Requires: emacs-mmm
%description -n emacs-%{pkg}
Proof General is a generic front-end for proof assistants based on Emacs.
This package contains the byte compiled elisp packages to run Proof
General with GNU Emacs.
%package -n emacs-%{pkg}-el
Summary: Elisp source files for Proof General under GNU Emacs
Group: Applications/Editors
Requires: emacs-%{pkg} = %{version}-%{release}
%description -n emacs-%{pkg}-el
This package contains the elisp source files for Proof General under
GNU Emacs. You do not need to install this package to run Proof
General. Install the emacs-%{pkg} package to use Proof General with
GNU Emacs.
%package -n xemacs-%{pkg}
Summary: Compiled elisp files to run Proof General under XEmacs
Group: Applications/Editors
Requires: xemacs(bin) >= %{xemacs_version}
Requires: emacs-common-%{pkg} = %{version}-%{release}
# For MMM mode (and X-Symbol, whose use in this package currently
# doesn't work - disabled until X-Symbol can be separately packaged)
Requires: xemacs-packages-extra
%description -n xemacs-%{pkg}
Proof General is a generic front-end for proof assistants based on Emacs.
This package contains the byte compiled elisp packages to run Proof
General with XEmacs.
%package -n xemacs-%{pkg}-el
Summary: Elisp source files for Proof General under XEmacs
Group: Applications/Editors
Requires: emacs-%{pkg} = %{version}-%{release}
%description -n xemacs-%{pkg}-el
This package contains the elisp source files for Proof General under
XEmacs. You do not need to install this package to run Proof
General. Install the xemacs-%{pkg} package to use Proof General with
XEmacs.
%prep
%setup -q -n ProofGeneral-%{version}
%patch0
%patch1
%patch2 -p1
%build
# Fix rpmlint complaints:
# Correct permissions for isartags script
chmod 755 isar/isartags
# Correct permissions for x-symbol ChangeLog
chmod 644 x-symbol/lisp/ChangeLog
# Correct permissions for x-symbol Makefile
chmod 644 x-symbol/etc/fonts/Makefile
# Remove .cvsignore file
rm images/gimp/.cvsignore
# Fix non UTF-8 documentation and theory files
# File listing taken from the Makefile
%define doc_files AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
for f in `find %{doc_files}`; do mv $f $f.old && iconv -f iso-8859-1 -t utf8 < $f.old > $f && rm $f.old; done
# Make full copies of emacs and xemacs versions, set options in the proofgeneral start script
make clean
make EMACS=emacs compile bashscripts perlscripts doc
sed -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{emacs_lispdir}|' -e 's|^XEMACS_LISPDIR=.*$|XEMACS_LISPDIR=%{xemacs_lispdir}|' -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' < bin/proofgeneral > .tmp && cat .tmp > bin/proofgeneral
mkdir emacs
for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs`; do cp -pr $f emacs/$f; done
make clean
make EMACS=xemacs compile bashscripts perlscripts doc
sed -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{emacs_lispdir}|' -e 's|^XEMACS_LISPDIR=.*$|XEMACS_LISPDIR=%{xemacs_lispdir}|' -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' < bin/proofgeneral > .tmp && cat .tmp > bin/proofgeneral
mkdir xemacs
for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs ! -name xemacs`; do cp -pr $f xemacs/$f; done
%install
rm -rf %{buildroot}
%define full_doc_dir %{_datadir}/doc/%{pkg}
%define full_man_dir %{_mandir}/man1
%define full_data_dir %{_datadir}/%{pkg}
%define doc_options DOCDIR=%{buildroot}%{full_doc_dir} MANDIR=%{buildroot}%{full_man_dir} INFODIR=%{buildroot}%{_infodir}
%define common_options PREFIX=%{buildroot}%{_prefix} DEST_PREFIX=%{_prefix} DESKTOP=%{buildroot}%{full_data_dir} BINDIR=%{buildroot}%{_bindir} %{doc_options}
%define emacs_options ELISP_START=%{buildroot}%{emacs_startdir} ELISP=%{buildroot}%{emacs_lispdir}/%{pkg} DEST_ELISP=%{emacs_lispdir}/%{pkg}
%define xemacs_options ELISP_START=%{buildroot}%{xemacs_startdir} ELISP=%{buildroot}%{xemacs_lispdir}/%{pkg} DEST_ELISP=%{xemacs_lispdir}/%{pkg}
cp -pr `find xemacs/ -maxdepth 1 -mindepth 1` .
make EMACS=xemacs %{common_options} %{xemacs_options} install install-doc
cp -pr `find emacs/ -maxdepth 1 -mindepth 1` .
make EMACS=emacs %{common_options} %{emacs_options} install install-doc
# Don't accidentally install an infodir file over an existing one
rm -f %{buildroot}%{_infodir}/dir
%clean
rm -rf %{buildroot}
%post
/sbin/install-info %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
/sbin/install-info %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
%preun
if [ $1 -eq 0 ]; then
/sbin/install-info --delete %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
/sbin/install-info --delete %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
fi
%files
%defattr(-,root,root,-)
%{full_doc_dir}
%{full_data_dir}
%{full_man_dir}/*
%{_infodir}/*
%{_bindir}/*
%files -n emacs-%{pkg}
%defattr(-,root,root,-)
%{emacs_lispdir}/%{pkg}/*
# Exclude bundled X-symbol, which should be separately packaged but
# is not critical for the core functionality of the package
%exclude %{emacs_lispdir}/%{pkg}/x-symbol
# Exclude bundled mmm-mode, packaged separately
%exclude %{emacs_lispdir}/%{pkg}/mmm
%exclude %{emacs_lispdir}/%{pkg}/*/*.el
%{emacs_startdir}/*.el
%dir %{emacs_lispdir}/%{pkg}
%files -n emacs-%{pkg}-el
%defattr(-,root,root,-)
%{emacs_lispdir}/%{pkg}/*/*.el
%files -n xemacs-%{pkg}
%defattr(-,root,root,-)
%{xemacs_lispdir}/%{pkg}/*
# Exclude bundled X-symbol, which should be separately packaged but
# is not critical for the core functionality of the package
%exclude %{xemacs_lispdir}/%{pkg}/x-symbol
# Exclude bundled mmm-mode, packaged separately
%exclude %{xemacs_lispdir}/%{pkg}/mmm
%exclude %{xemacs_lispdir}/%{pkg}/*/*.el
%{xemacs_startdir}/*.el
%dir %{xemacs_lispdir}/%{pkg}
%files -n xemacs-%{pkg}-el
%defattr(-,root,root,-)
%{xemacs_lispdir}/%{pkg}/*/*.el
%changelog
* Wed Jul 29 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-4
- Incorporated comments from Jerry James about applying his patch:
patch now applied unconditionally (regardless of Fedora version
which was used as a somewhat imperfect way to control XEmacs
version).
- Patch descriptions moved upward in spec file in accordance with
examples in guidelines.
* Thu Jul 09 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-3
- Added xemacs patch that fixes compilation problems for X-Symbol code.
* Thu Jul 02 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-2
- Excluded bundled X-symbol, mmm-mode.
- Changed requires for these bundled packages.
* Tue Apr 07 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-1
- Initial Fedora RPM.
--- NEW FILE import.log ---
emacs-common-proofgeneral-3_7_1-4_fc10:F-11:emacs-common-proofgeneral-3.7.1-4.fc10.src.rpm:1249079698
pg-3.7.1-Makefile.patch:
Makefile | 2 --
1 file changed, 2 deletions(-)
--- NEW FILE pg-3.7.1-Makefile.patch ---
--- Makefile 2009-01-27 21:22:49.000000000 -0500
+++ Makefile 2009-01-27 21:23:26.000000000 -0500
@@ -215,8 +215,6 @@
cp -pf doc/proofgeneral.1 ${MANDIR}
mkdir -p ${INFODIR}
cp -pf doc/*.info ${INFODIR}
- /sbin/install-info ${INFODIR}/ProofGeneral.info* ${INFODIR}/dir
- /sbin/install-info ${INFODIR}/PG-adapting.info* ${INFODIR}/dir
mkdir -p ${DOCDIR}
for f in ${DOC_FILES}; do cp -pf $$f ${DOCDIR}; done
for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; cp -pf $$f ${DOCDIR}/$$f; done
pg-3.7.1-startscript.patch:
proofgeneral | 50 +++++++++++++++++++++++++++++---------------------
1 file changed, 29 insertions(+), 21 deletions(-)
--- NEW FILE pg-3.7.1-startscript.patch ---
--- bin/proofgeneral 2009-02-04 06:03:47.000000000 -0500
+++ bin/proofgeneral 2009-02-04 07:24:42.000000000 -0500
@@ -15,31 +15,18 @@
#
# proofgeneral,v 9.6 2008/07/19 16:10:12 da Exp
#
+# Additional edits for Fedora made by Alan Dunn (parts of script
+# also rearranged)
+
+# Fedora extra variables
+EMACS_LISPDIR=
+XEMACS_LISPDIR=
+PACKAGE=
# The default path should work if you are using the Proof General RPM
# or unpack Proof General in your home directory. Otherwise edit below.
# NB: no trailing backslash here!
-PGHOMEDEFAULT=$HOME/ProofGeneral
-
-# Try to find a default Emacs executable
-if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
- if which emacs > /dev/null; then
- EMACS=`which emacs`
- else
- EMACS=`which xemacs`
- fi
-fi
-
-# Try to find Proof General directory
-if [ -d $PGHOMEDEFAULT ]; then
- PGHOME=$PGHOMEDEFAULT
-elif [ -d /usr/share/${EMACSVERSION}/site-lisp/proofgeneral ]; then
- PGHOME=/usr/share/${EMACSVERSION}/site-lisp/proofgeneral
-else
- echo "Cannot find the Proof General lisp files: please edit script to set PGHOMEDEFAULT correctly."
- exit 1
-fi
-
+PGHOMEDEFAULT=/usr/share/emacs/site-lisp/${PACKAGE}
NAME=`basename $0`
@@ -98,6 +85,15 @@
esac
do shift; done
+# Try to find a default Emacs executable
+if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
+ if which emacs > /dev/null; then
+ EMACS=`which emacs`
+ else
+ EMACS=`which xemacs`
+ fi
+fi
+
if [ ! -x "$EMACS" ]; then
echo "$NAME: cannot find an Emacs or XEmacs executable. Set EMACS or your PATH." 1>&2
exit 1
@@ -105,6 +101,18 @@
EMACSVERSION=`basename $EMACS`
+# Try to find Proof General directory
+if [ -d $PGHOMEDEFAULT ]; then
+ PGHOME=$PGHOMEDEFAULT
+elif [[ $EMACSVERSION == emacs && -d ${EMACS_LISPDIR}/${PACKAGE} ]]; then
+ PGHOME=${EMACS_LISPDIR}/${PACKAGE}
+elif [[ $EMACSVERSION == xemacs && -d ${XEMACS_LISPDIR}/${PACKAGE} ]]; then
+ PGHOME=${XEMACS_LISPDIR}/${PACKAGE}
+else
+ echo "Cannot find the Proof General lisp files: please edit script to set PGHOMEDEFAULT correctly."
+ exit 1
+fi
+
# Deal with UTF issue
if [ `locale | grep LC_CTYPE | grep UTF` ]; then
echo "Warning: detected Unicode LC_CTYPE setting, switched back to C"
pg-3.7.1-xemacs-display-table.patch:
Makefile | 2 -
generic/pg-display-table.el | 46 +++++++++++++++++++++++++++++++++++++++
generic/proof-shell.el | 3 +-
phox/phox-sym-lock.el | 10 +++++---
x-symbol/lisp/x-symbol-nomule.el | 6 ++---
x-symbol/lisp/x-symbol.el | 3 +-
6 files changed, 59 insertions(+), 11 deletions(-)
--- NEW FILE pg-3.7.1-xemacs-display-table.patch ---
diff -durN ProofGeneral-3.7.1.ORIG/generic/pg-display-table.el ProofGeneral-3.7.1/generic/pg-display-table.el
--- ProofGeneral-3.7.1.ORIG/generic/pg-display-table.el 1969-12-31 19:00:00.000000000 -0500
+++ ProofGeneral-3.7.1/generic/pg-display-table.el 2009-07-09 12:49:34.923843082 -0400
@@ -0,0 +1,46 @@
+;; pg-display-table.el --- Wrapper functions for display-table vectors and
+;; objects.
+;;
+;; Copyright (C) 2009 LFCS Edinburgh.
+;; Author: Jerry James
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; pg-display-table.el,v 1.0 2009/07/06 16:07:09 da Exp
+;;
+;;
+;;; Commentary:
+;;
+;; This file hides the differences between display-tables that are represented
+;; as vectors and recent XEmacs display-tables, which are objects.
+
+;;; Code:
+
+(require 'disp-table)
+
+(defmacro defun-when-void (&rest args)
+ "Define a function, just like `defun', unless it's already defined.
+Used for compatibility among different emacs variants."
+ `(if (fboundp ',(car args))
+ nil
+ (defun ,@args)))
+
+(defun-when-void put-display-table (range value display-table)
+ "Set the value for char RANGE to VALUE in DISPLAY-TABLE."
+ (if (sequencep display-table)
+ (aset display-table range value)
+ (put-char-table range value display-table)))
+
+(defun-when-void get-display-table (character display-table)
+ "Find value for CHARACTER in DISPLAY-TABLE."
+ (if (sequencep display-table)
+ (aref display-table character)
+ (get-char-table character display-table)))
+
+(defun-when-void fill-display-table (value display-table)
+ "Map every entry in the table to VALUE."
+ (if (sequencep display-table)
+ (fillarray display-table value)
+ (put-char-table t value display-table)))
+
+(provide 'pg-display-table)
+;;; pg-display-table.el ends here
diff -durN ProofGeneral-3.7.1.ORIG/generic/proof-shell.el ProofGeneral-3.7.1/generic/proof-shell.el
--- ProofGeneral-3.7.1.ORIG/generic/proof-shell.el 2008-07-10 08:49:32.000000000 -0400
+++ ProofGeneral-3.7.1/generic/proof-shell.el 2009-07-09 12:49:34.948238190 -0400
@@ -16,6 +16,7 @@
(require 'proof-utils))
(require 'proof-autoloads)
+(require 'pg-display-table)
(require 'pg-response)
(require 'pg-goals)
(require 'proof-script)
@@ -1695,7 +1696,7 @@
(let ((disp (make-display-table))
(i 128))
(while (< i 256)
- (aset disp i [])
+ (put-display-table i [] disp)
(incf i))
(cond ((featurep 'xemacs)
(add-spec-to-specifier current-display-table disp (current-buffer)))
diff -durN ProofGeneral-3.7.1.ORIG/Makefile ProofGeneral-3.7.1/Makefile
--- ProofGeneral-3.7.1.ORIG/Makefile 2008-01-31 08:06:38.000000000 -0500
+++ ProofGeneral-3.7.1/Makefile 2009-07-09 13:16:35.366276826 -0400
@@ -86,8 +86,6 @@
@echo " Byte compiling... "
@echo "****************************************************************"
make elc
- @echo " Byte compiling X-Symbol..."
- (cd x-symbol/lisp; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
echo $(EMACS) > $(@)
@echo "****************************************************************"
@echo " Finished."
diff -durN ProofGeneral-3.7.1.ORIG/phox/phox-sym-lock.el ProofGeneral-3.7.1/phox/phox-sym-lock.el
--- ProofGeneral-3.7.1.ORIG/phox/phox-sym-lock.el 2008-01-30 10:22:21.000000000 -0500
+++ ProofGeneral-3.7.1/phox/phox-sym-lock.el 2009-07-09 12:49:35.065515654 -0400
@@ -28,6 +28,7 @@
;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*'
(require 'font-lock)
+(require 'pg-display-table)
(if (featurep 'xemacs)
(require 'atomic-extents)) ;; not available on GNU Emacs
@@ -223,9 +224,10 @@
(let* ((name (phox-sym-lock-gen-symbol "face"))
(table (make-display-table))
(tface (make-face name "phox-sym-lock-remap-face" t)))
- (fillarray table "")
- (aset table (string-to-char (substring pat (1- pos) pos))
- (phox-sym-lock-translate-char-or-string obj))
+ (fill-display-table "" table)
+ (put-display-table (string-to-char (substring pat (1- pos) pos))
+ (phox-sym-lock-translate-char-or-string obj)
+ table)
(set-face-foreground tface (if (and (boundp 'font-lock-use-fonts)
font-lock-use-fonts)
(face-foreground 'default) phox-sym-lock-color))
@@ -240,7 +242,7 @@
(let* ((name (phox-sym-lock-gen-symbol "face"))
(table (make-display-table))
(tface (make-face name "phox-sym-lock-remap-face" t)))
- (fillarray table "")
+ (fill-display-table "" table)
(set-face-property tface 'display-table table)
(set-face-property tface 'phox-sym-lock-remap 1) ; mark it
tface
diff -durN ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol.el ProofGeneral-3.7.1/x-symbol/lisp/x-symbol.el
--- ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol.el 2008-07-18 12:10:30.000000000 -0400
+++ ProofGeneral-3.7.1/x-symbol/lisp/x-symbol.el 2009-07-09 12:49:35.115921558 -0400
@@ -39,6 +39,7 @@
(provide 'x-symbol)
;;(require 'x-symbol-hooks)
(require 'x-symbol-vars)
+(require 'pg-display-table)
(require (if (featurep 'mule) 'x-symbol-mule 'x-symbol-nomule))
(eval-when-compile (require 'x-symbol-macs))
(eval-when-compile (require 'cl))
@@ -1612,7 +1613,7 @@
(let ((table (make-display-table))
(i 0))
(while (< i 256)
- (aset table i "")
+ (put-display-table i "" table)
(setq i (1+ i)))
table)
"Internal variable. Display table for `x-symbol-invisible-face'.")
diff -durN ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol-nomule.el ProofGeneral-3.7.1/x-symbol/lisp/x-symbol-nomule.el
--- ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol-nomule.el 2008-01-30 10:22:26.000000000 -0500
+++ ProofGeneral-3.7.1/x-symbol/lisp/x-symbol-nomule.el 2009-07-09 12:49:35.156890261 -0400
@@ -33,6 +33,7 @@
(error "This file is meant to be used with XEmacs/no-Mule"))
(provide 'x-symbol-nomule)
(require 'x-symbol-hooks)
+(require 'pg-display-table)
(eval-when-compile (require 'x-symbol)) ; x-symbol also requires this file
;;(eval-when-compile
;; (defvar x-symbol-encode-rchars)
@@ -80,11 +81,10 @@
"Internal. Face to fontify current font-lock match.")
(defvar x-symbol-nomule-display-table
- ;; display-table via characters table is not implemented in XEmacs yet...
- (let ((table (make-vector 256 nil))
+ (let ((table (make-display-table))
(i 128))
(while (< i 160)
- (aset table i "")
+ (put-display-table i "" table)
(incf i))
table)
"Display table in faces with non-standard charset registry.
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/emacs-common-proofgeneral/F-11/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- .cvsignore 31 Jul 2009 21:14:21 -0000 1.1
+++ .cvsignore 31 Jul 2009 22:41:37 -0000 1.2
@@ -0,0 +1 @@
+ProofGeneral-3.7.1.tgz
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/emacs-common-proofgeneral/F-11/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- sources 31 Jul 2009 21:14:21 -0000 1.1
+++ sources 31 Jul 2009 22:41:37 -0000 1.2
@@ -0,0 +1 @@
+eebfff672b5941823fe893075316b02e ProofGeneral-3.7.1.tgz
Author: amdunn
Update of /cvs/pkgs/rpms/emacs-common-proofgeneral/devel
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv3064/devel
Modified Files:
.cvsignore sources
Added Files:
emacs-common-proofgeneral.spec import.log
pg-3.7.1-Makefile.patch pg-3.7.1-startscript.patch
pg-3.7.1-xemacs-display-table.patch
Log Message:
* Wed Jul 29 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-4
- Incorporated comments from Jerry James about applying his patch:
patch now applied unconditionally (regardless of Fedora version
which was used as a somewhat imperfect way to control XEmacs
version).
- Patch descriptions moved upward in spec file in accordance with
examples in guidelines.
* Thu Jul 09 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-3
- Added xemacs patch that fixes compilation problems for X-Symbol code.
* Thu Jul 02 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-2
- Excluded bundled X-symbol, mmm-mode.
- Changed requires for these bundled packages.
* Tue Apr 07 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-1
- Initial Fedora RPM.
--- NEW FILE emacs-common-proofgeneral.spec ---
# Patches described below with the patch commands
%define pkg proofgeneral
# Check version defaults
# If the emacs-el package has installed a pkgconfig file, use that to
# determine install locations and Emacs version at build time, otherwise
# set defaults.
%if %($(pkg-config emacs) ; echo $?)
%define emacs_version 22.1
%define emacs_lispdir %{_datadir}/emacs/site-lisp
%define emacs_startdir %{_datadir}/emacs/site-lisp/site-start.d
%else
%define emacs_version %(pkg-config emacs --modversion)
%define emacs_lispdir %(pkg-config emacs --variable sitepkglispdir)
%define emacs_startdir %(pkg-config emacs --variable sitestartdir)
%endif
# If the xemacs-devel package has installed a pkgconfig file, use that
# to determine install locations and Emacs version at build time,
# otherwise set defaults.
%if %($(pkg-config xemacs) ; echo $?)
%define xemacs_version 21.5
%define xemacs_lispdir %{_datadir}/xemacs/site-packages/lisp
%define xemacs_startdir %{_datadir}/xemacs/site-packages/lisp/site-start.d
%else
%define xemacs_version %(pkg-config xemacs --modversion)
%define xemacs_lispdir %(pkg-config xemacs --variable sitepkglispdir)
%define xemacs_startdir %(pkg-config xemacs --variable sitestartdir)
%endif
Name: emacs-common-%{pkg}
Version: 3.7.1
Release: 4%{?dist}
Summary: Emacs mode for standard interaction interface for proof assistants
Group: Applications/Editors
License: GPLv2
URL: http://proofgeneral.inf.ed.ac.uk/
Source0: http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-%{version}.tgz
# Patch 0 - Fedora specific, don't do an "install-info" in the make process
# (which would occur at build time), but instead put it into a scriptlet
Patch0: pg-3.7.1-Makefile.patch
# Patch 1 - Somewhat Fedora specific, patches Proof General starting
# script to include values of build time generated variables (which
# are inserted in the build process with sed) instead of its way of
# getting this information. Also moves around some script parts related
# to emacs version detection.
Patch1: pg-3.7.1-startscript.patch
# Patch 2 - Display tables were changed in XEmacs 21.5.29 in a way
# that breaks ProofGeneral's X-Symbol code unless changes are made
# Incorporating a patch here from Jerry James. (Of course, right now
# the X-Symbol code is disabled as X-Symbol isn't packaged and
# ProofGeneral makes changes to the X-Symbol code that would have to
# be included somehow anyway, but ProofGeneral's X-Symbol code could
# be activated in the future and the change is necessary to allow the
# code to be byte-compiled).
Patch2: pg-3.7.1-xemacs-display-table.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildArch: noarch
BuildRequires: emacs emacs-el xemacs xemacs-devel texinfo-tex xemacs-packages-extra
%description
Proof General is a generic front-end for proof assistants (also known
as interactive theorem provers) based on Emacs.
Proof General allows one to edit and submit a proof script to a proof
assistant in an interactive manner:
- It tracks the goal state, and the script as it is submitted, and
allows for easy backtracking and block execution.
- It adds toolbars and menus to Emacs for easy access to proof
assistant features.
- It integrates with X-Symbol for some provers to provide output using
proper mathematical symbols.
- It includes utilities for generating Emacs tags for proof scripts,
allowing for easy navigation.
Proof General supports a number of different proof assistants
(Isabelle, Coq, PhoX, and LEGO to name a few) and is designed to be
easily extendable to work with others.
%package -n emacs-%{pkg}
Summary: Compiled elisp files to run Proof General under GNU Emacs
Group: Applications/Editors
Requires: emacs(bin) >= %{emacs_version}
Requires: emacs-common-%{pkg} = %{version}-%{release}
# MMM Mode is separately packaged for emacs (but not for XEmacs)
Requires: emacs-mmm
%description -n emacs-%{pkg}
Proof General is a generic front-end for proof assistants based on Emacs.
This package contains the byte compiled elisp packages to run Proof
General with GNU Emacs.
%package -n emacs-%{pkg}-el
Summary: Elisp source files for Proof General under GNU Emacs
Group: Applications/Editors
Requires: emacs-%{pkg} = %{version}-%{release}
%description -n emacs-%{pkg}-el
This package contains the elisp source files for Proof General under
GNU Emacs. You do not need to install this package to run Proof
General. Install the emacs-%{pkg} package to use Proof General with
GNU Emacs.
%package -n xemacs-%{pkg}
Summary: Compiled elisp files to run Proof General under XEmacs
Group: Applications/Editors
Requires: xemacs(bin) >= %{xemacs_version}
Requires: emacs-common-%{pkg} = %{version}-%{release}
# For MMM mode (and X-Symbol, whose use in this package currently
# doesn't work - disabled until X-Symbol can be separately packaged)
Requires: xemacs-packages-extra
%description -n xemacs-%{pkg}
Proof General is a generic front-end for proof assistants based on Emacs.
This package contains the byte compiled elisp packages to run Proof
General with XEmacs.
%package -n xemacs-%{pkg}-el
Summary: Elisp source files for Proof General under XEmacs
Group: Applications/Editors
Requires: emacs-%{pkg} = %{version}-%{release}
%description -n xemacs-%{pkg}-el
This package contains the elisp source files for Proof General under
XEmacs. You do not need to install this package to run Proof
General. Install the xemacs-%{pkg} package to use Proof General with
XEmacs.
%prep
%setup -q -n ProofGeneral-%{version}
%patch0
%patch1
%patch2 -p1
%build
# Fix rpmlint complaints:
# Correct permissions for isartags script
chmod 755 isar/isartags
# Correct permissions for x-symbol ChangeLog
chmod 644 x-symbol/lisp/ChangeLog
# Correct permissions for x-symbol Makefile
chmod 644 x-symbol/etc/fonts/Makefile
# Remove .cvsignore file
rm images/gimp/.cvsignore
# Fix non UTF-8 documentation and theory files
# File listing taken from the Makefile
%define doc_files AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
for f in `find %{doc_files}`; do mv $f $f.old && iconv -f iso-8859-1 -t utf8 < $f.old > $f && rm $f.old; done
# Make full copies of emacs and xemacs versions, set options in the proofgeneral start script
make clean
make EMACS=emacs compile bashscripts perlscripts doc
sed -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{emacs_lispdir}|' -e 's|^XEMACS_LISPDIR=.*$|XEMACS_LISPDIR=%{xemacs_lispdir}|' -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' < bin/proofgeneral > .tmp && cat .tmp > bin/proofgeneral
mkdir emacs
for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs`; do cp -pr $f emacs/$f; done
make clean
make EMACS=xemacs compile bashscripts perlscripts doc
sed -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{emacs_lispdir}|' -e 's|^XEMACS_LISPDIR=.*$|XEMACS_LISPDIR=%{xemacs_lispdir}|' -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' < bin/proofgeneral > .tmp && cat .tmp > bin/proofgeneral
mkdir xemacs
for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs ! -name xemacs`; do cp -pr $f xemacs/$f; done
%install
rm -rf %{buildroot}
%define full_doc_dir %{_datadir}/doc/%{pkg}
%define full_man_dir %{_mandir}/man1
%define full_data_dir %{_datadir}/%{pkg}
%define doc_options DOCDIR=%{buildroot}%{full_doc_dir} MANDIR=%{buildroot}%{full_man_dir} INFODIR=%{buildroot}%{_infodir}
%define common_options PREFIX=%{buildroot}%{_prefix} DEST_PREFIX=%{_prefix} DESKTOP=%{buildroot}%{full_data_dir} BINDIR=%{buildroot}%{_bindir} %{doc_options}
%define emacs_options ELISP_START=%{buildroot}%{emacs_startdir} ELISP=%{buildroot}%{emacs_lispdir}/%{pkg} DEST_ELISP=%{emacs_lispdir}/%{pkg}
%define xemacs_options ELISP_START=%{buildroot}%{xemacs_startdir} ELISP=%{buildroot}%{xemacs_lispdir}/%{pkg} DEST_ELISP=%{xemacs_lispdir}/%{pkg}
cp -pr `find xemacs/ -maxdepth 1 -mindepth 1` .
make EMACS=xemacs %{common_options} %{xemacs_options} install install-doc
cp -pr `find emacs/ -maxdepth 1 -mindepth 1` .
make EMACS=emacs %{common_options} %{emacs_options} install install-doc
# Don't accidentally install an infodir file over an existing one
rm -f %{buildroot}%{_infodir}/dir
%clean
rm -rf %{buildroot}
%post
/sbin/install-info %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
/sbin/install-info %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
%preun
if [ $1 -eq 0 ]; then
/sbin/install-info --delete %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
/sbin/install-info --delete %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
fi
%files
%defattr(-,root,root,-)
%{full_doc_dir}
%{full_data_dir}
%{full_man_dir}/*
%{_infodir}/*
%{_bindir}/*
%files -n emacs-%{pkg}
%defattr(-,root,root,-)
%{emacs_lispdir}/%{pkg}/*
# Exclude bundled X-symbol, which should be separately packaged but
# is not critical for the core functionality of the package
%exclude %{emacs_lispdir}/%{pkg}/x-symbol
# Exclude bundled mmm-mode, packaged separately
%exclude %{emacs_lispdir}/%{pkg}/mmm
%exclude %{emacs_lispdir}/%{pkg}/*/*.el
%{emacs_startdir}/*.el
%dir %{emacs_lispdir}/%{pkg}
%files -n emacs-%{pkg}-el
%defattr(-,root,root,-)
%{emacs_lispdir}/%{pkg}/*/*.el
%files -n xemacs-%{pkg}
%defattr(-,root,root,-)
%{xemacs_lispdir}/%{pkg}/*
# Exclude bundled X-symbol, which should be separately packaged but
# is not critical for the core functionality of the package
%exclude %{xemacs_lispdir}/%{pkg}/x-symbol
# Exclude bundled mmm-mode, packaged separately
%exclude %{xemacs_lispdir}/%{pkg}/mmm
%exclude %{xemacs_lispdir}/%{pkg}/*/*.el
%{xemacs_startdir}/*.el
%dir %{xemacs_lispdir}/%{pkg}
%files -n xemacs-%{pkg}-el
%defattr(-,root,root,-)
%{xemacs_lispdir}/%{pkg}/*/*.el
%changelog
* Wed Jul 29 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-4
- Incorporated comments from Jerry James about applying his patch:
patch now applied unconditionally (regardless of Fedora version
which was used as a somewhat imperfect way to control XEmacs
version).
- Patch descriptions moved upward in spec file in accordance with
examples in guidelines.
* Thu Jul 09 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-3
- Added xemacs patch that fixes compilation problems for X-Symbol code.
* Thu Jul 02 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-2
- Excluded bundled X-symbol, mmm-mode.
- Changed requires for these bundled packages.
* Tue Apr 07 2009 Alan Dunn <amdunn(a)gmail.com> 3.7.1-1
- Initial Fedora RPM.
--- NEW FILE import.log ---
emacs-common-proofgeneral-3_7_1-4_fc10:HEAD:emacs-common-proofgeneral-3.7.1-4.fc10.src.rpm:1249077541
pg-3.7.1-Makefile.patch:
Makefile | 2 --
1 file changed, 2 deletions(-)
--- NEW FILE pg-3.7.1-Makefile.patch ---
--- Makefile 2009-01-27 21:22:49.000000000 -0500
+++ Makefile 2009-01-27 21:23:26.000000000 -0500
@@ -215,8 +215,6 @@
cp -pf doc/proofgeneral.1 ${MANDIR}
mkdir -p ${INFODIR}
cp -pf doc/*.info ${INFODIR}
- /sbin/install-info ${INFODIR}/ProofGeneral.info* ${INFODIR}/dir
- /sbin/install-info ${INFODIR}/PG-adapting.info* ${INFODIR}/dir
mkdir -p ${DOCDIR}
for f in ${DOC_FILES}; do cp -pf $$f ${DOCDIR}; done
for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; cp -pf $$f ${DOCDIR}/$$f; done
pg-3.7.1-startscript.patch:
proofgeneral | 50 +++++++++++++++++++++++++++++---------------------
1 file changed, 29 insertions(+), 21 deletions(-)
--- NEW FILE pg-3.7.1-startscript.patch ---
--- bin/proofgeneral 2009-02-04 06:03:47.000000000 -0500
+++ bin/proofgeneral 2009-02-04 07:24:42.000000000 -0500
@@ -15,31 +15,18 @@
#
# proofgeneral,v 9.6 2008/07/19 16:10:12 da Exp
#
+# Additional edits for Fedora made by Alan Dunn (parts of script
+# also rearranged)
+
+# Fedora extra variables
+EMACS_LISPDIR=
+XEMACS_LISPDIR=
+PACKAGE=
# The default path should work if you are using the Proof General RPM
# or unpack Proof General in your home directory. Otherwise edit below.
# NB: no trailing backslash here!
-PGHOMEDEFAULT=$HOME/ProofGeneral
-
-# Try to find a default Emacs executable
-if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
- if which emacs > /dev/null; then
- EMACS=`which emacs`
- else
- EMACS=`which xemacs`
- fi
-fi
-
-# Try to find Proof General directory
-if [ -d $PGHOMEDEFAULT ]; then
- PGHOME=$PGHOMEDEFAULT
-elif [ -d /usr/share/${EMACSVERSION}/site-lisp/proofgeneral ]; then
- PGHOME=/usr/share/${EMACSVERSION}/site-lisp/proofgeneral
-else
- echo "Cannot find the Proof General lisp files: please edit script to set PGHOMEDEFAULT correctly."
- exit 1
-fi
-
+PGHOMEDEFAULT=/usr/share/emacs/site-lisp/${PACKAGE}
NAME=`basename $0`
@@ -98,6 +85,15 @@
esac
do shift; done
+# Try to find a default Emacs executable
+if [ -z "$EMACS" ] || [ ! -x "$EMACS" ]; then
+ if which emacs > /dev/null; then
+ EMACS=`which emacs`
+ else
+ EMACS=`which xemacs`
+ fi
+fi
+
if [ ! -x "$EMACS" ]; then
echo "$NAME: cannot find an Emacs or XEmacs executable. Set EMACS or your PATH." 1>&2
exit 1
@@ -105,6 +101,18 @@
EMACSVERSION=`basename $EMACS`
+# Try to find Proof General directory
+if [ -d $PGHOMEDEFAULT ]; then
+ PGHOME=$PGHOMEDEFAULT
+elif [[ $EMACSVERSION == emacs && -d ${EMACS_LISPDIR}/${PACKAGE} ]]; then
+ PGHOME=${EMACS_LISPDIR}/${PACKAGE}
+elif [[ $EMACSVERSION == xemacs && -d ${XEMACS_LISPDIR}/${PACKAGE} ]]; then
+ PGHOME=${XEMACS_LISPDIR}/${PACKAGE}
+else
+ echo "Cannot find the Proof General lisp files: please edit script to set PGHOMEDEFAULT correctly."
+ exit 1
+fi
+
# Deal with UTF issue
if [ `locale | grep LC_CTYPE | grep UTF` ]; then
echo "Warning: detected Unicode LC_CTYPE setting, switched back to C"
pg-3.7.1-xemacs-display-table.patch:
Makefile | 2 -
generic/pg-display-table.el | 46 +++++++++++++++++++++++++++++++++++++++
generic/proof-shell.el | 3 +-
phox/phox-sym-lock.el | 10 +++++---
x-symbol/lisp/x-symbol-nomule.el | 6 ++---
x-symbol/lisp/x-symbol.el | 3 +-
6 files changed, 59 insertions(+), 11 deletions(-)
--- NEW FILE pg-3.7.1-xemacs-display-table.patch ---
diff -durN ProofGeneral-3.7.1.ORIG/generic/pg-display-table.el ProofGeneral-3.7.1/generic/pg-display-table.el
--- ProofGeneral-3.7.1.ORIG/generic/pg-display-table.el 1969-12-31 19:00:00.000000000 -0500
+++ ProofGeneral-3.7.1/generic/pg-display-table.el 2009-07-09 12:49:34.923843082 -0400
@@ -0,0 +1,46 @@
+;; pg-display-table.el --- Wrapper functions for display-table vectors and
+;; objects.
+;;
+;; Copyright (C) 2009 LFCS Edinburgh.
+;; Author: Jerry James
+;; License: GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; pg-display-table.el,v 1.0 2009/07/06 16:07:09 da Exp
+;;
+;;
+;;; Commentary:
+;;
+;; This file hides the differences between display-tables that are represented
+;; as vectors and recent XEmacs display-tables, which are objects.
+
+;;; Code:
+
+(require 'disp-table)
+
+(defmacro defun-when-void (&rest args)
+ "Define a function, just like `defun', unless it's already defined.
+Used for compatibility among different emacs variants."
+ `(if (fboundp ',(car args))
+ nil
+ (defun ,@args)))
+
+(defun-when-void put-display-table (range value display-table)
+ "Set the value for char RANGE to VALUE in DISPLAY-TABLE."
+ (if (sequencep display-table)
+ (aset display-table range value)
+ (put-char-table range value display-table)))
+
+(defun-when-void get-display-table (character display-table)
+ "Find value for CHARACTER in DISPLAY-TABLE."
+ (if (sequencep display-table)
+ (aref display-table character)
+ (get-char-table character display-table)))
+
+(defun-when-void fill-display-table (value display-table)
+ "Map every entry in the table to VALUE."
+ (if (sequencep display-table)
+ (fillarray display-table value)
+ (put-char-table t value display-table)))
+
+(provide 'pg-display-table)
+;;; pg-display-table.el ends here
diff -durN ProofGeneral-3.7.1.ORIG/generic/proof-shell.el ProofGeneral-3.7.1/generic/proof-shell.el
--- ProofGeneral-3.7.1.ORIG/generic/proof-shell.el 2008-07-10 08:49:32.000000000 -0400
+++ ProofGeneral-3.7.1/generic/proof-shell.el 2009-07-09 12:49:34.948238190 -0400
@@ -16,6 +16,7 @@
(require 'proof-utils))
(require 'proof-autoloads)
+(require 'pg-display-table)
(require 'pg-response)
(require 'pg-goals)
(require 'proof-script)
@@ -1695,7 +1696,7 @@
(let ((disp (make-display-table))
(i 128))
(while (< i 256)
- (aset disp i [])
+ (put-display-table i [] disp)
(incf i))
(cond ((featurep 'xemacs)
(add-spec-to-specifier current-display-table disp (current-buffer)))
diff -durN ProofGeneral-3.7.1.ORIG/Makefile ProofGeneral-3.7.1/Makefile
--- ProofGeneral-3.7.1.ORIG/Makefile 2008-01-31 08:06:38.000000000 -0500
+++ ProofGeneral-3.7.1/Makefile 2009-07-09 13:16:35.366276826 -0400
@@ -86,8 +86,6 @@
@echo " Byte compiling... "
@echo "****************************************************************"
make elc
- @echo " Byte compiling X-Symbol..."
- (cd x-symbol/lisp; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
echo $(EMACS) > $(@)
@echo "****************************************************************"
@echo " Finished."
diff -durN ProofGeneral-3.7.1.ORIG/phox/phox-sym-lock.el ProofGeneral-3.7.1/phox/phox-sym-lock.el
--- ProofGeneral-3.7.1.ORIG/phox/phox-sym-lock.el 2008-01-30 10:22:21.000000000 -0500
+++ ProofGeneral-3.7.1/phox/phox-sym-lock.el 2009-07-09 12:49:35.065515654 -0400
@@ -28,6 +28,7 @@
;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*'
(require 'font-lock)
+(require 'pg-display-table)
(if (featurep 'xemacs)
(require 'atomic-extents)) ;; not available on GNU Emacs
@@ -223,9 +224,10 @@
(let* ((name (phox-sym-lock-gen-symbol "face"))
(table (make-display-table))
(tface (make-face name "phox-sym-lock-remap-face" t)))
- (fillarray table "")
- (aset table (string-to-char (substring pat (1- pos) pos))
- (phox-sym-lock-translate-char-or-string obj))
+ (fill-display-table "" table)
+ (put-display-table (string-to-char (substring pat (1- pos) pos))
+ (phox-sym-lock-translate-char-or-string obj)
+ table)
(set-face-foreground tface (if (and (boundp 'font-lock-use-fonts)
font-lock-use-fonts)
(face-foreground 'default) phox-sym-lock-color))
@@ -240,7 +242,7 @@
(let* ((name (phox-sym-lock-gen-symbol "face"))
(table (make-display-table))
(tface (make-face name "phox-sym-lock-remap-face" t)))
- (fillarray table "")
+ (fill-display-table "" table)
(set-face-property tface 'display-table table)
(set-face-property tface 'phox-sym-lock-remap 1) ; mark it
tface
diff -durN ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol.el ProofGeneral-3.7.1/x-symbol/lisp/x-symbol.el
--- ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol.el 2008-07-18 12:10:30.000000000 -0400
+++ ProofGeneral-3.7.1/x-symbol/lisp/x-symbol.el 2009-07-09 12:49:35.115921558 -0400
@@ -39,6 +39,7 @@
(provide 'x-symbol)
;;(require 'x-symbol-hooks)
(require 'x-symbol-vars)
+(require 'pg-display-table)
(require (if (featurep 'mule) 'x-symbol-mule 'x-symbol-nomule))
(eval-when-compile (require 'x-symbol-macs))
(eval-when-compile (require 'cl))
@@ -1612,7 +1613,7 @@
(let ((table (make-display-table))
(i 0))
(while (< i 256)
- (aset table i "")
+ (put-display-table i "" table)
(setq i (1+ i)))
table)
"Internal variable. Display table for `x-symbol-invisible-face'.")
diff -durN ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol-nomule.el ProofGeneral-3.7.1/x-symbol/lisp/x-symbol-nomule.el
--- ProofGeneral-3.7.1.ORIG/x-symbol/lisp/x-symbol-nomule.el 2008-01-30 10:22:26.000000000 -0500
+++ ProofGeneral-3.7.1/x-symbol/lisp/x-symbol-nomule.el 2009-07-09 12:49:35.156890261 -0400
@@ -33,6 +33,7 @@
(error "This file is meant to be used with XEmacs/no-Mule"))
(provide 'x-symbol-nomule)
(require 'x-symbol-hooks)
+(require 'pg-display-table)
(eval-when-compile (require 'x-symbol)) ; x-symbol also requires this file
;;(eval-when-compile
;; (defvar x-symbol-encode-rchars)
@@ -80,11 +81,10 @@
"Internal. Face to fontify current font-lock match.")
(defvar x-symbol-nomule-display-table
- ;; display-table via characters table is not implemented in XEmacs yet...
- (let ((table (make-vector 256 nil))
+ (let ((table (make-display-table))
(i 128))
(while (< i 160)
- (aset table i "")
+ (put-display-table i "" table)
(incf i))
table)
"Display table in faces with non-standard charset registry.
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/emacs-common-proofgeneral/devel/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- .cvsignore 31 Jul 2009 21:14:21 -0000 1.1
+++ .cvsignore 31 Jul 2009 22:05:37 -0000 1.2
@@ -0,0 +1 @@
+ProofGeneral-3.7.1.tgz
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/emacs-common-proofgeneral/devel/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- sources 31 Jul 2009 21:14:21 -0000 1.1
+++ sources 31 Jul 2009 22:05:38 -0000 1.2
@@ -0,0 +1 @@
+eebfff672b5941823fe893075316b02e ProofGeneral-3.7.1.tgz