diff -ruN /usr/ports/math/proofgeneral/Makefile /usr/ports/math/proofgeneral-new/Makefile
--- /usr/ports/math/proofgeneral/Makefile	Fri Oct 28 16:34:44 2005
+++ /usr/ports/math/proofgeneral-new/Makefile	Sun Mar 19 13:04:50 2006
@@ -6,13 +6,10 @@
 #
 
 PORTNAME=	proofgeneral
-PORTVERSION=	3.5
+PORTVERSION=	3.6
 CATEGORIES=	math elisp
-MASTER_SITES=	http://proofgeneral.inf.ed.ac.uk/releases/ \
-		http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/contrib/ \
-		http://isabelle.in.tum.de/dist/contrib/ \
-		http://mirror.cse.unsw.edu.au/pub/isabelle/contrib/
-DISTNAME=	ProofGeneral-3.5
+MASTER_SITES=	http://proofgeneral.inf.ed.ac.uk/releases/
+DISTNAME=	ProofGeneral-3.6pre051004
 
 MAINTAINER=	timbob@bigpond.com
 COMMENT=	A generic interface for proof assistants
@@ -70,16 +67,12 @@
 .endif
 
 post-patch:
-	@${TOUCH} -m -r ${WRKSRC}/generic/proof-menu.el.orig \
-	${WRKSRC}/generic/proof-menu.el
 	@${REINPLACE_CMD} -e 's,%%PREFIX%%,${PREFIX},' \
 		${WRKSRC}/etc/desktop/proofgeneral.desktop
+	${TOUCH} ${WRKSRC}/.byte-compile
 
 pre-build:
 .if defined(BYTE_COMPILE)
-	@${ECHO_CMD} "************************************************************"
-	@${ECHO_CMD} "* Byte compilation may not work properly for all files...  *"
-	@${ECHO_CMD} "************************************************************"
 	@${RM} ${WRKSRC}/.byte-compile
 .endif
 
diff -ruN /usr/ports/math/proofgeneral/distinfo /usr/ports/math/proofgeneral-new/distinfo
--- /usr/ports/math/proofgeneral/distinfo	Thu Feb  2 08:59:41 2006
+++ /usr/ports/math/proofgeneral-new/distinfo	Sun Mar 19 13:04:50 2006
@@ -1,3 +1,2 @@
-MD5 (ProofGeneral-3.5.tar.gz) = 2114f0ead1cb0b4c6be992aa7bf1529c
-SHA256 (ProofGeneral-3.5.tar.gz) = 6c044a44dc4457a0b6d7660afb9ae0a36240c22fc9f5475a90ff5bb685875a0b
-SIZE (ProofGeneral-3.5.tar.gz) = 1799956
+MD5 (ProofGeneral-3.6pre051004.tar.gz) = 84d7c8ee9db2e52d1891b66da1e74ef8
+SIZE (ProofGeneral-3.6pre051004.tar.gz) = 2243863
diff -ruN /usr/ports/math/proofgeneral/files/patch-Makefile /usr/ports/math/proofgeneral-new/files/patch-Makefile
--- /usr/ports/math/proofgeneral/files/patch-Makefile	Wed Aug 31 20:36:36 2005
+++ /usr/ports/math/proofgeneral-new/files/patch-Makefile	Sun Mar 19 13:04:50 2006
@@ -1,5 +1,5 @@
---- Makefile.orig	Sun Apr 18 01:23:53 2004
-+++ Makefile	Sat Aug 13 13:50:43 2005
+--- Makefile.orig	Thu Dec  8 07:07:44 2005
++++ Makefile	Thu Dec  8 07:36:00 2005
 @@ -15,7 +15,7 @@
  
  # Set this to "emacs" or "xemacs" according to your version of Emacs.
@@ -19,26 +19,17 @@
  
  PWD=$(shell pwd)
  
-@@ -65,7 +64,8 @@
+@@ -69,8 +68,7 @@
  ##	     compiles.
  ##
  compile: .byte-compile
 -	lastemacs=`cat .byte-compile`; if [ "$$lastemacs" != "$(EMACS)" ]; then rm -f .byte-compile; make .byte-compile; fi
