Skip site navigation (1)Skip section navigation (2)
Date:      Thu, 12 Apr 2012 01:43:35 -0700
From:      Timothy Beyer <beyert@cs.ucr.edu>
To:        FreeBSD-gnats-submit@FreeBSD.org
Cc:        Timothy Beyer <beyert@cs.ucr.edu>
Subject:   ports/166867: update port and fix build: math/proofgeneral
Message-ID:  <87lim1gx1k.wl@fastmail.fm>
Resent-Message-ID: <201204120850.q3C8oCYx064316@freefall.freebsd.org>

next in thread | raw e-mail | index | archive | help

>Number:         166867
>Category:       ports
>Synopsis:       update port and fix build: math/proofgeneral
>Confidential:   no
>Severity:       non-critical
>Priority:       low
>Responsible:    freebsd-ports-bugs
>State:          open
>Quarter:        
>Keywords:       
>Date-Required:
>Class:          maintainer-update
>Submitter-Id:   current-users
>Arrival-Date:   Thu Apr 12 08:50:12 UTC 2012
>Closed-Date:
>Last-Modified:
>Originator:     Timothy Beyer
>Release:        FreeBSD 9.0-RELEASE i386
>Organization:
no organization
>Environment:
System: FreeBSD aeonserv.aeonnet 9.0-RELEASE FreeBSD 9.0-RELEASE #9: Fri Mar 9 00:02:30 PST 2012 root@aeonserv.aeonnet:/usr/obj/usr/src/sys/CUSTOM i386

>Description:

- Update port to version 4.1

- Fix build on amd64 (and likely all other architectures)

- XEmacs is no longer supported by proofgeneral developers, so only GNU Emacs may be used

- simplify some of the patches by using MAKE_ARGS when possible.

- get rid of USE_GNOME, since there is nothing Gnome related about this port

- Omit Pdf compilation

Explanation:

Due to recent changes to the port print/texinfo, math/proofgeneral (3.7.1) no
longer compiles properly.  (due to issues compiling the info files with the
newer texinfo) The new version of math/proofgeneral (this one) does not have
this issue, because it works with recent versions of texinfo, as it should.

However, the pdf compilation in the newest version requires a newer version of
latex than what is available in the tetex distribution.  (the latex in texlive
would be sufficient if that feature is desired) Therefore, pdf compilation is
ommitted, due to this issue.

This is a fairly important update, because the current version in ports no
longer compiles, according to error logs on portsmon.

>How-To-Repeat:
apply the patch and build

>Fix:
    Apply the patch and build

--- proofgeneral.diff begins here ---
Index: math/proofgeneral/Makefile
==================================================================
--- math/proofgeneral/Makefile
+++ math/proofgeneral/Makefile
@@ -4,56 +4,43 @@
 #
 # $FreeBSD: ports/math/proofgeneral/Makefile,v 1.27 2011/06/18 16:13:31 hrs Exp $
 #
 
 PORTNAME=	proofgeneral
-PORTVERSION=	3.7.1
-PORTREVISION=	5
+PORTVERSION=	4.1
 CATEGORIES=	math elisp
 MASTER_SITES=	http://proofgeneral.inf.ed.ac.uk/releases/
-DISTNAME=	ProofGeneral-3.7.1
+DISTNAME=	ProofGeneral-${PORTVERSION}
 EXTRACT_SUFX=	.tgz
 
 MAINTAINER=	beyert@cs.ucr.edu
 COMMENT=	A generic interface for proof assistants
 
+LICENSE=	GPLv2
+LICENSE_FILE=	${WRKSRC}/COPYING
+
 PKGNAMESUFFIX+=	-${EMACS_NAME}
 
 BUILD_DEPENDS+=	bash:${PORTSDIR}/shells/bash
 RUN_DEPENDS+=	${LOCALBASE}/share/icons/hicolor/index.theme:${PORTSDIR}/misc/hicolor-icon-theme
 
-#
-# Unless EMACS_PORT_NAME is overriden by the user,
-# use any installed version of [X]Emacs.
-#
-# If there is none installed, use xemacs21-mule.
-#
-.if !defined(EMACS_PORT_NAME)
-.if !exists(${LOCALBASE}/bin/emacs)
-EMACS_PORT_NAME=xemacs21-mule
-BUILD_DEPENDS+=	${LOCALBASE}/bin/xemacs:${PORTSDIR}/editors/${EMACS_PORT_NAME}
-RUN_DEPENDS+=	${LOCALBASE}/bin/xemacs:${PORTSDIR}/editors/${EMACS_PORT_NAME}
-
-# xemacs21-mule does not depend on xemacs-packages, so add a dependency here
-BUILD_DEPENDS+=	${LOCALBASE}/lib/xemacs/xemacs-packages/lisp/xlib/xlib-xlib.el:${PORTSDIR}/editors/xemacs-packages
-RUN_DEPENDS+=	${LOCALBASE}/lib/xemacs/xemacs-packages/lisp/xlib/xlib-xlib.el:${PORTSDIR}/editors/xemacs-packages
-.else
-EMACS_PORT_NAME=emacs
-BUILD_DEPENDS+=	${LOCALBASE}/bin/emacs:${PORTSDIR}/editors/${EMACS_PORT_NAME}
-RUN_DEPENDS+=	${LOCALBASE}/bin/emacs:${PORTSDIR}/editors/${EMACS_PORT_NAME}
-.endif
-.endif
-
 USE_EMACS=	yes
 USE_GMAKE=	yes
