12 files changed, 421 insertions, 146 deletions

diff --git a/lang/twelf/Makefile b/lang/twelf/Makefile
index 97ec56aed0bc..d1999c52b042 100644
--- a/lang/twelf/Makefile
+++ b/lang/twelf/Makefile
@@ -6,21 +6,37 @@
 #
 
 PORTNAME=	twelf
-PORTVERSION=	1.4
+PORTVERSION=	1.5R1
 CATEGORIES=	lang
 MASTER_SITES=	http://www-2.cs.cmu.edu/~twelf/dist/ http://www.cs.cmu.edu/~twelf/dist/
-DISTNAME=	twelf-1-4
+DISTNAME=	twelf-1-5R1
 
 MAINTAINER=	andrewb@cs.cmu.edu
 COMMENT=	A meta-logical framework for deductive systems
 
+.if defined(WITH_MLTON)
+RUN_DEPENDS=	mlton:${PORTSDIR}/lang/mlton
+BUILD_DEPENDS=	mlton:${PORTSDIR}/lang/mlton
+.elif defined(WITH_SML_NJ_DEVEL)
+RUN_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj-devel
+BUILD_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj-devel
+.else
 RUN_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj
 BUILD_DEPENDS=	sml:${PORTSDIR}/lang/sml-nj
+.endif
+
+BUILD_DEPENDS+=	tex:${PORTSDIR}/print/teTeX
+
+.if defined(WITH_MLTON)
+MAKEFILE=	mlton/Makefile
+.elif defined(WITH_SML_NJ_DEVEL)
+MAKEFILE=	smlnj/Makefile
+.endif
 
 WRKSRC=		${WRKDIR}/twelf
 INFO=		twelf
 
-RESTRICTED=	"License is currently indeterminate (expected to be GPL)"
+RESTRICTED=	License is currently indeterminate (expected to be GPL)
 
 post-patch:
 	@${REINPLACE_CMD} -e "s|%%PREFIX%%|${PREFIX}|g" ${WRKSRC}/Makefile
