[emacs-common-proofgeneral] New upstream release. Upstream no longer supports XEmacs. Upstream no longer bundles X-Symbol. Remov

Jerry James jjames at fedoraproject.org
Tue Jul 24 18:30:09 UTC 2012


commit fb4b44efe0774c26cfd5b8ceadfa8a6e72dd09b8
Author: Jerry James <loganjerry at gmail.com>
Date:   Tue Jul 24 12:29:33 2012 -0600

    New upstream release.
    Upstream no longer supports XEmacs.
    Upstream no longer bundles X-Symbol.
    Remove unnecessary spec file elements (defattr, etc.).
    Move desktop files into places where they will be used.

 .gitignore                                       |    3 +-
 emacs-common-proofgeneral.spec                   |  239 +++++++++-------------
 pg-3.7.1-startscript.patch                       |   77 -------
 pg-3.7.1-xemacs-display-table.patch              |  161 ---------------
 pg-3.7.1-Makefile.patch => pg-4.1-Makefile.patch |    6 +-
 pg-4.1-desktop.patch                             |   19 ++
 pg-4.1-elisp.patch                               |  101 +++++++++
 sources                                          |    3 +-
 8 files changed, 221 insertions(+), 388 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index dbb45e5..a34164f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
-ProofGeneral-3.7.1.tgz
+/ProofGeneral-4.1.tgz
+/ProofGeneralPortrait.eps.gz
diff --git a/emacs-common-proofgeneral.spec b/emacs-common-proofgeneral.spec
index 510fda4..2f743bc 100644
--- a/emacs-common-proofgeneral.spec
+++ b/emacs-common-proofgeneral.spec
@@ -1,70 +1,34 @@
-# 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
+%global pkg proofgeneral
 
 Name:           emacs-common-%{pkg}