+-
 +	lastemacs=`cat .byte-compile`; if [ "$$lastemacs" != "${EMACS_NAME}" ]; then rm -f .byte-compile; $(MAKE) .byte-compile; fi
-+	$(BYTECOMP) generic/proof-menu.el
- 
  
  .byte-compile: $(EL) x-symbol/lisp/*.el
-@@ -78,7 +78,7 @@
- 	rm -f $(BROKENELC)
- 	@echo " Byte compiling X-Symbol..."
- 	(cd x-symbol/lisp; rm -f *.elc; $(MAKE) EMACS="$(EMACS) -q -no-site-file")
--	echo $(EMACS) > $(@)
-+	echo ${EMACS_NAME} > $(@)
- 	@echo "*************************************************"
- 	@echo " Finished."
  	@echo "*************************************************"
-@@ -123,41 +123,36 @@
+@@ -127,41 +125,36 @@
  # 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.
@@ -56,11 +47,10 @@
  DEST_ELISP=${DEST_PREFIX}/${ELISPP}
  
  BINDIR=${PREFIX}/bin
--DESKTOP=${PREFIX}/share
+ DESKTOP=${PREFIX}/share
 -DOCDIR=${PREFIX}/share/doc/ProofGeneral
 -MANDIR=${PREFIX}/share/man/man1
 -INFODIR=${PREFIX}/share/info/
-+DESKTOP=${DESKTOP_PREFIX}/share
 +DOCDIR=${DOCSDIR}
 +MANDIR=${PREFIX}/man/man1
 +INFODIR=${PREFIX}/info/
@@ -69,33 +59,40 @@
 +install: install-desktop install-elisp install-bin install-init install-doc
  
  install-desktop:
- 	mkdir -p ${DESKTOP}/icons/hicolor/16x16
+-	mkdir -p ${DESKTOP}/icons/hicolor/16x16
 -	cp etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16
-+	${BSD_INSTALL_DATA} etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16
- 	mkdir -p ${DESKTOP}/icons/hicolor/32x32
+-	mkdir -p ${DESKTOP}/icons/hicolor/32x32
 -	cp etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32
-+	${BSD_INSTALL_DATA} etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32
- 	mkdir -p ${DESKTOP}/icons/hicolor/48x48
+-	mkdir -p ${DESKTOP}/icons/hicolor/48x48
 -	cp etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48
-+	${BSD_INSTALL_DATA} etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48
- 	mkdir -p ${DESKTOP}/pixmaps
+-	mkdir -p ${DESKTOP}/pixmaps
 -	cp etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/pixmaps
-+	${BSD_INSTALL_DATA} etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/pixmaps
- 	mkdir -p ${DESKTOP}/applications
+-	mkdir -p ${DESKTOP}/applications
 -	cp etc/desktop/proofgeneral.desktop ${DESKTOP}/applications
-+	${BSD_INSTALL_DATA} etc/desktop/proofgeneral.desktop ${DESKTOP}/applications
- 	mkdir -p ${DESKTOP}/mime-info
+-	mkdir -p ${DESKTOP}/mime-info
 -	cp etc/desktop/mime-info/proofgeneral.mime ${DESKTOP}/mime-info
 -	cp etc/desktop/mime-info/proofgeneral.keys ${DESKTOP}/mime-info
+-	mkdir -p ${DESKTOP}/application-registry
+-	cp etc/desktop/application-registry/proofgeneral.applications ${DESKTOP}/application-registry
++	mkdir -p ${DESKTOP}/icons/hicolor/16x16
++	${BSD_INSTALL_DATA} etc/desktop/icons/16x16/proofgeneral.png ${DESKTOP}/icons/hicolor/16x16
++	mkdir -p ${DESKTOP}/icons/hicolor/32x32
++	${BSD_INSTALL_DATA} etc/desktop/icons/32x32/proofgeneral.png ${DESKTOP}/icons/hicolor/32x32
++	mkdir -p ${DESKTOP}/icons/hicolor/48x48
++	${BSD_INSTALL_DATA} etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/icons/hicolor/48x48
++	mkdir -p ${DESKTOP}/pixmaps
++	${BSD_INSTALL_DATA} etc/desktop/icons/48x48/proofgeneral.png ${DESKTOP}/pixmaps
++	mkdir -p ${DESKTOP}/applications
++	${BSD_INSTALL_DATA} etc/desktop/proofgeneral.desktop ${DESKTOP}/applications
++	mkdir -p ${DESKTOP}/mime-info
 +	${BSD_INSTALL_DATA} etc/desktop/mime-info/proofgeneral.mime ${DESKTOP}/mime-info
 +	${BSD_INSTALL_DATA} etc/desktop/mime-info/proofgeneral.keys ${DESKTOP}/mime-info
- 	mkdir -p ${DESKTOP}/application-registry
--	cp etc/desktop/application-registry/proofgeneral.applications ${DESKTOP}/application-registry
++	mkdir -p ${DESKTOP}/application-registry
 +	${BSD_INSTALL_DATA} etc/desktop/application-registry/proofgeneral.applications ${DESKTOP}/application-registry
  
  # NB: .el files are not strictly necessary, but we package/install them
  # for the time being to help with debugging, or for users to recompile.
-@@ -172,14 +167,30 @@
+@@ -176,14 +169,30 @@
  install-el:
  	mkdir -p ${ELISP}
  	for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done
@@ -130,7 +127,7 @@
  
  install-init:
  	mkdir -p ${ELISP_START}
-@@ -189,18 +200,16 @@
+@@ -193,18 +202,16 @@
  
  install-bin: scripts
  	mkdir -p ${BINDIR}
@@ -154,16 +151,16 @@
  
  ##
  ## scripts: try to patch bash and perl scripts with correct paths
-@@ -243,7 +252,7 @@
+@@ -247,7 +254,7 @@
  
  # Set PGHOME path in scripts back to default location.
  cleanpgscripts:
 -	make pgscripts DEST_ELISP='$$$$HOME/ProofGeneral'
-+    $(MAKE) pgscripts DEST_ELISP='$$$$HOME/ProofGeneral'
++	$(MAKE) pgscripts DEST_ELISP='$$$$HOME/ProofGeneral'
  
  
  ##
-@@ -253,11 +262,11 @@
+@@ -257,11 +264,11 @@
  ##
  
  devel.%:
diff -ruN /usr/ports/math/proofgeneral/files/patch-doc-Makefile /usr/ports/math/proofgeneral-new/files/patch-doc-Makefile
--- /usr/ports/math/proofgeneral/files/patch-doc-Makefile	Wed Aug 31 20:36:36 2005
+++ /usr/ports/math/proofgeneral-new/files/patch-doc-Makefile	Thu Jan  1 10:00:00 1970
@@ -1,13 +0,0 @@
---- doc/Makefile.orig	Tue Jun  7 17:42:22 2005
-+++ doc/Makefile	Tue Jun  7 17:42:47 2005
-@@ -19,8 +19,8 @@
- 	$(MAKE) doc
- 
- %:
--	make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" $@
--	make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" $@ 
-+	$(MAKE) -f Makefile.doc DOCNAME=PG-adapting MAKE="$(MAKE) -f Makefile.doc" $@
-+	$(MAKE) -f Makefile.doc DOCNAME=ProofGeneral MAKE="$(MAKE) -f Makefile.doc" $@ 
- 
- ##
- ## man page for proofgeneral script
diff -ruN /usr/ports/math/proofgeneral/files/patch-doc-Makefile.doc /usr/ports/math/proofgeneral-new/files/patch-doc-Makefile.doc
--- /usr/ports/math/proofgeneral/files/patch-doc-Makefile.doc	Wed Aug 31 20:36:36 2005
+++ /usr/ports/math/proofgeneral-new/files/patch-doc-Makefile.doc	Sun Mar 19 13:04:50 2006
@@ -1,17 +1,17 @@
---- doc/Makefile.doc.orig	Sun Apr 18 09:39:58 2004
-+++ doc/Makefile.doc	Fri Jul 22 22:10:05 2005
-@@ -152,10 +152,10 @@
+--- doc/Makefile.doc.orig	Thu Dec  8 07:39:33 2005
++++ doc/Makefile.doc	Thu Dec  8 07:39:46 2005
+@@ -153,10 +153,10 @@
  ## texi: update magic comments in texi from docstrings in code.
  ##	  (developer use only!)
  ##
 -$(DOCNAME).texi: ../*/*.el 
 -	$(MAKE) magic
 -magic:
--	$(EMACS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
+-	$(EMACS) $(EMACSFLAGS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
 +#$(DOCNAME).texi: ../*/*.el 
 +#	$(MAKE) magic
 +#magic:
-+#	$(EMACS) -batch -l ../generic/texi-docstring-magic.el -l ../generic/proof-site.el -l ../generic/pg-user.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
++#	$(EMACS) $(EMACSFLAGS) -l docstring-magic.el $(DOCNAME).texi -f texi-docstring-magic -f save-buffer
  
  
  
diff -ruN /usr/ports/math/proofgeneral/files/patch-etc_desktop_proofgeneral.desktop /usr/ports/math/proofgeneral-new/files/patch-etc_desktop_proofgeneral.desktop
--- /usr/ports/math/proofgeneral/files/patch-etc_desktop_proofgeneral.desktop	Wed Aug 31 20:36:36 2005
+++ /usr/ports/math/proofgeneral-new/files/patch-etc_desktop_proofgeneral.desktop	Sun Mar 19 13:04:50 2006
@@ -1,11 +1,11 @@
---- etc/desktop/proofgeneral.desktop.orig	Sat Aug 13 14:19:29 2005
-+++ etc/desktop/proofgeneral.desktop	Sat Aug 13 14:19:46 2005
-@@ -2,7 +2,7 @@
+--- etc/desktop/proofgeneral.desktop.orig	Thu Dec  8 07:40:38 2005
++++ etc/desktop/proofgeneral.desktop	Thu Dec  8 07:41:03 2005
+@@ -5,7 +5,7 @@
  Name=Proof General
- Comment=Organise Your Proofs!
- Exec=proofgeneral %F
+ GenericName=Theorem proving environment
+ Comment=Organise your proofs!
 -Icon=proofgeneral.png
 +Icon=%%PREFIX%%/share/pixmaps/proofgeneral.png
- Terminal=false
- Type=Application
- Encoding=UTF-8
+ FilePattern=proofgeneral
+ TryExec=proofgeneral
+ Exec=proofgeneral %F
diff -ruN /usr/ports/math/proofgeneral/files/patch-generic-proof-menu.el /usr/ports/math/proofgeneral-new/files/patch-generic-proof-menu.el
--- /usr/ports/math/proofgeneral/files/patch-generic-proof-menu.el	Wed Aug 31 20:36:36 2005
+++ /usr/ports/math/proofgeneral-new/files/patch-generic-proof-menu.el	Thu Jan  1 10:00:00 1970
@@ -1,15 +0,0 @@
---- generic/proof-menu.el.orig	Fri Jul 22 17:46:09 2005
-+++ generic/proof-menu.el	Fri Jul 22 17:46:09 2005
-@@ -176,10 +176,10 @@
- 	     (cons "Help"
- 		   (append
- 		    `([,(concat proof-assistant " information")
--		       '(proof-help)
-+		        (proof-help)
- 		       ,menuvisiblep proof-info-command]
- 		      [,(concat proof-assistant " web page")
--		       '(browse-url proof-assistant-home-page)
-+		        (browse-url proof-assistant-home-page)
- 		       ,menuvisiblep proof-assistant-home-page])
- 		    (proof-ass help-menu-entries))))))))
- 
diff -ruN /usr/ports/math/proofgeneral/files/patch-isa_isabelle-system.el /usr/ports/math/proofgeneral-new/files/patch-isa_isabelle-system.el
--- /usr/ports/math/proofgeneral/files/patch-isa_isabelle-system.el	Thu Sep 15 10:47:17 2005
+++ /usr/ports/math/proofgeneral-new/files/patch-isa_isabelle-system.el	Sun Mar 19 13:04:50 2006
@@ -1,6 +1,6 @@
---- isa/isabelle-system.el.orig	Thu Sep  8 12:43:45 2005
-+++ isa/isabelle-system.el	Thu Sep  8 12:45:12 2005
-@@ -73,10 +73,6 @@
+--- isa/isabelle-system.el.orig	Thu Dec  8 07:43:17 2005
++++ isa/isabelle-system.el	Thu Dec  8 07:43:38 2005
+@@ -74,10 +74,6 @@
  with full path."
    (interactive)
    (unless (or isatool-not-found (file-executable-p isa-isatool-command))
diff -ruN /usr/ports/math/proofgeneral/pkg-plist /usr/ports/math/proofgeneral-new/pkg-plist
--- /usr/ports/math/proofgeneral/pkg-plist	Thu Feb  2 08:59:41 2006
+++ /usr/ports/math/proofgeneral-new/pkg-plist	Sun Mar 19 13:04:50 2006
@@ -1,12 +1,15 @@
+bin/coqtags
+bin/interface
+bin/legotags
 bin/proofgeneral
 %%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/coq/coq-abbrev-V7.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/coq/coq-abbrev-V7.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-indent.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/coq/coq-indent.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/coq/coq-syntax.el
@@ -20,15 +23,21 @@
 %%EMACS_SITE_LISPDIR%%/proofgeneral/demoisa/demoisa.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/demoisa/demoisa.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/generic/_pkg.elc
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/holes.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/holes.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-goals.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-goals.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-metadata.elc
+%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-pbrpm.el
+%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-pbrpm.elc
+%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-pgip-old.el
+%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-pgip-old.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-pgip.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-pgip.elc
+%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-resolve.el
+%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/pg-resolve.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
@@ -41,8 +50,6 @@
 %%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-compat.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/proof-compat.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
@@ -75,14 +82,6 @@
 %%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/generic/span-extent.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/span-extent.elc
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/span-overlay.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/span-overlay.elc
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/span.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/span.elc
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/texi-docstring-magic.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/generic/texi-docstring-magic.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/hol98/hol98.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/hol98/hol98.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/hol98/x-symbol-hol98.el
@@ -142,6 +141,8 @@
 %%EMACS_SITE_LISPDIR%%/proofgeneral/isa/x-symbol-isa.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/isa/x-symbol-isabelle.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/isa/x-symbol-isabelle.elc
+%%EMACS_SITE_LISPDIR%%/proofgeneral/isar/isar-autotest.el
+%%EMACS_SITE_LISPDIR%%/proofgeneral/isar/isar-autotest.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
@@ -160,6 +161,22 @@
 %%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/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/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/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/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
@@ -190,10 +207,12 @@
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-font.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-fun.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-fun.elc
+%%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-lang.el
+%%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-lang.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-outline.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-outline.elc
-%%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-sym-lock.el
-%%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-sym-lock.elc
+%%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-pbrpm.el
+%%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-pbrpm.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-tags.el
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox-tags.elc
 %%EMACS_SITE_LISPDIR%%/proofgeneral/phox/phox.el
@@ -215,6 +234,8 @@
 %%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
@@ -231,8 +252,12 @@
 %%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
@@ -249,6 +274,10 @@
 %%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
@@ -257,13 +286,23 @@
 %%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
@@ -287,6 +326,10 @@
 %%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
@@ -300,12 +343,24 @@
 %%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/info/x-symbol.info
@@ -352,12 +407,14 @@
 @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
+@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/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
@@ -369,7 +426,7 @@
 @dirrm %%EMACS_SITE_LISPDIR%%/proofgeneral/coq
 @dirrm %%EMACS_SITE_LISPDIR%%/proofgeneral/acl2
 @dirrm %%EMACS_SITE_LISPDIR%%/proofgeneral
-@dirrmtry %%EMACS_SITE_LISPDIR%%/site-start.d
+@unexec rmdir %D/%%EMACS_SITE_LISPDIR%%/site-start.d 2>/dev/null || true
 share/application-registry/proofgeneral.applications
 share/applications/proofgeneral.desktop
 share/icons/hicolor/16x16/proofgeneral.png