diff --git a/lang/twelf/distinfo b/lang/twelf/distinfo
index cdd43f68d813..d0d0200a4045 100644
--- a/lang/twelf/distinfo
+++ b/lang/twelf/distinfo
@@ -1,3 +1,3 @@
-MD5 (twelf-1-4.tar.gz) = ba4d2a374242dae6e3c0dada30adeae2
-SHA256 (twelf-1-4.tar.gz) = 63d0a283f75201467b10d541d643eba82f0e52b0ee4ea88a391c574a314ad62a
-SIZE (twelf-1-4.tar.gz) = 1463158
+MD5 (twelf-1-5R1.tar.gz) = 05b5c65f297c1f4ee07641682121ebbc
+SHA256 (twelf-1-5R1.tar.gz) = d20473493cd39e111ce3585f8c32eefc79de4099ae4e97bfe2eb7695d6987564
+SIZE (twelf-1-5R1.tar.gz) = 1157430
diff --git a/lang/twelf/files/patch-FreeBSD.mk b/lang/twelf/files/patch-FreeBSD.mk
new file mode 100644
index 000000000000..1522b132bed8
--- /dev/null
+++ b/lang/twelf/files/patch-FreeBSD.mk
@@ -0,0 +1,170 @@
+--- FreeBSD.mk.orig	2009-02-12 21:33:04.000000000 -0500
++++ FreeBSD.mk	2009-02-12 21:48:54.000000000 -0500
+@@ -0,0 +1,82 @@
++# ---------------------------------------------------------------
++# Executables
++# ---------------------------------------------------------------
++
++arch != uname -p
++
++.if ${arch} == "i386"
++smlarch = x86
++.else
++smlarch = ${arch}
++.endif
++
++prefix        = ${PREFIX}
++bindir        = ${prefix}/bin
++infodir       = ${prefix}/info
++twelfexecdir  = ${prefix}/libexec/twelf
++twelfsharedir = ${prefix}/share/twelf
++
++runfile  = bin/twelf-server
++heapfile = bin/.heap/twelf-server.${smlarch}-bsd
++
++# ---------------------------------------------------------------
++# Documentation
++# ---------------------------------------------------------------
++
++htmlnodes = toc abt 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
++
++dvifile = doc/dvi/twelf.dvi
++htmlfiles := doc/html/index.html ${htmlnodes:%=doc/html/twelf_%.html}
++infofile = doc/info/twelf.info
++pdffile = doc/pdf/twelf.pdf
++psfile = doc/ps/twelf.ps
++
++docfiles = ${dvifile} ${htmlfiles} ${infofile} ${pdffile} ${psfile}
++
++.for file in ${docfiles}
++${file}:
++	(cd doc/guide; make; make install)
++.endfor
++
++all: ${runfile} ${heapfile} ${docfiles}
++
++# ---------------------------------------------------------------
++# Installation
++# ---------------------------------------------------------------
++
++sharefiles != (echo README HISTORY;                            \
++               echo ${docfiles};                               \
++               find emacs        -type f -not -path '*/CVS/*'; \
++               find examples     -type f -not -path '*/CVS/*'; \
++               find examples-clp -type f -not -path '*/CVS/*'; \
++               find exercises    -type f -not -path '*/CVS/*'; \
++               find tex          -type f -not -path '*/CVS/*'; \
++               find vim          -type f -not -path '*/CVS/*' )
++
++installfiles := ${bindir}/twelf-server             \
++                ${twelfsharedir}/${runfile}        \
++                ${twelfexecdir}/${heapfile}        \
++                ${infodir}/twelf.info              \
++                ${sharefiles:%=$(twelfsharedir)/%}
++
++${bindir}/twelf-server: ${twelfsharedir}/${runfile}
++	ln -s $? $@
++
++${twelfsharedir}/${runfile}: ${runfile}
++	@install -d -o root -g wheel -m 0755 ${@D}
++	install -o root -g wheel -m 0555 $? $@
++
++${twelfexecdir}/${heapfile}: ${heapfile}
++	@install -d -o root -g wheel -m 0755 ${@D}
++	install -o root -g wheel -m 0444 $? $@
++
++${infodir}/twelf.info: doc/info/twelf.info
++	install -o root -g wheel -m 0444 $? $@
++
++.for file in ${sharefiles}
++${twelfsharedir}/${file}: ${file}
++	@install -d -o root -g wheel -m 0755 ${@D}
++	install -o root -g wheel -m 0644 $? $@
++.endfor
++
++install: ${installfiles}
+--- FreeBSD.mk.orig	2009-02-12 21:33:04.000000000 -0500
++++ FreeBSD.mk	2009-02-12 21:48:54.000000000 -0500
+@@ -0,0 +1,82 @@
++# ---------------------------------------------------------------
++# Executables
++# ---------------------------------------------------------------
++
++arch != uname -p
++
++.if ${arch} == "i386"
++smlarch = x86
++.else
++smlarch = ${arch}
++.endif
++
++prefix        = ${PREFIX}
++bindir        = ${prefix}/bin
++infodir       = ${prefix}/info
++twelfexecdir  = ${prefix}/libexec/twelf
++twelfsharedir = ${prefix}/share/twelf
++
++runfile  = bin/twelf-server
++heapfile = bin/.heap/twelf-server.${smlarch}-bsd
++
++# ---------------------------------------------------------------
++# Documentation
++# ---------------------------------------------------------------
++
++htmlnodes = toc abt 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
++
++dvifile = doc/dvi/twelf.dvi
++htmlfiles := doc/html/index.html ${htmlnodes:%=doc/html/twelf_%.html}
++infofile = doc/info/twelf.info
++pdffile = doc/pdf/twelf.pdf
++psfile = doc/ps/twelf.ps
++
++docfiles = ${dvifile} ${htmlfiles} ${infofile} ${pdffile} ${psfile}
++
++.for file in ${docfiles}
++${file}:
++	(cd doc/guide; make; make install)
++.endfor
++
++all: ${runfile} ${heapfile} ${docfiles}
++
++# ---------------------------------------------------------------
++# Installation
++# ---------------------------------------------------------------
++
++sharefiles != (echo README HISTORY;                            \
++               echo ${docfiles};                               \
++               find emacs        -type f -not -path '*/CVS/*'; \
++               find examples     -type f -not -path '*/CVS/*'; \
++               find examples-clp -type f -not -path '*/CVS/*'; \
++               find exercises    -type f -not -path '*/CVS/*'; \
++               find tex          -type f -not -path '*/CVS/*'; \
++               find vim          -type f -not -path '*/CVS/*' )
++
++installfiles := ${bindir}/twelf-server             \
++                ${twelfsharedir}/${runfile}        \
++                ${twelfexecdir}/${heapfile}        \
++                ${infodir}/twelf.info              \
++                ${sharefiles:%=$(twelfsharedir)/%}
++
++${bindir}/twelf-server: ${twelfsharedir}/${runfile}
++	ln -s $? $@
++
++${twelfsharedir}/${runfile}: ${runfile}
++	@install -d -o root -g wheel -m 0755 ${@D}
++	install -o root -g wheel -m 0555 $? $@
++
++${twelfexecdir}/${heapfile}: ${heapfile}
++	@install -d -o root -g wheel -m 0755 ${@D}
++	install -o root -g wheel -m 0444 $? $@
++
++${infodir}/twelf.info: doc/info/twelf.info
++	install -o root -g wheel -m 0444 $? $@
++
++.for file in ${sharefiles}
++${twelfsharedir}/${file}: ${file}
++	@install -d -o root -g wheel -m 0755 ${@D}
++	install -o root -g wheel -m 0644 $? $@
++.endfor
++
++install: ${installfiles}
diff --git a/lang/twelf/files/patch-Makefile b/lang/twelf/files/patch-Makefile
index 09d18c15fcff..992543b181ec 100644
--- a/lang/twelf/files/patch-Makefile
+++ b/lang/twelf/files/patch-Makefile
@@ -1,85 +1,26 @@
---- Makefile.orig	Sun Dec 22 11:29:46 2002
-+++ Makefile	Sat Jul  9 18:52:09 2005
-@@ -31,7 +31,7 @@
+--- Makefile.orig	2005-03-08 15:49:53.000000000 -0500
++++ Makefile	2009-02-12 22:07:33.000000000 -0500
+@@ -32,16 +32,20 @@
+ version = "1.5"
+ delphinversion = "0.1"
  