-Version:        3.7.1
-Release:        7%{?dist}
+Version:        4.1
+Release:        1%{?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
+Source1:        http://proofgeneral.inf.ed.ac.uk/ProofGeneralPortrait.eps.gz
 
 # 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)
+Patch0:         pg-4.1-Makefile.patch
+
+# Adapt the Emacs Lisp code to Emacs 24.  Applied upstream.
+Patch1:         pg-4.1-elisp.patch
+
+# Bring the desktop file up to date with current standards.
+Patch2:         pg-4.1-desktop.patch
 
 BuildArch:      noarch
-BuildRequires:  emacs emacs-el xemacs xemacs-devel texinfo-tex xemacs-packages-extra
+BuildRequires:  desktop-file-utils emacs emacs-el texinfo-tex texlive-utils
+
+# Remove these once Fedora 18 has reached EOL
+Obsoletes:      xemacs-%{pkg} < 4.0
+Obsoletes:      xemacs-%{pkg}-el < 4.0
+Provides:       xemacs-%{pkg} = %{version}-%{release}
+Provides:       xemacs-%{pkg}-el = %{version}-%{release}
 
 %description
 Proof General is a generic front-end for proof assistants (also known
@@ -76,8 +40,8 @@ assistant in an interactive manner:
   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 integrates with Emacs Unicode support for some provers to provide
+  output using proper mathematical symbols.
 - It includes utilities for generating Emacs tags for proof scripts,
   allowing for easy navigation.
 
@@ -88,9 +52,9 @@ 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(bin) >= %{_emacs_version}
 Requires:       emacs-common-%{pkg} = %{version}-%{release}
-# MMM Mode is separately packaged for emacs (but not for XEmacs)
+# MMM Mode is separately packaged for emacs
 Requires:       emacs-mmm
 
 %description -n emacs-%{pkg}
@@ -110,97 +74,84 @@ 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
+%patch2
 
-%build
+# Prepare the documentation image, and make the texi files use the right name
+mkdir web
+cp -p %{SOURCE1} web
+cd doc
+zcat ProofGeneralPortrait.eps.gz | epstopdf -f -o=ProofGeneralPortrait.pdf
+cd ..
+sed -i "s/image{ProofGeneral}/image{ProofGeneralPortrait}/" doc/*.texi
+
+# Default to using SMIE, since we ship recent enough Emacs versions
+sed "s/coq-use-smie nil/coq-use-smie t/" coq/coq.el > coq/coq.el.fixed
+touch -r coq/coq.el coq/coq.el.fixed
+mv -f coq/coq.el.fixed coq/coq.el
 
+%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
+# Remove .cvsignore files
+find . -name .cvsignore | xargs rm -f
 
 # 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
+for f in phox/square-root-2.phx; do
+  mv $f $f.old
+  iconv -f iso-8859-1 -t utf8 $f.old > $f
+  touch -r $f.old $f
+  rm $f.old
+done
+
+# Make full copies of emacs 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
+sed -r -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=%{_emacs_sitelispdir}|' \
+    -e 's|^PACKAGE=.*$|PACKAGE=%{pkg}|' \
+    -e 's|^(PGHOMEDEFAULT=).*|\1%{_emacs_sitelispdir}/%{pkg}|' \
+    bin/proofgeneral > .tmp
+touch -r bin/proofgeneral .tmp
+mv -f .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
+for f in `find . -maxdepth 1 -mindepth 1 ! -name emacs`; do
+  cp -pr $f emacs/$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 common_options PREFIX=%{buildroot}%{_prefix} DEST_PREFIX=%{_prefix} DESKTOP=%{buildroot}%{_datadir} 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}
+%define emacs_options ELISP_START=%{buildroot}%{_emacs_sitestartdir} ELISP=%{buildroot}%{_emacs_sitelispdir}/%{pkg} DEST_ELISP=%{_emacs_sitelispdir}/%{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}
+# Remove empty, obsolete directories
+rmdir %{buildroot}%{full_doc_dir}/lclam %{buildroot}%{full_doc_dir}/plastic
+
+# Fix executable bits on scripts
+chmod a+x %{buildroot}%{_bindir}/*
+
+# Validate the desktop file
+desktop-file-validate %{buildroot}%{_datadir}/applications/proofgeneral.desktop
 
 %post
 /sbin/install-info %{_infodir}/ProofGeneral.info* %{_infodir}/dir 2>/dev/null || :
 /sbin/install-info %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
+/bin/touch --no-create %{_datadir}/icons/hicolor &>/dev/null || :
 
 %preun
 if [ $1 -eq 0 ]; then
@@ -208,47 +159,45 @@ if [ $1 -eq 0 ]; then
   /sbin/install-info --delete %{_infodir}/PG-adapting.info* %{_infodir}/dir 2>/dev/null || :
 fi
 
+%postun
+if [ $1 -eq 0 ] ; then
+  /bin/touch --no-create %{_datadir}/icons/hicolor &>/dev/null
+  /usr/bin/gtk-update-icon-cache -f %{_datadir}/icons/hicolor &>/dev/null || :
+fi
+
+%posttrans
+/usr/bin/gtk-update-icon-cache -f %{_datadir}/icons/hicolor &>/dev/null || :
+
 %files
-%defattr(-,root,root,-)
 %{full_doc_dir}
-%{full_data_dir}
 %{full_man_dir}/*
 %{_infodir}/*
 %{_bindir}/*
+%{_datadir}/application-registry/%{pkg}.applications
+%{_datadir}/applications/%{pkg}.desktop
+%{_datadir}/icons/hicolor/*/%{pkg}.png
+%{_datadir}/mime-info/%{pkg}.*
+%{_datadir}/pixmaps/%{pkg}.png
 
 %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
+%{_emacs_sitelispdir}/%{pkg}/*
 # Exclude bundled mmm-mode, packaged separately
-%exclude %{emacs_lispdir}/%{pkg}/mmm
-%exclude %{emacs_lispdir}/%{pkg}/*/*.el
-%{emacs_startdir}/*.el
-%dir %{emacs_lispdir}/%{pkg}
+%exclude %{_emacs_sitelispdir}/%{pkg}/contrib
+%exclude %{_emacs_sitelispdir}/%{pkg}/*/*.el
+%{_emacs_sitestartdir}/*.el
+%dir %{_emacs_sitelispdir}/%{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
+%{_emacs_sitelispdir}/%{pkg}/*/*.el
 
 %changelog
+* Tue Jul 24 2012 Jerry James <loganjerry at gmail.com> 4.1-1
+- New upstream release
+- Upstream no longer supports XEmacs
+- Upstream no longer bundles X-Symbol
+- Remove unnecessary spec file elements (defattr, etc.)
+- Move desktop files into places where they will be used
+
 * Wed Jul 18 2012 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 3.7.1-7
 - Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild
 
diff --git a/pg-3.7.1-Makefile.patch b/pg-4.1-Makefile.patch
similarity index 76%
rename from pg-3.7.1-Makefile.patch
rename to pg-4.1-Makefile.patch
index 9fa7c4a..5581180 100644
--- a/pg-3.7.1-Makefile.patch
+++ b/pg-4.1-Makefile.patch
@@ -1,6 +1,6 @@
---- Makefile	2009-01-27 21:22:49.000000000 -0500
-+++ Makefile	2009-01-27 21:23:26.000000000 -0500
-@@ -215,8 +215,6 @@
+--- Makefile.orig	2010-10-10 16:56:56.000000000 -0600
++++ Makefile	2012-07-23 21:45:16.988966315 -0600
+@@ -193,8 +193,6 @@
  	cp -pf doc/proofgeneral.1 ${MANDIR}
  	mkdir -p ${INFODIR}
  	cp -pf doc/*.info ${INFODIR}
diff --git a/pg-4.1-desktop.patch b/pg-4.1-desktop.patch
new file mode 100644
index 0000000..ecdf001
--- /dev/null
+++ b/pg-4.1-desktop.patch
@@ -0,0 +1,19 @@
+--- ./etc/desktop/proofgeneral.desktop.orig	2010-10-10 16:57:01.000000000 -0600
++++ ./etc/desktop/proofgeneral.desktop	2012-07-24 11:44:35.384749567 -0600
+@@ -1,14 +1,12 @@
+ [Desktop Entry]
+ Type=Application
+ Version=1.0
+-Encoding=UTF-8
+ Name=Proof General
+ GenericName=Theorem proving environment
+ Comment=Organise your proofs!
+-Icon=proofgeneral.png
+-FilePattern=proofgeneral
++Icon=proofgeneral
+ TryExec=proofgeneral
+ Exec=proofgeneral %F
+ Terminal=false
+-Categories=Application;IDE;Development;TextEditor;Math
++Categories=Development;IDE;Utility;TextEditor;Education;Science;Math;
+ StartupWMClass=Emacs
diff --git a/pg-4.1-elisp.patch b/pg-4.1-elisp.patch
new file mode 100644
index 0000000..4666a8a
--- /dev/null
+++ b/pg-4.1-elisp.patch
@@ -0,0 +1,101 @@
+--- ./coq/coq-db.el.orig	2011-06-06 19:47:24.000000000 -0600
++++ ./coq/coq-db.el	2012-07-23 22:46:48.607320881 -0600
+@@ -183,9 +183,9 @@ for DB structure."
+ 
+ (defun coq-sort-menu-entries (menu)
+   (sort menu
+-	'(lambda (x y) (string<
+-			(downcase (elt x 0))
+-			(downcase (elt y 0))))))
++	#'(lambda (x y) (string<
++			 (downcase (elt x 0))
++			 (downcase (elt y 0))))))
+ 
+ (defun coq-build-menu-from-db (db &optional size)
+   "Take a keyword database DB and return a list of insertion menus for them.
+--- ./generic/proof-script.el.orig	2011-06-09 06:29:33.000000000 -0600
++++ ./generic/proof-script.el	2012-07-23 22:46:48.610320642 -0600
+@@ -431,13 +431,13 @@ Point must be after the locked region or
+ If called interactively or SWITCH is non-nil, switch to script buffer.
+ If called interactively, a mark is set at the current location with `push-mark'"
+   (interactive)
+-  (if (and proof-script-buffer (interactive-p))
++  (if (and proof-script-buffer (called-interactively-p 'interactive))
+       (push-mark))
+   (proof-with-script-buffer
+    (if ;; there is an active scripting buffer and it's not displayed
+        (and proof-script-buffer
+ 	    (not (get-buffer-window proof-script-buffer))
+-	    (or switch (interactive-p)))
++	    (or switch (called-interactively-p 'interactive)))
+        ;; display it
+        (switch-to-buffer proof-script-buffer))
+    (goto-char (proof-unprocessed-begin))))
+@@ -1260,7 +1260,7 @@ activation is considered to have failed
+       ;; immediately because scripting has been turned on now.
+       (if proof-activate-scripting-hook
+ 	  (let
+-	      ((activated-interactively	(interactive-p)))
++	      ((activated-interactively	(called-interactively-p 'interactive)))
+ 	    (setq proof-shell-last-output-kind nil)
+ 	    (run-hooks 'proof-activate-scripting-hook)
+ 	    ;; If activate scripting functions caused an error,
+--- ./generic/proof-menu.el.orig	2011-08-24 02:55:15.000000000 -0600
++++ ./generic/proof-menu.el	2012-07-23 22:46:48.614320322 -0600
+@@ -49,7 +49,7 @@ without adjusting window layout."
+   ;; trace buffer, etc.  (Makes less sense from the menu, though,
+   ;; where it seems more natural just to rotate from last position)
+   (cond
+-   ((and (interactive-p)
++   ((and (called-interactively-p 'interactive)
+ 	 (eq last-command 'proof-display-some-buffers))
+     (incf proof-display-some-buffers-count))
+    (t
+--- ./generic/proof-splash.el.orig	2010-10-10 16:57:05.000000000 -0600
++++ ./generic/proof-splash.el	2012-07-23 22:46:48.615320242 -0600
+@@ -287,7 +287,7 @@ binding to remove this buffer."
+ 	(progn
+ 	  ;; disable ordinary emacs splash
+ 	  (setq inhibit-startup-message t)
+-	  (proof-splash-display-screen (not (interactive-p))))
++	  (proof-splash-display-screen (not (called-interactively-p 'interactive))))
+       ;; Otherwise, a message
+       (message "Welcome to %s Proof General!" proof-assistant))
+     (setq proof-splash-seen t)))
+--- ./lib/scomint.el.orig	2011-01-25 03:06:57.000000000 -0700
++++ ./lib/scomint.el	2012-07-23 22:47:28.240165379 -0600
+@@ -251,7 +251,7 @@ NO-NEWLINE is non-nil."
+     (save-excursion
+       (condition-case nil
+ 	  (goto-char
+-	   (if (interactive-p) scomint-last-input-end scomint-last-output-start))
++	   (if (called-interactively-p 'interactive) scomint-last-input-end scomint-last-output-start))
+ 	(error nil))
+       (while (re-search-forward "\r+$" pmark t)
+ 	(replace-match "" t t)))))
+--- ./isar/isabelle-system.el.orig	2010-10-10 16:57:07.000000000 -0600
++++ ./isar/isabelle-system.el	2012-07-23 22:46:48.616320162 -0600
+@@ -292,7 +292,8 @@ for you, you should disable this behavio
+   "Refresh isabelle-logics-menu-entries, returning new entries."
+   (interactive)
+   (if (and isabelle-refresh-logics
+-	   (or isabelle-time-to-refresh-logics (interactive-p)))
++	   (or isabelle-time-to-refresh-logics
++	       (called-interactively-p 'interactive)))
+       (progn
+ 	(setq isabelle-logics-available (isa-tool-list-logics))
+ 	(isabelle-logics-menu-calculate)
+--- ./phox/phox-lang.el.orig	2010-10-10 16:57:10.000000000 -0600
++++ ./phox/phox-lang.el	2012-07-23 22:46:48.617320082 -0600
+@@ -7,7 +7,10 @@
+ (require 'cl)				; for case
+ 
+ (defvar phox-lang
+-  (let* ((s1 (getenv "LANG")) (s2 (getenv "LC_LANG")) (s (substring (if s1 s1 (if s2 s2 "en")) 0 2)))
++  (let* ((s1 (getenv "LANG"))
++	 (s2 (getenv "LC_LANG"))
++	 (loc (if s1 s1 (if s2 s2 "en")))
++	 (s (if (> (length loc) 1) (substring loc 0 2) loc)))
+     (cond
+       ((or (string= s "en") (string= s "us")) 'en)
+       ((string= s "fr") 'fr)
diff --git a/sources b/sources
index a06446c..6e2e056 100644
--- a/sources
+++ b/sources
@@ -1 +1,2 @@
-eebfff672b5941823fe893075316b02e  ProofGeneral-3.7.1.tgz
+a04ebe2c6b56a4fd6c16a070ea7fe3a9  ProofGeneral-4.1.tgz
+211195547064f1281b7333c93bd5a0b4  ProofGeneralPortrait.eps.gz


More information about the scm-commits mailing list