-USE_GNOME=	gnomehier
 INSTALLS_ICONS=	yes
 USE_PERL5=	yes
 
 .include <bsd.port.pre.mk>
 
-MAKE_ARGS+=	EMACS_NAME=${EMACS_NAME} EMACS_SITE_LISPDIR=${EMACS_SITE_LISPDIR}
+MAKE_ARGS+=	PREFIX="${LOCALBASE}" DEST_PREFIX="${PREFIX}" MAKE="${GMAKE}" \
+	DOCDIR="${DOCSDIR}" MANDIR="${PREFIX}/man/man1" INFODIR="${PREFIX}/info" \
+	BINDIR="${PREFIX}/bin" DESKTOP="${PREFIX}/share" \
+	ELISPP="${EMACS_SITE_LISPDIR}/ProofGeneral" \
+	ELISP="${PREFIX}/${EMACS_SITE_LISPDIR}/ProofGeneral" \
+	ELISP_START="${PREFIX}/${EMACS_SITE_LISPDIR}/site-start.d" \
+	EMACS="${EMACS_NAME}" EMACS_NAME="${EMACS_NAME}" \
+	DEST_ELISP="${PREFIX}/${EMACS_SITE_LISPDIR}/ProofGeneral" \
+	EMACS_SITE_LISPDIR="${EMACS_SITE_LISPDIR}"
 
 SUB_FILES=	pkg-message
 SUB_LIST=	EMACS_SITE_LISPDIR=${EMACS_SITE_LISPDIR}
 
 MAN1=		proofgeneral.1
@@ -60,12 +47,11 @@
 MANCOMPRESSED=	no
 INFO=		PG-adapting ProofGeneral
 
 .if !defined(NOPORTDOCS)
 MAKE_ARGS+=	DOCSDIR=${DOCSDIR} INSTALLDOC=install-doc
-BUILD_DEPENDS+=	latex:${PORTSDIR}/print/teTeX-base \
-		texi2pdf:${PORTSDIR}/print/texinfo
+BUILD_DEPENDS+=	texi2html:${PORTSDIR}/print/texinfo
 .endif
 
 post-patch:
 	@${REINPLACE_CMD} -e 's,%%PREFIX%%,${PREFIX},' \
 		${WRKSRC}/etc/desktop/proofgeneral.desktop

Index: math/proofgeneral/distinfo
==================================================================
--- math/proofgeneral/distinfo
+++ math/proofgeneral/distinfo
@@ -1,2 +1,2 @@
-SHA256 (ProofGeneral-3.7.1.tgz) = e613aa2f24564465f450b06b2d804e6815b220652c9f778e3d3471b644fdaa93
-SIZE (ProofGeneral-3.7.1.tgz) = 2023176
+SHA256 (ProofGeneral-4.1.tgz) = 2a264d46b48185cf1a6ebcca958e59171ea670fb0fc82ba46b8e1d6918ea7dc7
+SIZE (ProofGeneral-4.1.tgz) = 1428499

Index: math/proofgeneral/files/patch-Makefile
==================================================================
--- math/proofgeneral/files/patch-Makefile
+++ math/proofgeneral/files/patch-Makefile
@@ -1,78 +1,22 @@
---- Makefile.orig	2008-02-01 00:06:38.000000000 +1100
-+++ Makefile	2008-07-29 13:09:58.000000000 +1000
-@@ -21,7 +21,7 @@
+--- Makefile.orig	2010-10-10 15:56:56.000000000 -0700
++++ Makefile	2012-04-11 22:30:19.000000000 -0700
+@@ -41,7 +41,7 @@
+ ELISP_EXTRAS=isar/interface isar/isartags
+ EXTRA_DIRS = images
  