++.include "FreeBSD.mk"
++
  default : twelf-server twelf-emacs
  
 -all : twelf-server twelf-sml twelf-emacs
-+# all : twelf-server twelf-sml twelf-emacs
++#all : twelf-server twelf-sml twelf-emacs
  
- twelf-server: ; 
+-twelf-server: ; 
++${runfile}: ;
  	@echo "*************************************************"
-@@ -62,3 +62,73 @@
- 
- clean: ;
- 	rm -rf $(twelfdir)/src/*/CM ;
-+
-+# ---------------------------------------------------------------
-+# Installation
-+# ---------------------------------------------------------------
-+
-+arch != uname -p
-+
-+.if ${arch} == "i386"
-+smlarch = x86
-+.else
-+smlarch = ${arch}
-+.endif
-+
-+prefix        = %%PREFIX%%
-+bindir        = ${prefix}/bin
-+infodir       = ${prefix}/info
-+twelfexecdir  = ${prefix}/libexec/twelf
-+twelfsharedir = ${prefix}/share/twelf
-+
-+runfile  = bin/twelf-server
-+heapfile = bin/.heap/twelf-server.${smlarch}-bsd
-+
-+infofiles  != (cd doc/info; find . -type f -not -name '*.orig')
-+sharefiles != (find README       -type f;                     \
-+               find doc          -type f -not -name '*.orig'; \
-+               find emacs        -type f;                     \
-+               find examples     -type f;                     \
-+               find examples-clp -type f;                     \
-+               find tex          -type f)
-+
-+installfiles := ${bindir}/twelf-server             \
-+                ${twelfsharedir}/${runfile}        \
-+                ${twelfexecdir}/${heapfile}        \
-+                ${infofiles:%=$(infodir)/%}        \
-+                ${sharefiles:%=$(twelfsharedir)/%}
-+
-+all: ${runfile} ${heapfile}
-+
-+${runfile}:
-+	echo "#!/bin/sh" >$@
-+	echo "exec ${sml} @SMLload=${twelfexecdir}/${heapfile} @SMLdebug=/dev/null" >>$@
-+
-+${heapfile}:
-+	$(sml) < twelf-server.sml
-+
-+${bindir}/twelf-server: ${twelfsharedir}/${runfile}
-+	ln -s $? $@
-+
-+${twelfsharedir}/${runfile}: ${runfile}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0555 $? $@
-+
-+${twelfexecdir}/${heapfile}: ${heapfile}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0444 $? $@
-+
-+.for file in ${infofiles}
-+${infodir}/${file}: doc/info/${file}
-+	ln -s ${twelfsharedir}/$? $@
-+.endfor
-+
-+.for file in ${sharefiles}
-+${twelfsharedir}/${file}: ${file}
-+	@install -d -o root -g wheel -m 0755 ${@D}
-+	install -o root -g wheel -m 0644 $? $@
-+.endfor
-+
-+install: ${installfiles}
-+	install-info ${infodir}/twelf.info ${infodir}/dir
+ 	@echo "Twelf $(version): Server"
+ 	@echo "*************************************************"	 
+ 	$(sml) < twelf-server.sml ;
+-	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" ;
++	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" "$(twelfexecdir)" ;
 +
++${heapfile}: ${runfile}
+ 
+ twelf-sml: ; 
+ 	@echo "*************************************************"
diff --git a/lang/twelf/files/patch-bin-mkexec b/lang/twelf/files/patch-bin-mkexec
new file mode 100644
index 000000000000..216c90f8d557
--- /dev/null
+++ b/lang/twelf/files/patch-bin-mkexec
@@ -0,0 +1,13 @@
+--- bin/.mkexec.orig	2003-01-21 01:03:32.000000000 -0500
++++ bin/.mkexec	2009-02-12 21:24:27.000000000 -0500
+@@ -7,8 +7,9 @@
+ # $2 = Twelf root directory
+ # $3 = Type of executable (e.g. twelf-server, twelf-sml)
+ # $4 = Name of executable (e.g. twelf-server, twelf-sml)
++# $5 = Twelf installation directory (e.g. /usr/local/libexec/twelf)
+ cat > "$2/bin/$4" <<EOF
+ #! /bin/sh
+-exec "$1" @SMLload="$2/bin/.heap/$3" @SMLdebug=/dev/null
++exec "$1" @SMLload="$5/bin/.heap/$3" @SMLdebug=/dev/null
+ EOF
+ chmod a+x "$2/bin/$4"
diff --git a/lang/twelf/files/patch-doc-guide-Makefile b/lang/twelf/files/patch-doc-guide-Makefile
new file mode 100644
index 000000000000..74b33913e7e4
--- /dev/null
+++ b/lang/twelf/files/patch-doc-guide-Makefile
@@ -0,0 +1,11 @@
+--- doc/guide/Makefile.orig	2009-02-08 13:47:36.000000000 -0500
++++ doc/guide/Makefile	2009-02-08 13:23:38.000000000 -0500
+@@ -39,7 +39,7 @@
+ twelf_toc.html : twelf.texi;
+ 	@echo "---------- Creating HTML: twelf_*.html"
+ 	$(texi2html) -menu -number -split_chapter twelf.texi;
+-	$(texi2html) -check *.html;
++#	$(texi2html) -check *.html;
+ 
+ twelf.pdf : twelf.texi;
+ 	@echo "---------- Creating unindexed PDF: twelf.pdf"
diff --git a/lang/twelf/files/patch-doc-guide-twelf.texi b/lang/twelf/files/patch-doc-guide-twelf.texi
new file mode 100644
index 000000000000..0d1ded32f9ba
--- /dev/null
+++ b/lang/twelf/files/patch-doc-guide-twelf.texi
@@ -0,0 +1,14 @@
+--- doc/guide/twelf.texi.orig	2009-02-08 18:21:50.000000000 -0500
++++ doc/guide/twelf.texi	2009-02-08 18:23:11.000000000 -0500
+@@ -12,6 +12,11 @@
+ @syncodeindex fn cp
+ @c %**end of header
+ 
++@dircategory Programming
++@direntry
++* Twelf User Guide: (twelf).   The Twelf User's Guide.
++@end direntry
++
+ @titlepage
+ @title Twelf User's Guide
+ @subtitle Version @value{VERSION}
diff --git a/lang/twelf/files/patch-mlton-Makefile b/lang/twelf/files/patch-mlton-Makefile
new file mode 100644
index 000000000000..9b13fcb758f2
--- /dev/null
+++ b/lang/twelf/files/patch-mlton-Makefile
@@ -0,0 +1,30 @@
+--- mlton/Makefile.orig	2004-11-12 14:10:27.000000000 -0500
++++ mlton/Makefile	2009-02-12 22:40:25.000000000 -0500
+@@ -28,11 +28,13 @@
+ version = "1.5"
+ delphinversion = "0.1"
+ 
++.include "FreeBSD.mk"
++
+ default : twelf-server twelf-emacs
+ 
+-all : twelf-server twelf-emacs
++#all : twelf-server twelf-emacs
+ 
+-twelf-server: ; 
++${runfile}: ; 
+ 	@echo "*************************************************"
+ 	@echo "Twelf $(version): Server"
+ 	@echo "*************************************************"
+@@ -47,7 +49,10 @@
+ 		cmfileid="-97";						\
+ 	fi;								\
+ 	$(sml) mlton/twelf-server$${cmfileid}.cm ;			\
+-	mv mlton/twelf-server$${cmfileid} bin/$(twelfserver)
++	mv mlton/twelf-server$${cmfileid} ${runfile}
++
++${heapfile}:
++	touch ${heapfile}
+ 
+ twelf-sml: ; 
+ 	@echo "*************************************************"
diff --git a/lang/twelf/files/patch-smlnj-Makefile b/lang/twelf/files/patch-smlnj-Makefile
new file mode 100644
index 000000000000..739869e21e6f
--- /dev/null
+++ b/lang/twelf/files/patch-smlnj-Makefile
@@ -0,0 +1,26 @@
+--- smlnj/Makefile.orig	2003-10-17 23:35:23.000000000 -0400
++++ smlnj/Makefile	2009-02-12 22:22:57.000000000 -0500
+@@ -32,16 +32,20 @@
+ version = "1.5"
+ delphinversion = "0.1"
+ 
++.include "FreeBSD.mk"
++
+ default : twelf-server twelf-emacs
+ 
+-all : twelf-server twelf-sml twelf-emacs
++#all : twelf-server twelf-sml twelf-emacs
+ 
+-twelf-server: ; 
++${runfile}: ; 
+ 	@echo "*************************************************"
+ 	@echo "Twelf $(version): Server"
+ 	@echo "*************************************************"	 
+ 	$(sml) < smlnj/twelf-server.sml ;
+-	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" ;
++	bin/.mkexec "$(sml)" "$(twelfdir)" twelf-server "$(twelfserver)" "$(twelfexecdir)" ;
++
++${heapfile}: ${runfile}
+ 
+ twelf-sml: ; 
+ 	@echo "*************************************************"
diff --git a/lang/twelf/files/patch-twelf.info b/lang/twelf/files/patch-twelf.info
deleted file mode 100644
index a74c22a58fce..000000000000
--- a/lang/twelf/files/patch-twelf.info
+++ /dev/null
@@ -1,13 +0,0 @@
---- doc/info/twelf.info.orig	Sat Jul  9 16:05:36 2005
-+++ doc/info/twelf.info	Sat Jul  9 15:52:24 2005
-@@ -1,5 +1,10 @@
- This is twelf.info, produced by makeinfo version 4.2 from twelf.texi.
- 
-+INFO-DIR-SECTION Programming
-+START-INFO-DIR-ENTRY
-+* Twelf User Guide: (twelf).   The Twelf User's Guide.
-+END-INFO-DIR-ENTRY
-+
- 
- Indirect:
- twelf.info-1: 71
diff --git a/lang/twelf/pkg-descr b/lang/twelf/pkg-descr
index f32f99997930..433a4a2c6183 100644
--- a/lang/twelf/pkg-descr
+++ b/lang/twelf/pkg-descr
@@ -1,4 +1,3 @@
-
 The Twelf implementation comprises
 
  * the LF logical framework, including type reconstruction;
@@ -17,3 +16,4 @@ and Hilbert's deduction theorem.
 -- the Twelf home page
 
 WWW: http://www.cs.cmu.edu/~twelf
+Maintainer: Andrew Bernard (andrewb@cs.cmu.edu)
diff --git a/lang/twelf/pkg-plist b/lang/twelf/pkg-plist
index f8d81053e035..62958d4c8ac3 100644
--- a/lang/twelf/pkg-plist
+++ b/lang/twelf/pkg-plist
@@ -1,18 +1,13 @@
 bin/twelf-server
 libexec/twelf/bin/.heap/twelf-server.x86-bsd
-share/twelf/README
 share/twelf/bin/twelf-server
+share/twelf/README
+share/twelf/HISTORY
 share/twelf/doc/dvi/twelf.dvi
 share/twelf/doc/html/index.html
+share/twelf/doc/html/twelf_toc.html
+share/twelf/doc/html/twelf_abt.html
 share/twelf/doc/html/twelf_1.html
-share/twelf/doc/html/twelf_10.html
-share/twelf/doc/html/twelf_11.html
-share/twelf/doc/html/twelf_12.html
-share/twelf/doc/html/twelf_13.html
-share/twelf/doc/html/twelf_14.html
-share/twelf/doc/html/twelf_15.html
-share/twelf/doc/html/twelf_16.html
-share/twelf/doc/html/twelf_17.html
 share/twelf/doc/html/twelf_2.html
 share/twelf/doc/html/twelf_3.html
 share/twelf/doc/html/twelf_4.html
@@ -21,29 +16,35 @@ share/twelf/doc/html/twelf_6.html
 share/twelf/doc/html/twelf_7.html
 share/twelf/doc/html/twelf_8.html
 share/twelf/doc/html/twelf_9.html
-share/twelf/doc/html/twelf_toc.html
+share/twelf/doc/html/twelf_10.html
+share/twelf/doc/html/twelf_11.html
+share/twelf/doc/html/twelf_12.html
+share/twelf/doc/html/twelf_13.html
+share/twelf/doc/html/twelf_14.html
+share/twelf/doc/html/twelf_15.html
+share/twelf/doc/html/twelf_16.html
+share/twelf/doc/html/twelf_17.html
+share/twelf/doc/html/twelf_18.html
+share/twelf/doc/html/twelf_19.html
+share/twelf/doc/html/twelf_20.html
 share/twelf/doc/info/twelf.info
-share/twelf/doc/info/twelf.info-1
-share/twelf/doc/info/twelf.info-2
-share/twelf/doc/info/twelf.info-3
-share/twelf/doc/info/twelf.info-4
-share/twelf/doc/info/twelf.info-5
 share/twelf/doc/pdf/twelf.pdf
 share/twelf/doc/ps/twelf.ps
+share/twelf/emacs/.cvsignore
 share/twelf/emacs/README
 share/twelf/emacs/auc-menu.el
 share/twelf/emacs/twelf-font.el
 share/twelf/emacs/twelf-hilit.el
 share/twelf/emacs/twelf-init.el
 share/twelf/emacs/twelf.el
-share/twelf/examples/README
-share/twelf/examples/arith/README
 share/twelf/examples/arith/arith.elf
+share/twelf/examples/arith/README
 share/twelf/examples/arith/arith.thm
 share/twelf/examples/arith/sources.cfg
 share/twelf/examples/arith/test.cfg
-share/twelf/examples/ccc/README
+share/twelf/examples/README
 share/twelf/examples/ccc/abs-env.elf
+share/twelf/examples/ccc/README
 share/twelf/examples/ccc/catlem.elf
 share/twelf/examples/ccc/ccc.elf
 share/twelf/examples/ccc/conc.elf
@@ -63,10 +64,10 @@ share/twelf/examples/ccc/spass.elf
 share/twelf/examples/ccc/spass.sml
 share/twelf/examples/ccc/subext.elf
 share/twelf/examples/ccc/test.cfg
+share/twelf/examples/church-rosser/equiv.elf
 share/twelf/examples/church-rosser/README
-share/twelf/examples/church-rosser/church-rosser.thm
 share/twelf/examples/church-rosser/cr.thm
-share/twelf/examples/church-rosser/equiv.elf
+share/twelf/examples/church-rosser/church-rosser.thm
 share/twelf/examples/church-rosser/examples.quy
 share/twelf/examples/church-rosser/lam.elf
 share/twelf/examples/church-rosser/ord-cr.elf
@@ -79,7 +80,6 @@ share/twelf/examples/church-rosser/sources.cfg
 share/twelf/examples/church-rosser/test-unsafe.cfg
 share/twelf/examples/church-rosser/test.cfg
 share/twelf/examples/church-rosser/test.tag
-share/twelf/examples/compile/README
 share/twelf/examples/compile/cls/cls-complete.elf
 share/twelf/examples/compile/cls/cls-sound.elf
 share/twelf/examples/compile/cls/cls.elf
@@ -93,6 +93,7 @@ share/twelf/examples/compile/cls/sources.cfg
 share/twelf/examples/compile/cls/test.cfg
 share/twelf/examples/compile/cls/trans.elf
 share/twelf/examples/compile/cls/trans2.elf
+share/twelf/examples/compile/README
 share/twelf/examples/compile/cpm/ceval-complete.elf
 share/twelf/examples/compile/cpm/ceval-complete.thm
 share/twelf/examples/compile/cpm/ceval-sound.elf
@@ -141,9 +142,9 @@ share/twelf/examples/compile/debruijn1/mini-ml.elf
 share/twelf/examples/compile/debruijn1/sources.cfg
 share/twelf/examples/compile/debruijn1/test.cfg
 share/twelf/examples/compile/debruijn1/trans.elf
+share/twelf/examples/cpsocc/corr.elf
 share/twelf/examples/cpsocc/NOTES
 share/twelf/examples/cpsocc/READ.ME
-share/twelf/examples/cpsocc/corr.elf
 share/twelf/examples/cpsocc/cpsBNF.elf
 share/twelf/examples/cpsocc/def1+5+fig4.elf
 share/twelf/examples/cpsocc/def13.elf
@@ -175,8 +176,8 @@ share/twelf/examples/cpsocc/th15.elf
 share/twelf/examples/cpsocc/th18.elf
 share/twelf/examples/cpsocc/th4.elf
 share/twelf/examples/cpsocc/th8.elf
-share/twelf/examples/cut-elim/README
 share/twelf/examples/cut-elim/cl-admit.elf
+share/twelf/examples/cut-elim/README
 share/twelf/examples/cut-elim/cl-cut.elf
 share/twelf/examples/cut-elim/cl-elim.elf
 share/twelf/examples/cut-elim/cl.elf
@@ -190,10 +191,10 @@ share/twelf/examples/cut-elim/int.elf
 share/twelf/examples/cut-elim/int.thm
 share/twelf/examples/cut-elim/sources.cfg
 share/twelf/examples/cut-elim/test.cfg
+share/twelf/examples/fol/sources.cfg
 share/twelf/examples/fol/README
 share/twelf/examples/fol/fol.elf
 share/twelf/examples/fol/fol.thm
-share/twelf/examples/fol/sources.cfg
 share/twelf/examples/fol/test.cfg
 share/twelf/examples/guide/arith.elf
 share/twelf/examples/guide/lam.elf
@@ -201,16 +202,16 @@ share/twelf/examples/guide/lists.elf
 share/twelf/examples/guide/nd.elf
 share/twelf/examples/guide/sources.cfg
 share/twelf/examples/guide/test.cfg
+share/twelf/examples/handbook/sources.cfg
 share/twelf/examples/handbook/README
 share/twelf/examples/handbook/fol.elf
-share/twelf/examples/handbook/sources.cfg
 share/twelf/examples/handbook/test.cfg
+share/twelf/examples/incll/incll.elf
 share/twelf/examples/incll/README
 share/twelf/examples/incll/bff-incll.elf
 share/twelf/examples/incll/bff-incll.quy
 share/twelf/examples/incll/cpm-incll.elf
 share/twelf/examples/incll/cpm-incll.quy
-share/twelf/examples/incll/incll.elf
 share/twelf/examples/incll/iosequents.elf
 share/twelf/examples/incll/lists-incll.elf
 share/twelf/examples/incll/lists-incll.quy
@@ -227,8 +228,8 @@ share/twelf/examples/incll/sort-incll.elf
 share/twelf/examples/incll/sort-incll.quy
 share/twelf/examples/incll/sources.cfg
 share/twelf/examples/incll/test.cfg
-share/twelf/examples/kolm/README
 share/twelf/examples/kolm/complete.elf
+share/twelf/examples/kolm/README
 share/twelf/examples/kolm/examples.quy
 share/twelf/examples/kolm/fol.elf
 share/twelf/examples/kolm/kolmtrans.elf
@@ -238,20 +239,6 @@ share/twelf/examples/kolm/report.ps
 share/twelf/examples/kolm/sound.elf
 share/twelf/examples/kolm/sources.cfg
 share/twelf/examples/kolm/test.cfg
-share/twelf/examples/lp-horn/canon.elf
-share/twelf/examples/lp-horn/conv.elf
-share/twelf/examples/lp-horn/examples.quy
-share/twelf/examples/lp-horn/iscan.elf
-share/twelf/examples/lp-horn/natded.elf
-share/twelf/examples/lp-horn/sources.cfg
-share/twelf/examples/lp-horn/test.cfg
-share/twelf/examples/lp-horn/uni-can.elf
-share/twelf/examples/lp-horn/uni-can.thm
-share/twelf/examples/lp-horn/uni-complete.elf
-share/twelf/examples/lp-horn/uni-complete.thm
-share/twelf/examples/lp-horn/uni-sound.elf
-share/twelf/examples/lp-horn/uni-sound.thm
-share/twelf/examples/lp-horn/uniform.elf
 share/twelf/examples/lp/canon.elf
 share/twelf/examples/lp/cont.elf
 share/twelf/examples/lp/conv.elf
@@ -269,8 +256,22 @@ share/twelf/examples/lp/test.cfg
 share/twelf/examples/lp/uni-complete.elf
 share/twelf/examples/lp/uni-sound.elf
 share/twelf/examples/lp/uniform.elf
-share/twelf/examples/mini-ml/README
+share/twelf/examples/lp-horn/canon.elf
+share/twelf/examples/lp-horn/conv.elf
+share/twelf/examples/lp-horn/examples.quy
+share/twelf/examples/lp-horn/iscan.elf
+share/twelf/examples/lp-horn/natded.elf
+share/twelf/examples/lp-horn/sources.cfg
+share/twelf/examples/lp-horn/test.cfg
+share/twelf/examples/lp-horn/uni-can.elf
+share/twelf/examples/lp-horn/uni-can.thm
+share/twelf/examples/lp-horn/uni-complete.elf
+share/twelf/examples/lp-horn/uni-complete.thm
+share/twelf/examples/lp-horn/uni-sound.elf
+share/twelf/examples/lp-horn/uni-sound.thm
+share/twelf/examples/lp-horn/uniform.elf
 share/twelf/examples/mini-ml/closed.elf
+share/twelf/examples/mini-ml/README
 share/twelf/examples/mini-ml/eval.elf
 share/twelf/examples/mini-ml/eval1.elf
 share/twelf/examples/mini-ml/eval2.elf
@@ -293,21 +294,28 @@ share/twelf/examples/polylam/examples.quy
 share/twelf/examples/polylam/polylam.elf
 share/twelf/examples/polylam/sources.cfg
 share/twelf/examples/polylam/test.cfg
-share/twelf/examples/prop-calc/README
 share/twelf/examples/prop-calc/equiv.elf
+share/twelf/examples/prop-calc/README
 share/twelf/examples/prop-calc/equiv.thm
 share/twelf/examples/prop-calc/examples.quy
+share/twelf/examples/prop-calc/nd.elf
+share/twelf/examples/prop-calc/nd.tex
+share/twelf/examples/prop-calc/ndclass.elf
+share/twelf/examples/prop-calc/prop-calc-solution.elf
 share/twelf/examples/prop-calc/prop-calc.elf
 share/twelf/examples/prop-calc/sources.cfg
 share/twelf/examples/prop-calc/test.cfg
-share/twelf/examples/tabled/README
-share/twelf/examples/tabled/all.sml
+share/twelf/examples/prop-calc/thm1.elf
+share/twelf/examples/prop-calc/thm2.elf
+share/twelf/examples/prop-calc/thm3.elf
 share/twelf/examples/tabled/ccc/README
 share/twelf/examples/tabled/ccc/ccc.elf
-share/twelf/examples/tabled/ccc/tab-examples.quy
 share/twelf/examples/tabled/ccc/tab.cfg
-share/twelf/examples/tabled/cr/lam.elf
+share/twelf/examples/tabled/ccc/tab-examples.quy
+share/twelf/examples/tabled/README
+share/twelf/examples/tabled/all.sml
 share/twelf/examples/tabled/cr/ord-red.elf
+share/twelf/examples/tabled/cr/lam.elf
 share/twelf/examples/tabled/cr/par-red.elf
 share/twelf/examples/tabled/cr/tab-examples.quy
 share/twelf/examples/tabled/cr/tab.cfg
@@ -336,6 +344,19 @@ share/twelf/examples/tabled/refine/programs.elf
 share/twelf/examples/tabled/refine/refex.elf
 share/twelf/examples/tabled/refine/refex.quy
 share/twelf/examples/tabled/refine/tab.cfg
+share/twelf/examples/tabled/seqCalc/focus.elf
+share/twelf/examples/tabled/seqCalc/foc.cfg
+share/twelf/examples/tabled/seqCalc/fol-int-at.elf
+share/twelf/examples/tabled/seqCalc/formulas.elf
+share/twelf/examples/tabled/seqCalc/int-atom.elf
+share/twelf/examples/tabled/seqCalc/int.elf
+share/twelf/examples/tabled/seqCalc/sources.cfg
+share/twelf/examples/tabled/seqCalc/tab-at.cfg
+share/twelf/examples/tabled/seqCalc/tab-ex-all.quy
+share/twelf/examples/tabled/seqCalc/tab-ex-np.quy
+share/twelf/examples/tabled/seqCalc/tab-foc-all.quy
+share/twelf/examples/tabled/seqCalc/tab-fol.cfg
+share/twelf/examples/tabled/seqCalc/tab.cfg
 share/twelf/examples/tabled/subtype/mini-ml.elf
 share/twelf/examples/tabled/subtype/subtype.elf
 share/twelf/examples/tabled/subtype/tab-examples.quy
@@ -344,8 +365,8 @@ share/twelf/examples/tabled/subtype1/basic.elf
 share/twelf/examples/tabled/subtype1/mini-ml.elf
 share/twelf/examples/tabled/subtype1/tab-examples.quy
 share/twelf/examples/tabled/subtype1/tab.cfg
-share/twelf/examples/tabled/tests/tab.cfg
 share/twelf/examples/tabled/tests/test1.elf
+share/twelf/examples/tabled/tests/tab.cfg
 share/twelf/examples/tabled/tests/test2.elf
 share/twelf/examples/tabled/tests/test3.elf
 share/twelf/examples/tabled/tests/test4.elf
@@ -393,9 +414,49 @@ share/twelf/examples-clp/sieve/sieve.elf
 share/twelf/examples-clp/sieve/sieve2.elf
 share/twelf/examples-clp/sieve/sources.cfg
 share/twelf/examples-clp/sieve/test.cfg
+share/twelf/exercises/opt-eval/eval.elf
+share/twelf/exercises/opt-eval/README
+share/twelf/exercises/opt-eval/examples.quy
+share/twelf/exercises/opt-eval/mini-ml.elf
+share/twelf/exercises/opt-eval/opt-equiv1.elf
+share/twelf/exercises/opt-eval/opt-equiv1.thm
+share/twelf/exercises/opt-eval/opt-equiv2.elf
+share/twelf/exercises/opt-eval/opt-equiv2.thm
+share/twelf/exercises/opt-eval/opt-eval.elf
+share/twelf/exercises/opt-eval/opt-mini-ml.elf
+share/twelf/exercises/opt-eval/opt-rep1.elf
+share/twelf/exercises/opt-eval/opt-rep2.elf
+share/twelf/exercises/opt-eval/sources.cfg
+share/twelf/exercises/opt-eval/test.cfg
+share/twelf/exercises/README
+share/twelf/exercises/units/eqtypes.elf
+share/twelf/exercises/units/NOTES
+share/twelf/exercises/units/README
+share/twelf/exercises/units/constants.elf
+share/twelf/exercises/units/eqtype-lemmas.elf
+share/twelf/exercises/units/equnits-alg.elf
+share/twelf/exercises/units/equnits-sound.elf
+share/twelf/exercises/units/equnits.elf
+share/twelf/exercises/units/eval.elf
+share/twelf/exercises/units/examples.quy
+share/twelf/exercises/units/language.elf
+share/twelf/exercises/units/number.elf
+share/twelf/exercises/units/sources.cfg
+share/twelf/exercises/units/test.cfg
+share/twelf/exercises/units/tp-complete.elf
+share/twelf/exercises/units/tp-inf.elf
+share/twelf/exercises/units/tp-preserve.elf
+share/twelf/exercises/units/tp-rules.elf
+share/twelf/exercises/units/tp-sound.elf
+share/twelf/exercises/units/types.elf
+share/twelf/exercises/units/units.elf
+share/twelf/exercises/units/value.elf
 share/twelf/tex/code.sty
 share/twelf/tex/example.tex
 share/twelf/tex/twelf.sty
+share/twelf/vim/filetype.vim
+share/twelf/vim/README
+share/twelf/vim/syntax/twelf.vim
 @dirrm libexec/twelf/bin/.heap
 @dirrm libexec/twelf/bin
 @dirrm libexec/twelf
@@ -435,6 +496,7 @@ share/twelf/tex/twelf.sty
 @dirrm share/twelf/examples/tabled/parsing
 @dirrm share/twelf/examples/tabled/poly
 @dirrm share/twelf/examples/tabled/refine
+@dirrm share/twelf/examples/tabled/seqCalc
 @dirrm share/twelf/examples/tabled/subtype
 @dirrm share/twelf/examples/tabled/subtype1
 @dirrm share/twelf/examples/tabled/tests
@@ -450,5 +512,10 @@ share/twelf/tex/twelf.sty
 @dirrm share/twelf/examples-clp/pelletier
 @dirrm share/twelf/examples-clp/sieve
 @dirrm share/twelf/examples-clp
+@dirrm share/twelf/exercises/opt-eval
+@dirrm share/twelf/exercises/units
+@dirrm share/twelf/exercises
 @dirrm share/twelf/tex
+@dirrm share/twelf/vim/syntax
+@dirrm share/twelf/vim
 @dirrm share/twelf