- # Set this to "emacs" or "xemacs" according to your version of Emacs.
- # NB: this is also used to set default install path names below.
--EMACS=$(shell if [ -z "`which emacs`" ]; then echo xemacs; else echo emacs; fi)
-+EMACS=${EMACS_NAME}
+-DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER doc/*.pdf
++DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER
+ DOC_EXAMPLES=acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf
+ DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS 
  
- # We default to /usr rather than /usr/local because installs of
- # desktop and doc files under /usr/local are unlikely to work with
-@@ -29,8 +29,7 @@
- # individually before the install section.
- # NB: DEST_PREFIX is used for final destination prefix, in case we're
- # packaging into a build prefix rather than live root (e.g. in rpmbuild).
--PREFIX=/usr
--DEST_PREFIX=/usr
-+DEST_PREFIX=${PREFIX}
+@@ -135,22 +135,23 @@
+ MANDIR=${PREFIX}/share/man/man1
+ INFODIR=${PREFIX}/share/info
  
- PWD=$(shell pwd)
- 
-@@ -75,8 +74,8 @@
- ##	     old .elc's and re-compile.
- ##
- compile: $(EL) x-symbol/lisp/*.el
--	lastemacs=`cat .byte-compile 2>/dev/null || echo `; if [ "$$lastemacs" != "" ] && [ "$$lastemacs" != "$(EMACS)" ]; then rm -f .byte-compile $(ELC) x-symbol/lisp/*.elc; fi
--	make .byte-compile
-+	lastemacs=`cat .byte-compile 2>/dev/null || echo `; if [ "$$lastemacs" != "" ] && [ "$$lastemacs" != "$(EMACS_NAME)" ]; then rm -f .byte-compile $(ELC) x-symbol/lisp/*.elc; fi
-+	$(MAKE) .byte-compile
- 
- ## Compiling can show up errors in the code, but be wary of fixing obsoletion
- ## or argument call warnings unless they're valid for both Emacsen.
-@@ -85,10 +84,10 @@
- 	@echo "****************************************************************"
- 	@echo " Byte compiling... "
- 	@echo "****************************************************************"
--	make elc
-+	$(MAKE) elc
- 	@echo " Byte compiling X-Symbol..."
- 	(cd x-symbol/lisp; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
--	echo $(EMACS) > $(@)
-+	echo $(EMACS_NAME) > $(@)
- 	@echo "****************************************************************"
- 	@echo " Finished."
- 	@echo "****************************************************************"
-@@ -137,39 +136,35 @@
- # Set Elisp directories according to paths used in Red Hat RPMs
- # (which may or may not be official Emacs policy).  We generate
- # a pg-init.el file which loads the appropriate proof-site.el.
--ifeq ($(EMACS),xemacs) 
--ELISPP=share/xemacs/site-packages/lisp/ProofGeneral
--ELISP_START=${PREFIX}/share/xemacs/site-packages/lisp/site-start.d
--else
--ELISPP=share/${EMACS}/site-lisp/ProofGeneral
--ELISP_START=${PREFIX}/share/${EMACS}/site-lisp/site-start.d
--endif
-+ELISPP=${EMACS_SITE_LISPDIR}/ProofGeneral
-+ELISP_START=${PREFIX}/${EMACS_SITE_LISPDIR}/site-start.d
- 
- ELISP=${PREFIX}/${ELISPP}
- DEST_ELISP=${DEST_PREFIX}/${ELISPP}
- 
- BINDIR=${PREFIX}/bin
- DESKTOP=${PREFIX}/share
--DOCDIR=${PREFIX}/share/doc/ProofGeneral
--MANDIR=${PREFIX}/share/man/man1
--INFODIR=${PREFIX}/share/info
-+DOCDIR=${DOCSDIR}
-+MANDIR=${PREFIX}/man/man1
-+INFODIR=${PREFIX}/info
- 
 -install: install-desktop install-elisp install-bin install-init
-+install: install-desktop install-elisp install-bin install-init install-man ${INSTALLDOC}
++install: install-desktop install-elisp install-bin install-init ${INSTALLDOC}
  
  install-desktop:
 -	mkdir -p ${DESKTOP}/icons/hicolor/16x16
 -	cp etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16
 -	mkdir -p ${DESKTOP}/icons/hicolor/32x32
@@ -101,11 +45,11 @@
 +	${BSD_INSTALL_DATA} etc/desktop/mime-info/proofgeneral.keys ${DESKTOP}/mime-info/
 +
  # backwards compatibility with old linuxes
  	mkdir -p ${DESKTOP}/application-registry
  	cp etc/desktop/application-registry/proofgeneral.applications ${DESKTOP}/application-registry
-@@ -190,15 +185,23 @@
+@@ -168,15 +169,23 @@
  install-el:
  	mkdir -p ${ELISP}
  	for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
 -	for f in ${ELISP_DIRS}; do cp -pf $$f/*.el ${ELISP}/$$f; done
 -	for f in ${EXTRA_DIRS}; do cp -prf $$f/* ${ELISP}/$$f; done
@@ -130,30 +74,28 @@
 +	for f in ${ELISP_DIRS}; do ${BSD_INSTALL_DATA} $$f/*.elc ${ELISP}/$$f; done
 +	for f in ${ELISP_EXTRAS}; do ${BSD_INSTALL_SCRIPT} $$f ${ELISP}/$$f; done
  
  install-init:
  	mkdir -p ${ELISP_START}
-@@ -208,24 +211,33 @@
+@@ -186,18 +195,23 @@
  
  install-bin: scripts
  	mkdir -p ${BINDIR}
 -	cp -pf ${BIN_SCRIPTS} ${BINDIR}
 +	${BSD_INSTALL_SCRIPT} ${BIN_SCRIPTS} ${BINDIR}
  
 -install-doc: doc.info doc.pdf
-+install-man: doc.info
++install-doc: doc.html
  	mkdir -p ${MANDIR}
 -	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
 +	${BSD_INSTALL_MAN} doc/proofgeneral.1 ${MANDIR}
 +	${BSD_INSTALL_MAN} doc/PG-adapting.info ${INFODIR}
 +	${BSD_INSTALL_MAN} doc/ProofGeneral.info ${INFODIR}
-+
-+install-doc: doc.pdf doc.html
  	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
 +	for f in ${DOC_FILES}; do ${BSD_INSTALL_MAN} $$f ${DOCDIR}; done
 +	for f in ${DOC_EXAMPLES}; do mkdir -p ${DOCDIR}/`dirname $$f`; \
@@ -162,18 +104,8 @@
 +	for f in doc/ProofGeneral/*.html; do \
 +		${BSD_INSTALL_MAN} $$f ${DOCDIR}/ProofGeneral/`basename $$f`; done
 +	mkdir -p ${DOCDIR}/PG-adapting
 +	for f in doc/PG-adapting/*.html; do \
 +		${BSD_INSTALL_MAN} $$f ${DOCDIR}/PG-adapting/`basename $$f`; done
-+	for f in ProofGeneral.pdf PG-adapting.pdf; do \
-+		${BSD_INSTALL_MAN} doc/$$f ${DOCDIR}/$$f; done
  
  doc: FORCE
--	(cd doc; make EMACS=$(EMACS) $*)
-+	(cd doc; $(MAKE) EMACS=$(EMACS) $*)
- 
- doc.%: FORCE
--	(cd doc; make EMACS=$(EMACS) $*)
-+	(cd doc; $(MAKE) EMACS=$(EMACS) $*)
- 
- ##
- ## scripts: try to patch bash and perl scripts with correct paths
+ 	(cd doc; $(MAKE) EMACS=$(EMACS) $*)

DELETED math/proofgeneral/files/patch-doc-Makefile.doc
Index: math/proofgeneral/files/patch-doc-Makefile.doc
==================================================================
--- math/proofgeneral/files/patch-doc-Makefile.doc
+++ math/proofgeneral/files/patch-doc-Makefile.doc
@@ -1,17 +0,0 @@
---- doc/Makefile.doc.orig	2008-02-23 15:11:19.000000000 +1100
-+++ doc/Makefile.doc	2008-02-23 15:10:59.000000000 +1100
-@@ -155,10 +155,10 @@
- ##	  (developer use only!)
- ##
- ## remove this for now: no magic during dist ../*/*.el 
--$(DOCNAME).texi: 
--	$(MAKE) magic
--magic:
--	$(EMACS) $(EMACSFLAGS) -batch -l ./docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
-+#$(DOCNAME).texi: 
-+#	$(MAKE) magic
-+#magic:
-+#	$(EMACS) $(EMACSFLAGS) -batch -l ./docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
- 
- debugmagic:
- 	$(EMACS) $(EMACFLAGS)  -eval '(setq debug-on-error t)' -l ./docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer

ADDED    math/proofgeneral/files/patch-doc_Makefile.doc
Index: math/proofgeneral/files/patch-doc_Makefile.doc
==================================================================
--- math/proofgeneral/files/patch-doc_Makefile.doc
+++ math/proofgeneral/files/patch-doc_Makefile.doc
@@ -0,0 +1,66 @@
+--- doc/Makefile.doc.orig	2011-05-05 10:46:27.000000000 -0700
++++ doc/Makefile.doc	2012-04-11 22:03:35.000000000 -0700
+@@ -40,16 +40,13 @@
+ 
+ TMPFILE=pgt
+ 
+-.SUFFIXES:  .texi .info .html .pdf .gz
++.SUFFIXES:  .texi .info .html .gz
+ 
+ default: doc
+ 
+ .texi.info:
+ 	$(MAKEINFO) $< 
+ 
+-.texi.pdf:
+-	$(TEXI2PDF) $< 
+-
+ .texi.html:	
+ 	$(TEXI2HTML) --output $* $< 
+ 
+@@ -61,21 +58,19 @@
+ 	gzip -f -9 $*
+ 
+ ## 
+-## doc : build pdf, info files from $(DOCNAME).texi
++## doc : build info files from $(DOCNAME).texi
+ ##
+-doc:	pdf info
++doc:	info
+ 
+ ## 
+ ## all : build all documentation targets
+ ##
+-all:    html info pdf
++all:    html info
+ 
+ ##
+ ## dist: build distribution targets
+ ##
+-dist:   info html pdf
+-
+-pdf:    $(DOCNAME).pdf
++dist:   info html
+ 
+ # da: target is a fake: we actually make in a subdir
+ html:   $(DOCNAME).html
+@@ -97,18 +92,13 @@
+ ## distclean: Remove documentation targets
+ ##
+ distclean:   clean
+-	rm -rf $(DOCNAME).info* $(DOCNAME).pdf $(DOCNAME)
++	rm -rf $(DOCNAME).info* $(DOCNAME)
+ 
+ ##
+ ## texi: update magic comments in texi from docstrings in code.
+ ##	  (developer use only!)
+ ##       Must be run from source .els otherwise function arguments lost
+ ##
+-$(DOCNAME).texi: 
+-	$(MAKE) magic
+-magic:
+-	(cd ..; make clean)
+-	$(EMACS) $(EMACSFLAGS) -batch -l ./docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
+ 
+ debugmagic:
+ 	$(EMACS) $(EMACFLAGS)  -eval '(setq debug-on-error t)' -l ./docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer

Index: math/proofgeneral/files/patch-etc_desktop_proofgeneral.desktop
==================================================================
--- math/proofgeneral/files/patch-etc_desktop_proofgeneral.desktop
+++ math/proofgeneral/files/patch-etc_desktop_proofgeneral.desktop
@@ -1,11 +1,11 @@
---- etc/desktop/proofgeneral.desktop.orig	Thu Dec  8 07:40:38 2005
-+++ etc/desktop/proofgeneral.desktop	Thu Dec  8 07:41:03 2005
+--- etc/desktop/proofgeneral.desktop.orig	2012-04-11 20:39:33.000000000 -0700
++++ etc/desktop/proofgeneral.desktop	2012-04-11 20:41:16.000000000 -0700
 @@ -5,7 +5,7 @@
  Name=Proof General
  GenericName=Theorem proving environment
  Comment=Organise your proofs!
 -Icon=proofgeneral.png
 +Icon=%%PREFIX%%/share/pixmaps/proofgeneral.png
  FilePattern=proofgeneral
  TryExec=proofgeneral
  Exec=proofgeneral %F

DELETED math/proofgeneral/files/patch-isar-interface
Index: math/proofgeneral/files/patch-isar-interface
==================================================================
--- math/proofgeneral/files/patch-isar-interface
+++ math/proofgeneral/files/patch-isar-interface
@@ -1,11 +0,0 @@
---- isar/interface.orig	2008-07-29 13:22:58.000000000 +1000
-+++ isar/interface	2008-07-29 13:25:10.000000000 +1000
-@@ -60,7 +60,7 @@
- GEOMETRY=""
- KEYWORDS=""
- LOGIC="$ISABELLE_LOGIC"
--PROGNAME="emacs"
-+PROGNAME="%%EMACS_NAME%%"
- INITFILE="true"
- WINDOWSYSTEM="true"
- XSYMBOL=""

ADDED    math/proofgeneral/files/patch-isar_interface
Index: math/proofgeneral/files/patch-isar_interface
==================================================================
--- math/proofgeneral/files/patch-isar_interface
+++ math/proofgeneral/files/patch-isar_interface
@@ -0,0 +1,11 @@
+--- isar/interface.orig	2011-01-27 11:54:20.000000000 -0800
++++ isar/interface	2012-04-11 20:26:06.000000000 -0700
+@@ -57,7 +57,7 @@
+ UNICODE=""
+ FONT=""
+ GEOMETRY=""
+-PROGNAME="emacs"
++PROGNAME="%%EMACS_NAME%%"
+ INITFILE="true"
+ WINDOWSYSTEM="true"
+ UNICODE_SYMBOLS=""

Index: math/proofgeneral/pkg-plist
==================================================================
--- math/proofgeneral/pkg-plist
+++ math/proofgeneral/pkg-plist
@@ -1,15 +1,111 @@
 bin/coqtags
 bin/isartags
 bin/legotags
 bin/proofgeneral
+share/application-registry/proofgeneral.applications
+share/applications/proofgeneral.desktop
+%%PORTDOCS%%%%DOCSDIR%%/AUTHORS
+%%PORTDOCS%%%%DOCSDIR%%/BUGS
+%%PORTDOCS%%%%DOCSDIR%%/CHANGES
+%%PORTDOCS%%%%DOCSDIR%%/COMPATIBILITY
+%%PORTDOCS%%%%DOCSDIR%%/COPYING
+%%PORTDOCS%%%%DOCSDIR%%/INSTALL
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_1.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_10.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_11.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_12.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_13.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_14.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_15.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_16.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_17.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_18.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_19.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_2.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_3.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_4.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_5.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_6.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_7.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_8.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_9.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_abt.html
+%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_toc.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_1.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_10.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_11.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_12.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_13.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_14.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_15.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_16.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_17.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_18.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_19.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_2.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_20.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_21.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_22.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_23.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_3.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_4.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_5.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_6.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_7.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_8.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_9.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_abt.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_fot.html
+%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_toc.html
+%%PORTDOCS%%%%DOCSDIR%%/README
+%%PORTDOCS%%%%DOCSDIR%%/REGISTER
+%%PORTDOCS%%%%DOCSDIR%%/acl2/example.acl2
+%%PORTDOCS%%%%DOCSDIR%%/acl2/root2.acl2
+%%PORTDOCS%%%%DOCSDIR%%/hol98/example.sml
+%%PORTDOCS%%%%DOCSDIR%%/hol98/root2.sml
+%%PORTDOCS%%%%DOCSDIR%%/isar/Example-Tokens.thy
+%%PORTDOCS%%%%DOCSDIR%%/isar/Example.thy
+%%PORTDOCS%%%%DOCSDIR%%/lego/example.l
+%%PORTDOCS%%%%DOCSDIR%%/lego/example2.l
+%%PORTDOCS%%%%DOCSDIR%%/lego/root2.l
+%%PORTDOCS%%%%DOCSDIR%%/pgshell/example.pgsh
+%%PORTDOCS%%%%DOCSDIR%%/phox/example.phx
+%%PORTDOCS%%%%DOCSDIR%%/phox/square-root-2.phx
+%%PORTDOCS%%%%DOCSDIR%%/twelf/example.elf
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2/acl2.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2/acl2.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2/x-symbol-acl2.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2/x-symbol-acl2.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/ccc/ccc.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/ccc/ccc.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-auto.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-auto.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-class.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-class.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-cmds.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-cmds.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-compat.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-compat.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-cweb.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-cweb.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-mason.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-mason.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-mode.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-mode.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-region.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-region.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-rpm.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-rpm.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-sample.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-sample.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-univ.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-univ.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-utils.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-utils.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-vars.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm/mmm-vars.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-abbrev.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-abbrev.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-autotest.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-autotest.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-db.el
@@ -24,48 +120,45 @@
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-syntax.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-unicode-tokens.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq-unicode-tokens.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/coq.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/x-symbol-coq.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/coq/x-symbol-coq.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/demoisa/demoisa-easy.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/demoisa/demoisa-easy.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/demoisa/demoisa.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/demoisa/demoisa.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-assoc.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-assoc.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-autotest.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-autotest.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-custom.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-custom.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-goals.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-goals.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-movie.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-movie.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-pamacs.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-pamacs.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-pbrpm.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-pbrpm.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-pgip.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-pgip.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-response.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-response.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-thymodes.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-thymodes.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-user.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-user.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-vars.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-vars.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-xml.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/pg-xml.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-autoloads.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-autoloads.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-auxmodes.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-auxmodes.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-config.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-config.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-depends.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-depends.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-easy-config.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-easy-config.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-faces.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-faces.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-indent.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-indent.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-maths-menu.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-maths-menu.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-menu.el
@@ -84,20 +177,18 @@
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-syntax.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-toolbar.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-toolbar.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-unicode-tokens.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-unicode-tokens.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-useropts.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-useropts.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-utils.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-utils.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-x-symbol.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof-x-symbol.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic/proof.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/hol98/hol98.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/hol98/hol98.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/hol98/x-symbol-hol98.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/hol98/x-symbol-hol98.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/ProofGeneral.gif
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/ProofGeneral.jpg
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/README
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-abort.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-abort.xpm
@@ -111,10 +202,12 @@
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-goal.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-goto.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-goto.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-help.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-help.xpm
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-home.png
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-home.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-info.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-info.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-interrupt.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-interrupt.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-next.png
@@ -129,28 +222,11 @@
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-state.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-undo.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-undo.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-use.png
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/epg-use.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/gimp/.cvsignore
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/hiddenproof.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-abort.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-command.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-context.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-find.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-goal.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-goto.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-help.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-info.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-interrupt.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-next.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-qed.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-restart.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-retract.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-state.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-undo.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/images/pg-use.xpm
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/interface
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/interface-setup.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/interface-setup.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isabelle-system.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isabelle-system.elc
@@ -160,84 +236,47 @@
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-find-theorems.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-keywords.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-keywords.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-mmm.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-mmm.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-profiling.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-profiling.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-syntax.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-syntax.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-unicode-tokens.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar-unicode-tokens.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isar.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/isartags
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/x-symbol-isar.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/isar/x-symbol-isar.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lclam/lclam.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lclam/lclam.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lego/lego-syntax.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lego/lego-syntax.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lego/lego.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lego/lego.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lego/x-symbol-lego.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lego/x-symbol-lego.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/bufhist.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/bufhist.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/holes-load.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/holes-load.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/holes.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/holes.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/local-vars-list.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/local-vars-list.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/maths-menu.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/maths-menu.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/pg-dev.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/pg-dev.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/pg-fontsets.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/pg-fontsets.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/proof-compat.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/proof-compat.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/span-extent.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/span-extent.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/span-overlay.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/span-overlay.elc
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/scomint.el
+%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/scomint.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/span.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/span.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/texi-docstring-magic.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/texi-docstring-magic.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/unicode-chars.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/unicode-chars.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/unicode-tokens.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/unicode-tokens.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/xml-fixed.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/lib/xml-fixed.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-auto.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-auto.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-class.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-class.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-cmds.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-cmds.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-compat.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-compat.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-cweb.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-cweb.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-mason.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-mason.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-mode.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-mode.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-noweb.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-noweb.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-region.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-region.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-rpm.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-rpm.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-sample.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-sample.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-univ.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-univ.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-utils.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-utils.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-vars.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm/mmm-vars.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/pgshell/pgshell.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/pgshell/pgshell.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox-extraction.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox-extraction.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox-font.el
@@ -254,285 +293,38 @@
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox-sym-lock.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox-tags.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox-tags.elc
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox.el
 %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/phox.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/x-symbol-phox.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/phox/x-symbol-phox.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/plastic/plastic-syntax.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/plastic/plastic-syntax.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/plastic/plastic.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/plastic/plastic.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/twelf-font.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/twelf-font.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/twelf-old.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/twelf-old.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/twelf.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/twelf.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/x-symbol-twelf.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf/x-symbol-twelf.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/README.x-symbol-for-ProofGeneral
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/Makefile.emacs
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/RIP.xbm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/bigfonts/README
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/bigfonts/fonts.tar
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/colormap138.xpm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/drawing.xbm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/escherknot.xbm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts-ttf/README
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts-ttf/isaxsym.ttf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts-ttf/XSymb0Medium.ttf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts-ttf/XSymb1Medium.ttf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/2helvR12.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/2helvR14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/3helvR12.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/3helvR14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/5etl14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/5etl16.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/Makefile
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/heriR12.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/heriR14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/makesub
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/nilxs.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb0_12.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb0_14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb0_18.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb0_24.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb1_12.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb1_14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb1_18.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts/xsymb1_24.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/2helvR12sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/2helvR12sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/2helvR14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/2helvR14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/3helvR12sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/3helvR12sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/3helvR14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/3helvR14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/5etl14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/5etl14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/5etl16sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/5etl16sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR12sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR12sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR18sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR18sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR24sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/helvR24sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/heriR12sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/heriR12sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/heriR14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/heriR14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_12sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_12sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_18sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_18sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_24sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb0_24sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_12sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_12sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_14sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_14sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_18sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_18sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_24sub.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts/xsymb1_24sup.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/hourglass.xbm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/origfonts/helvR12.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/origfonts/helvR14.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/origfonts/helvR18.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/origfonts/helvR24.bdf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/2helvR12.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/2helvR12sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/2helvR12sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/2helvR14.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/2helvR14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/2helvR14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/3helvR12.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/3helvR12sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/3helvR12sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/3helvR14.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/3helvR14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/3helvR14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/5etl14.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/5etl14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/5etl14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/5etl16.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/5etl16sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/5etl16sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/fonts.dir
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR12sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR12sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR18sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR18sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR24sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/helvR24sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/heriR12.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/heriR12sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/heriR12sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/heriR14.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/heriR14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/heriR14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/nilxs.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_12.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_12sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_12sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_14.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_18.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_18sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_18sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_24.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_24sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb0_24sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_12.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_12sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_12sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_14.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_14sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_14sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_18.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_18sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_18sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_24.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_24sub.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf/xsymb1_24sup.pcf
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/recycle.xbm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/termlock.xbm
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/utf-unicode-list.txt
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/info/x-symbol.info
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/ChangeLog
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/Makefile
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/_pkg.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/auto-autoloads.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/custom-load.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/makefile.pkg
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-autoloads.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-bib.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-bib.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-emacs.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-hooks.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-hooks.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-image.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-image.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-macs.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-macs.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-mule.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-mule.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-nomule.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-sgml.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-sgml.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-tex.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-tex.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-texi.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-texi.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-unichars.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-unicode-extras.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-unicode.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-vars.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-vars.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol-xmacs.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol.el
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp/x-symbol.elc
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/man/Makefile
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/man/x-symbol.css
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/man/x-symbol.init
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/man/x-symbol.texi
-%%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/pkginfo/MANIFEST.x-symbol
 %%EMACS_SITE_LISPDIR%%/site-start.d/pg-init.el
-share/application-registry/proofgeneral.applications
-share/applications/proofgeneral.desktop
-share/pixmaps/proofgeneral.png
 share/icons/hicolor/16x16/proofgeneral.png
 share/icons/hicolor/32x32/proofgeneral.png
 share/icons/hicolor/48x48/proofgeneral.png
-share/mime-info/proofgeneral.mime
 share/mime-info/proofgeneral.keys
-%%PORTDOCS%%%%DOCSDIR%%/AUTHORS
-%%PORTDOCS%%%%DOCSDIR%%/BUGS
-%%PORTDOCS%%%%DOCSDIR%%/CHANGES
-%%PORTDOCS%%%%DOCSDIR%%/COMPATIBILITY
-%%PORTDOCS%%%%DOCSDIR%%/COPYING
-%%PORTDOCS%%%%DOCSDIR%%/INSTALL
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting.pdf
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_1.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_10.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_11.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_12.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_13.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_14.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_15.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_16.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_17.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_18.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_19.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_2.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_3.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_4.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_5.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_6.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_7.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_8.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_9.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_abt.html
-%%PORTDOCS%%%%DOCSDIR%%/PG-adapting/PG-adapting_toc.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral.pdf
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_1.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_10.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_11.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_12.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_13.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_14.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_15.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_16.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_17.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_18.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_19.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_2.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_20.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_21.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_3.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_4.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_5.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_6.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_7.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_8.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_9.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_abt.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_fot.html
-%%PORTDOCS%%%%DOCSDIR%%/ProofGeneral/ProofGeneral_toc.html
-%%PORTDOCS%%%%DOCSDIR%%/README
-%%PORTDOCS%%%%DOCSDIR%%/REGISTER
-%%PORTDOCS%%%%DOCSDIR%%/acl2/example.acl2
-%%PORTDOCS%%%%DOCSDIR%%/acl2/root2.acl2
-%%PORTDOCS%%%%DOCSDIR%%/hol98/example.sml
-%%PORTDOCS%%%%DOCSDIR%%/hol98/root2.sml
-%%PORTDOCS%%%%DOCSDIR%%/isar/Example-Xsym.thy
-%%PORTDOCS%%%%DOCSDIR%%/isar/Example.thy
-%%PORTDOCS%%%%DOCSDIR%%/isar/KnasterTarski.thy
-%%PORTDOCS%%%%DOCSDIR%%/isar/Root2_Isar.thy
-%%PORTDOCS%%%%DOCSDIR%%/isar/Root2_Tactic.thy
-%%PORTDOCS%%%%DOCSDIR%%/isar/Tarski.thy
-%%PORTDOCS%%%%DOCSDIR%%/lclam/example.lcm
-%%PORTDOCS%%%%DOCSDIR%%/lego/example.l
-%%PORTDOCS%%%%DOCSDIR%%/lego/example2.l
-%%PORTDOCS%%%%DOCSDIR%%/lego/root2.l
-%%PORTDOCS%%%%DOCSDIR%%/pgshell/example.pgsh
-%%PORTDOCS%%%%DOCSDIR%%/phox/example.phx
-%%PORTDOCS%%%%DOCSDIR%%/phox/square-root-2.phx
-%%PORTDOCS%%%%DOCSDIR%%/plastic/test.lf
-%%PORTDOCS%%%%DOCSDIR%%/twelf/example.elf
+share/mime-info/proofgeneral.mime
+share/pixmaps/proofgeneral.png
+@dirrmtry share/mime-info
+@dirrmtry share/icons/hicolor/48x48
+@dirrmtry share/icons/hicolor/32x32
+@dirrmtry share/icons/hicolor/16x16
+@dirrmtry share/icons/hicolor
+@dirrmtry share/icons
+@dirrmtry %%EMACS_SITE_LISPDIR%%/site-start.d
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/pgshell
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/lego
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/images
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/hol98
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib/mmm
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/contrib
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/ccc
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2
+@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/twelf
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/plastic
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/phox
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/pgshell
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/lego
@@ -541,37 +333,10 @@
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/hol98
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/acl2
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/ProofGeneral
 %%PORTDOCS%%@dirrm %%DOCSDIR%%/PG-adapting
 %%PORTDOCS%%@dirrm %%DOCSDIR%%
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/pkginfo
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/man
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/lisp
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/info
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/pcf
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/origfonts
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/genfonts
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts-ttf
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/fonts
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc/bigfonts
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol/etc
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/x-symbol
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/twelf
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/plastic
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/phox
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/pgshell
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/mmm
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/lib
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/lego
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/lclam
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/isar
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/images/gimp
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/images
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/hol98
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/generic
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/demoisa
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/coq
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/ccc
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral/acl2
-@dirrm %%EMACS_SITE_LISPDIR%%/ProofGeneral
-@dirrmtry %%EMACS_SITE_LISPDIR%%/site-start.d
 @dirrmtry share/applications
+@dirrmtry share/application-registry
+@dirrmtry share/pixmaps
+%%PORTDOCS%%@exec mkdir -p %D/%%DOCSDIR%%/plastic
+%%PORTDOCS%%@exec mkdir -p %D/%%DOCSDIR%%/lclam

--- proofgeneral.diff ends here ---
>Release-Note:
>Audit-Trail:
>Unformatted:



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?87lim1gx1k.wl>