diff --git a/src/cmd/proof/font.c b/src/cmd/proof/font.c
new file mode 100644
index 0000000..d930f34
--- /dev/null
+++ b/src/cmd/proof/font.c
@@ -0,0 +1,372 @@
+#include <u.h>
+#include <libc.h>
+#include <draw.h>
+#include <event.h>
+#include <bio.h>
+#include "proof.h"
+
+char	fname[NFONT][20];		/* font names */
+char lastload[NFONT][20];	/* last file name prefix loaded for this font */
+Font	*fonttab[NFONT][NSIZE];	/* pointers to fonts */
+int	fmap[NFONT];		/* what map to use with this font */
+
+static void	loadfont(int, int);
+static void	fontlookup(int, char *);
+static void	buildxheight(Biobuf*);
+static void	buildmap(Biobuf*);
+static void	buildtroff(char *);
+static void	addmap(int, char *, int);
+static char	*map(Rune*, int);
+static void	scanstr(char *, char *, char **);
+
+int	specfont;	/* somehow, number of special font */
+
+#define	NMAP	5
+#define	QUICK	2048	/* char values less than this are quick to look up */
+#define	eq(s,t)	strcmp((char *) s, (char *) t) == 0
+
+int	curmap	= -1;	/* what map are we working on */
+
+typedef struct Link Link;
+struct Link	/* link names together */
+{
+	uchar	*name;
+	int	val;
+	Link	*next;
+};
+
+typedef struct Map Map;
+struct Map	/* holds a mapping from uchar name to index */
+{
+	double	xheight;
+	Rune	quick[QUICK];	/* low values get special treatment */
+	Link	*slow;	/* other stuff goes into a link list */
+};
+
+Map	charmap[5];
+
+typedef struct Fontmap Fontmap;
+struct Fontmap	/* mapping from troff name to filename */
+{
+	char	*troffname;
+	char	*prefix;
+	int	map;		/* which charmap to use for this font */
+	char	*fallback;	/* font to look in if can't find char here */
+};
+
+Fontmap	fontmap[100];
+int	pos2fontmap[NFONT];	/* indexed by troff font position, gives Fontmap */
+int	nfontmap	= 0;	/* how many are there */
+
+
+void
+dochar(Rune r[])
+{
+	char *s, *fb;
+	Font *f;
+	Point p;
+	int fontno, fm, i;
+	char buf[10];
+
+	fontno = curfont;
+	if((s = map(r, curfont)) == 0){		/* not on current font */
+		if ((s = map(r, specfont)) != 0)	/* on special font */
+			fontno = specfont;
+		else{
+			/* look for fallback */
+			fm = pos2fontmap[curfont];
+			fb = fontmap[fm].fallback;
+			if(fb){
+				/* see if fallback is mounted */
+				for(i = 0; i < NFONT; i++){
+					if(eq(fb, fontmap[pos2fontmap[i]].troffname)){
+						s = map(r, i);
+						if(s){
+							fontno = i;
+							goto found;
+						}
+					}
+				}
+			}
+			/* no such char; use name itself on defont */
+			/* this is not a general solution */
+			p.x = hpos/DIV + xyoffset.x + offset.x;
+			p.y = vpos/DIV + xyoffset.y + offset.y;
+			p.y -= font->ascent;
+			sprint(buf, "%S", r);
+			string(screen, p, display->black, ZP, font, buf);
+			return;
+		}
+	}
+    found:
+	p.x = hpos/DIV + xyoffset.x + offset.x;
+	p.y = vpos/DIV + xyoffset.y + offset.y;
+	while ((f = fonttab[fontno][cursize]) == 0)
+		loadfont(fontno, cursize);
+	p.y -= f->ascent;
+	dprint(2, "putting %S at %d,%d font %d, size %d\n", r, p.x, p.y, fontno, cursize);
+	string(screen, p, display->black, ZP, f, s);
+}
+
+static int drawlog2[] = { 
+	0, 0, 
+	1, 1, 
+	2, 2, 2, 2, 
+	3, 3, 3, 3, 3, 3, 3, 3, 
+	4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 4, 
+	5
+};
+
+static void
+loadfont(int n, int s)
+{
+	char file[100];
+	int i, fd, t, deep;
+	static char *try[3] = {"", "times/R.", "pelm/"};
+	Subfont *f;
+	Font *ff;
+
+	try[0] = fname[n];
+	dprint(2, "loadfont %d %d\n", n, s);
+	for (t = 0; t < 3; t++){
+		i = s * mag * charmap[fmap[n]].xheight/0.72;	/* a pixel is 0.72 points */
+		if (i < MINSIZE)
+			i = MINSIZE;
+		dprint(2, "size %d, i %d, mag %g\n", s, i, mag);
+		for(; i >= MINSIZE; i--){
+			/* if .font file exists, take that */
+			sprint(file, "%s/%s%d.font", libfont, try[t], i);
+			ff = openfont(display, file);
+			if(ff != 0){
+				fonttab[n][s] = ff;
+				dprint(2, "using %s for font %d %d\n", file, n, s);
+				return;
+			}
+			/* else look for a subfont file */
+			for (deep = drawlog2[screen->depth]; deep >= 0; deep--){
+				sprint(file, "%s/%s%d.%d", libfont, try[t], i, deep);
+				dprint(2, "trying %s for %d\n", file, i);
+				if ((fd = open(file, 0)) >= 0){
+					f = readsubfont(display, file, fd, 0);
+					if (f == 0) {
+						fprint(2, "can't rdsubfontfile %s: %r\n", file);
+						exits("rdsubfont");
+					}
+					close(fd);
+					ff = mkfont(f, 0);
+					if(ff == 0){
+						fprint(2, "can't mkfont %s: %r\n", file);
+						exits("rdsubfont");
+					}
+					fonttab[n][s] = ff;
+					dprint(2, "using %s for font %d %d\n", file, n, s);
+					return;
+				}
+			}
+		}
+	}
+	fprint(2, "can't find font %s.%d or substitute, quitting\n", fname[n], s);
+	exits("no font");
+}
+
+void
+loadfontname(int n, char *s)
+{
+	int i;
+	Font *f, *g = 0;
+
+	if (strcmp(s, fname[n]) == 0)
+		return;
+	if(fname[n] && fname[n][0]){
+		if(lastload[n] && strcmp(lastload[n], fname[n]) == 0)
+			return;
+		strcpy(lastload[n], fname[n]);
+	}
+	fontlookup(n, s);
+	for (i = 0; i < NSIZE; i++)
+		if (f = fonttab[n][i]){
+			if (f != g) {
+				freefont(f);
+				g = f;
+			}
+			fonttab[n][i] = 0;
+		}
+}
+
+void
+allfree(void)
+{
+	int i;
+
+	for (i=0; i<NFONT; i++)
+		loadfontname(i, "??");
+}
+
+
+void
+readmapfile(char *file)
+{
+	Biobuf *fp;
+	char *p, cmd[100];
+
+	if ((fp=Bopen(file, OREAD)) == 0){
+		fprint(2, "proof: can't open map file %s\n", file);
+		exits("urk");
+	}
+	while((p=Brdline(fp, '\n')) != 0) {
+		p[Blinelen(fp)-1] = 0;
+		scanstr(p, cmd, 0);
+		if(p[0]=='\0' || eq(cmd, "#"))	/* skip comments, empty */
+			continue;
+		else if(eq(cmd, "xheight"))
+			buildxheight(fp);
+		else if(eq(cmd, "map"))
+			buildmap(fp);
+		else if(eq(cmd, "special"))
+			buildtroff(p);
+		else if(eq(cmd, "troff"))
+			buildtroff(p);
+		else
+			fprint(2, "weird map line %s\n", p);
+	}
+	Bterm(fp);
+}
+
+static void
+buildxheight(Biobuf *fp)	/* map goes from char name to value to print via *string() */
+{
+	char *line;
+
+	line = Brdline(fp, '\n');
+	if(line == 0){
+		fprint(2, "proof: bad map file\n");
+		exits("map");
+	}
+	charmap[curmap].xheight = atof(line);
+}
+
+static void
+buildmap(Biobuf *fp)	/* map goes from char name to value to print via *string() */
+{
+	uchar *p, *line, ch[100];
+	int val;
+	Rune r;
+
+	curmap++;
+	if(curmap >= NMAP){
+		fprint(2, "proof: out of char maps; recompile\n");
+		exits("charmap");
+	}
+	while ((line = Brdline(fp, '\n'))!= 0){
+		if (line[0] == '\n')
+			return;
+		line[Blinelen(fp)-1] = 0;
+		scanstr((char *) line, (char *) ch, (char **)(void*)&p);
+		if (ch[0] == '\0') {
+			fprint(2, "bad map file line '%s'\n", (char*)line);
+			continue;
+		}
+		val = strtol((char *) p, 0, 10);
+dprint(2, "buildmap %s (%x %x) %s %d\n", (char*)ch, ch[0], ch[1], (char*)p, val);
+		chartorune(&r, (char*)ch);
+		if(utflen((char*)ch)==1 && r<QUICK)
+			charmap[curmap].quick[r] = val;
+		else
+			addmap(curmap, strdup((char *) ch), val);	/* put somewhere else */
+	}
+}
+
+static void
+addmap(int n, char *s, int val)	/* stick a new link on */
+{
+	Link *p = (Link *) malloc(sizeof(Link));
+	Link *prev = charmap[n].slow;
+
+	if(p == 0)
+		exits("out of memory in addmap");
+	p->name = (uchar *) s;
+	p->val = val;
+	p->next = prev;
+	charmap[n].slow = p;
+}
+
+static void
+buildtroff(char *buf)	/* map troff names into bitmap filenames */
+{				/* e.g., R -> times/R., I -> times/I., etc. */
+	char *p, cmd[100], name[200], prefix[400], fallback[100];
+
+	scanstr(buf, cmd, &p);
+	scanstr(p, name, &p);
+	scanstr(p, prefix, &p);
+	while(*p!=0 && isspace(*p))
+		p++;
+	if(*p != 0){
+		scanstr(p, fallback, &p);
+		fontmap[nfontmap].fallback = strdup(fallback);
+	}else
+		fontmap[nfontmap].fallback = 0;
+	fontmap[nfontmap].troffname = strdup(name);
+	fontmap[nfontmap].prefix = strdup(prefix);
+	fontmap[nfontmap].map = curmap;
+	dprint(2, "troff name %s is bitmap %s map %d in slot %d fallback %s\n", name, prefix, curmap, nfontmap, fontmap[nfontmap].fallback? fontmap[nfontmap].fallback : "<null>");
+	nfontmap++;
+}
+
+static void
+fontlookup(int n, char *s)	/* map troff name of s into position n */
+{
+	int i;
+
+	for(i = 0; i < nfontmap; i++)
+		if (eq(s, fontmap[i].troffname)) {
+			strcpy(fname[n], fontmap[i].prefix);
+			fmap[n] = fontmap[i].map;
+			pos2fontmap[n] = i;
+			if (eq(s, "S"))
+				specfont = n;
+			dprint(2, "font %d %s is %s\n", n, s, fname[n]);
+			return;
+		}
+	/* god help us if this font isn't there */
+}
+
+
+static char *
+map(Rune rp[], int font)	/* figure out mapping for char in this font */
+{
+	static char s[100];
+	char c[10];
+	Link *p;
+	Rune r;
+
+	if(rp[1]==0 &&  rp[0]<QUICK)	/* fast lookup */
+		r = charmap[fmap[font]].quick[rp[0]];
+	else {	/* high-valued or compound character name */
+		sprint(c, "%S", rp);
+		r = 0;
+		for (p = charmap[fmap[font]].slow; p; p = p->next)
+			if(eq(c, p->name)){
+				r = p->val;
+				break;
+			}
+	}
+	if(r == 0){	/* not there */
+		dprint(2, "didn't find %S font# %d\n", rp, font);
+		return 0;
+	}
+	dprint(2, "map %S to %s font# %d\n", rp, s, font);
+	s[runetochar(s, &r)] = 0;
+	return s;
+}
+
+static void
+scanstr(char *s, char *ans, char **ep)
+{
+	for (; isspace((uchar) *s); s++)
+		;
+	for (; *s!=0 && !isspace((uchar) *s); )
+		*ans++ = *s++;
+	*ans = 0;
+	if (ep)
+		*ep = s;
+}
diff --git a/src/cmd/proof/htroff.c b/src/cmd/proof/htroff.c
new file mode 100644
index 0000000..d591d38
--- /dev/null
+++ b/src/cmd/proof/htroff.c
@@ -0,0 +1,579 @@
+#include	<u.h>
+#include	<libc.h>
+#include	<draw.h>
+#include	<cursor.h>
+#include	<event.h>
+#include	<bio.h>
+#include	"proof.h"
+
+int	res;
+int	hpos;
+int	vpos;
+int	DIV = 11;
+
+Point offset;
+Point xyoffset = { 0,0 };
+
+Rectangle	view[MAXVIEW];
+Rectangle	bound[MAXVIEW];		/* extreme points */
+int	nview = 1;
+
+int	lastp;	/* last page number we were on */
+
+#define	NPAGENUMS	200
+struct pagenum {
+	int	num;
+	long	adr;
+} pagenums[NPAGENUMS];
+int	npagenums;
+
+int	curfont, cursize;
+
+char	*getcmdstr(void);
+
+static void	initpage(void);
+static void	view_setup(int);
+static Point	scale(Point);
+static void	clearview(Rectangle);
+static int	addpage(int);
+static void	spline(Image *, int, Point *);
+static int	skipto(int, int);
+static void	wiggly(int);
+static void	devcntrl(void);
+static void	eatline(void);
+static int	getn(void);
+static int	botpage(int);
+static void	getstr(char *);
+/*
+static void	getutf(char *);
+*/
+
+#define Do screen->r.min
+#define Dc screen->r.max
+
+/* declarations and definitions of font stuff are in font.c and main.c */
+
+static void
+initpage(void)
+{
+	int i;
+
+	view_setup(nview);
+	for (i = 0; i < nview-1; i++)
+		draw(screen, view[i], screen, nil, view[i+1].min);
+	clearview(view[nview-1]);
+	offset = view[nview-1].min;
+	vpos = 0;
+}
+
+static void
+view_setup(int n)
+{
+	int i, j, v, dx, dy, r, c;
+
+	switch (n) {
+	case 1: r = 1; c = 1; break;
+	case 2: r = 1; c = 2; break;
+	case 3: r = 1; c = 3; break;
+	case 4: r = 2; c = 2; break;
+	case 5: case 6: r = 2; c = 3; break;
+	case 7: case 8: case 9: r = 3; c = 3; break;
+	default: r = (n+2)/3; c = 3; break; /* finking out */
+	}
+	dx = (Dc.x - Do.x) / c;
+	dy = (Dc.y - Do.y) / r;
+	v = 0;
+	for (i = 0; i < r && v < n; i++)
+		for (j = 0; j < c && v < n; j++) {
+			view[v] = screen->r;
+			view[v].min.x = Do.x + j * dx;
+			view[v].max.x = Do.x + (j+1) * dx;
+			view[v].min.y = Do.y + i * dy;
+			view[v].max.y = Do.y + (i+1) * dy;
+			v++;
+		}
+}
+
+static void
+clearview(Rectangle r)
+{
+	draw(screen, r, display->white, nil, r.min);
+}
+
+int resized;
+void eresized(int new)
+{
+	/* this is called if we are resized */
+	if(new && getwindow(display, Refnone) < 0)
+		drawerror(display, "can't reattach to window");
+	initpage();
+	resized = 1;
+}
+
+static Point
+scale(Point p)
+{
+	p.x /= DIV;
+	p.y /= DIV;
+	return addpt(xyoffset, addpt(offset,p));
+}
+
+static int
+addpage(int n)
+{
+	int i;
+
+	for (i = 0; i < npagenums; i++)
+		if (n == pagenums[i].num)
+			return i;
+	if (npagenums < NPAGENUMS-1) {
+		pagenums[npagenums].num = n;
+		pagenums[npagenums].adr = offsetc();
+		npagenums++;
+	}
+	return npagenums;
+}
+
+void
+readpage(void)
+{
+	int c, i, a, alpha, phi;
+	static int first = 0;
+	int m, n, gonow = 1;
+	Rune r[32], t;
+	Point p,q,qq;
+
+	offset = screen->clipr.min;
+	esetcursor(&deadmouse);
+	while (gonow)
+	{
+		c = getc();
+		switch (c)
+		{
+		case -1:
+			esetcursor(0);
+			if (botpage(lastp+1)) {
+				initpage();
+				break;
+			}
+			exits(0);
+		case 'p':	/* new page */
+			lastp = getn();
+			addpage(lastp);
+			if (first++ > 0) {
+				esetcursor(0);
+				botpage(lastp);
+				esetcursor(&deadmouse);
+			}
+			initpage();
+			break;
+		case '\n':	/* when input is text */
+		case ' ':
+		case 0:		/* occasional noise creeps in */
+			break;
+		case '0': case '1': case '2': case '3': case '4':
+		case '5': case '6': case '7': case '8': case '9':
+			/* two motion digits plus a character */
+			hpos += (c-'0')*10 + getc()-'0';
+
+		/* FALLS THROUGH */
+		case 'c':	/* single ascii character */
+			r[0] = getrune();
+			r[1] = 0;
+			dochar(r);
+			break;
+
+		case 'C':
+			for(i=0; ; i++){
+				t = getrune();
+				if(isspace(t))
+					break;
+				r[i] = t;
+			}
+			r[i] = 0;
+			dochar(r);
+			break;
+
+		case 'N':
+			r[0] = getn();
+			r[1] = 0;
+			dochar(r);
+			break;
+
+		case 'D':	/* draw function */
+			switch (getc())
+			{
+			case 'l':	/* draw a line */
+				n = getn();
+				m = getn();
+				p = Pt(hpos,vpos);
+				q = addpt(p, Pt(n,m));
+				hpos += n;
+				vpos += m;
+				line(screen, scale(p), scale(q), 0, 0, 0, display->black, ZP);
+				break;
+			case 'c':	/* circle */
+				/*nop*/
+				m = getn()/2;
+				p = Pt(hpos+m,vpos);
+				hpos += 2*m;
+				ellipse(screen, scale(p), m/DIV, m/DIV, 0, display->black, ZP);
+				/* p=currentpt; p.x+=dmap(m/2);circle bp,p,a,ONES,Mode*/
+				break;
+			case 'e':	/* ellipse */
+				/*nop*/
+				m = getn()/2;
+				n = getn()/2;
+				p = Pt(hpos+m,vpos);
+				hpos += 2*m;
+				ellipse(screen, scale(p), m/DIV, n/DIV, 0, display->black, ZP);
+				break;
+			case 'a':	/* arc */
+				p = scale(Pt(hpos,vpos));
+				n = getn();
+				m = getn();
+				hpos += n;
+				vpos += m;
+				q = scale(Pt(hpos,vpos));
+				n = getn();
+				m = getn();
+				hpos += n;
+				vpos += m;
+				qq = scale(Pt(hpos,vpos));
+				/*
+				  * tricky: convert from 3-point clockwise to
+				  * center, angle1, delta-angle counterclockwise.
+				 */
+				a = hypot(qq.x-q.x, qq.y-q.y);
+				phi = atan2(q.y-p.y, p.x-q.x)*180./PI;
+				alpha = atan2(q.y-qq.y, qq.x-q.x)*180./PI - phi;
+				if(alpha < 0)
+					alpha += 360;
+				arc(screen, q, a, a, 0, display->black, ZP, phi, alpha);
+				break;
+			case '~':	/* wiggly line */
+				wiggly(0);
+				break;
+			default:
+				break;
+			}
+			eatline();
+			break;
+		case 's':
+			n = getn();	/* ignore fractional sizes */
+			if (cursize == n)
+				break;
+			cursize = n;
+			if (cursize >= NFONT)
+				cursize = NFONT-1;
+			break;
+		case 'f':
+			curfont = getn();
+			break;
+		case 'H':	/* absolute horizontal motion */
+			hpos = getn();
+			break;
+		case 'h':	/* relative horizontal motion */
+			hpos += getn();
+			break;
+		case 'w':	/* word space */
+			break;
+		case 'V':
+			vpos = getn();
+			break;
+		case 'v':
+			vpos += getn();
+			break;
+		case '#':	/* comment */
+		case 'n':	/* end of line */
+			eatline();
+			break;
+		case 'x':	/* device control */
+			devcntrl();
+			break;
+		default:
+			fprint(2, "unknown input character %o %c at offset %lud\n", c, c, offsetc());
+			exits("bad char");
+		}
+	}
+	esetcursor(0);
+}
+
+static void
+spline(Image *b, int n, Point *pp)
+{
+	long w, t1, t2, t3, fac=1000; 
+	int i, j, steps=10; 
+	Point p, q;
+
+	for (i = n; i > 0; i--)
+		pp[i] = pp[i-1];
+	pp[n+1] = pp[n];
+	n += 2;
+	p = pp[0];
+	for(i = 0; i < n-2; i++)
+	{
+		for(j = 0; j < steps; j++)
+		{
+			w = fac * j / steps;
+			t1 = w * w / (2 * fac);
+			w = w - fac/2;
+			t2 = 3*fac/4 - w * w / fac;
+			w = w - fac/2;
+			t3 = w * w / (2*fac);
+			q.x = (t1*pp[i+2].x + t2*pp[i+1].x + 
+				t3*pp[i].x + fac/2) / fac;
+			q.y = (t1*pp[i+2].y + t2*pp[i+1].y + 
+				t3*pp[i].y + fac/2) / fac;
+			line(b, p, q, 0, 0, 0, display->black, ZP);
+			p = q;
+		}
+	}
+}
+
+/* Have to parse skipped pages, to find out what fonts are loaded. */
+static int
+skipto(int gotop, int curp)
+{
+	char *p;
+	int i;
+
+	if (gotop == curp)
+		return 1;
+	for (i = 0; i < npagenums; i++)
+		if (pagenums[i].num == gotop) {
+			if (seekc(pagenums[i].adr) == Beof) {
+				fprint(2, "can't rewind input\n");
+				return 0;
+			}
+			return 1;
+		}
+	if (gotop <= curp) {
+	    restart:
+		if (seekc(0) == Beof) {
+			fprint(2, "can't rewind input\n");
+			return 0;
+		}
+	}
+	for(;;){
+		p = rdlinec();
+		if (p == 0) {
+			if(gotop>curp){
+				gotop = curp;
+				goto restart;
+			}
+			return 0;
+		} else if (*p == 'p') {
+			lastp = curp = atoi(p+1);
+			addpage(lastp);	/* maybe 1 too high */
+			if (curp>=gotop)
+				return 1;
+		}
+	}
+}
+
+static void
+wiggly(int skip)
+{
+	Point p[300];
+	int c,i,n;
+	for (n = 1; (c = getc()) != '\n' && c>=0; n++) {
+		ungetc();
+		p[n].x = getn();
+		p[n].y = getn();
+	}
+	p[0] = Pt(hpos, vpos);
+	for (i = 1; i < n; i++)
+		p[i] = addpt(p[i],p[i-1]);
+	hpos = p[n-1].x;
+	vpos = p[n-1].y;
+	for (i = 0; i < n; i++)
+		p[i] = scale(p[i]);
+	if (!skip)
+		spline(screen,n,p);
+}
+
+static void
+devcntrl(void)	/* interpret device control functions */
+{
+        char str[80];
+	int n;
+
+	getstr(str);
+	switch (str[0]) {	/* crude for now */
+	case 'i':	/* initialize */
+		break;
+	case 'T':	/* device name */
+		getstr(devname);
+		break;
+	case 't':	/* trailer */
+		break;
+	case 'p':	/* pause -- can restart */
+		break;
+	case 's':	/* stop */
+		break;
+	case 'r':	/* resolution assumed when prepared */
+		res=getn();
+		DIV = floor(.5 + res/(100.0*mag));
+		if (DIV < 1)
+			DIV = 1;
+		mag = res/(100.0*DIV); /* adjust mag according to DIV coarseness */
+		break;
+	case 'f':	/* font used */
+		n = getn();
+		getstr(str);
+		loadfontname(n, str);
+		break;
+	/* these don't belong here... */
+	case 'H':	/* char height */
+		break;
+	case 'S':	/* slant */
+		break;
+	case 'X':
+		break;
+	}
+	eatline();
+}
+
+int
+isspace(int c)
+{
+	return c==' ' || c=='\t' || c=='\n';
+}
+
+static void
+getstr(char *is)
+{
+	uchar *s = (uchar *) is;
+
+	for (*s = getc(); isspace(*s); *s = getc())
+		;
+	for (; !isspace(*s); *++s = getc())
+		;
+	ungetc();
+	*s = 0;
+}
+
+#if 0
+static void
+getutf(char *s)		/* get next utf char, as bytes */
+{
+	int c, i;
+
+	for (i=0;;) {
+		c = getc();
+		if (c < 0)
+			return;
+		s[i++] = c;
+
+		if (fullrune(s, i)) {
+			s[i] = 0;
+			return;
+		}
+	}
+}
+#endif
+
+static void
+eatline(void)
+{
+	int c;
+
+	while ((c=getc()) != '\n' && c >= 0)
+		;
+}
+
+static int
+getn(void)
+{
+	int n, c, sign;
+
+	while (c = getc())
+		if (!isspace(c))
+			break;
+	if(c == '-'){
+		sign = -1;
+		c = getc();
+	}else
+		sign = 1;
+	for (n = 0; '0'<=c && c<='9'; c = getc())
+		n = n*10 + c - '0';
+	while (c == ' ')
+		c = getc();
+	ungetc();
+	return(n*sign);
+}
+
+static int
+botpage(int np)	/* called at bottom of page np-1 == top of page np */
+{
+	char *p;
+	int n;
+
+	while (p = getcmdstr()) {
+		if (*p == '\0')
+			return 0;
+		if (*p == 'q')
+			exits(p);
+		if (*p == 'c')		/* nop */
+			continue;
+		if (*p == 'm') {
+			mag = atof(p+1);
+			if (mag <= .1 || mag >= 10)
+				mag = DEFMAG;
+			allfree();	/* zap fonts */
+			DIV = floor(.5 + res/(100.0*mag));
+			if (DIV < 1)
+				DIV = 1;
+			mag = res/(100.0*DIV);
+			return skipto(np-1, np);	/* reprint the page */
+		}
+		if (*p == 'x') {
+			xyoffset.x += atoi(p+1)*100;
+			skipto(np-1, np);
+			return 1;
+		}
+		if (*p == 'y') {
+			xyoffset.y += atoi(p+1)*100;
+			skipto(np-1, np);
+			return 1;
+		}
+		if (*p == '/') {	/* divide into n pieces */
+			nview = atoi(p+1);
+			if (nview < 1)
+				nview = 1;
+			else if (nview > MAXVIEW)
+				nview = MAXVIEW;
+			return skipto(np-1, np);
+		}
+		if (*p == 'p') {
+			if (p[1] == '\0'){	/* bare 'p' */
+				if(skipto(np-1, np))
+					return 1;
+				continue;
+			}
+			p++;
+		}
+		if ('0'<=*p && *p<='9') {
+			n = atoi(p);
+			if(skipto(n, np))
+				return 1;
+			continue;
+		}
+		if (*p == '-' || *p == '+') {
+			n = atoi(p);
+			if (n == 0)
+				n = *p == '-' ? -1 : 1;
+			if(skipto(np - 1 + n, np))
+				return 1;
+			continue;
+		}
+		if (*p == 'd') {
+			dbg = 1 - dbg;
+			continue;
+		}
+
+		fprint(2, "illegal;  try q, 17, +2, -1, p, m.7, /2, x1, y-.5 or return\n");
+	}
+	return 0;
+}
diff --git a/src/cmd/proof/main.c b/src/cmd/proof/main.c
new file mode 100644
index 0000000..5e0c804
--- /dev/null
+++ b/src/cmd/proof/main.c
@@ -0,0 +1,226 @@
+#include	<u.h>
+#include	<libc.h>
+#include	<draw.h>
+#include	<event.h>
+#include	<bio.h>
+#include	"proof.h"
+
+Rectangle rpage = { 0, 0, 850, 1150 };
+char devname[64];
+double mag = DEFMAG;
+int dbg = 0;
+char *track = 0;
+Biobuf bin;
+char *libfont = "#9/font";
+char *mapfile = "MAP";
+char *mapname = "MAP";
+
+void
+usage(void)
+{
+	fprint(2, "usage: proof [-m mag] [-/ nview] [-x xoff] [-y yoff] [-M mapfile] [-F fontdir] [-dt] file...\n");
+	exits("usage");
+}
+
+double
+getnum(char *s)
+{
+	if(s == nil)
+		usage();
+	return atof(s);
+}
+
+char*
+getstr(char *s)
+{
+	if(s == nil)
+		usage();
+	return s;
+}
+
+void
+main(int argc, char *argv[])
+{
+	char c;
+	int dotrack = 0;
+	
+	libfont = unsharp(libfont);
+	ARGBEGIN{
+	case 'm':	/* magnification */
+		mag = getnum(ARGF());
+		if (mag < 0.1 || mag > 10){
+			fprint(2, "ridiculous mag argument ignored\n");
+			mag = DEFMAG;
+		}
+		break;
+	case '/':
+		nview = getnum(ARGF());
+		if (nview < 1 || nview > MAXVIEW)
+			nview = 1;
+		break;
+	case 'x':
+		xyoffset.x += getnum(ARGF()) * 100;
+		break;
+	case 'y':
+		xyoffset.y += getnum(ARGF()) * 100;
+		break;
+	case 'M':	/* change MAP file */
+		mapname = EARGF(usage());
+		break;
+	case 'F':	/* change /lib/font/bit directory */
+		libfont = EARGF(usage());
+		break;
+	case 'd':
+		dbg = 1;
+		break;
+	case 't':
+		dotrack = 1;
+		break;
+	default:
+		usage();
+	}ARGEND
+
+	if (argc > 0) {
+		close(0);
+		if (open(argv[0], 0) != 0) {
+			sysfatal("can't open %s: %r\n", argv[0]);
+			exits("open failure");
+		}
+		if(dotrack)
+			track = argv[0];
+	}
+	Binit(&bin, 0, OREAD);
+	mapfile = smprint("%s/%s", libfont, mapname);
+	readmapfile(mapfile);
+	for (c = 0; c < NFONT; c++)
+		loadfontname(c, "??");
+	mapscreen();
+	clearscreen();
+	readpage(); 
+}
+
+/*
+ * Input buffer to allow us to back up
+ */
+#define	SIZE	100000	/* 8-10 pages, typically */
+
+char	bufc[SIZE];
+char	*inc = bufc;		/* where next input character goes */
+char	*outc = bufc;	/* next character to be read from buffer */
+int	off;		/* position of outc in total input stream */
+
+void
+addc(int c)
+{
+	*inc++ = c;
+	if(inc == &bufc[SIZE])
+		inc = &bufc[0];
+}
+
+int
+getc(void)
+{
+	int c;
+
+	if(outc == inc){
+		c = Bgetc(&bin);
+		if(c == Beof)
+			return Beof;
+		addc(c);
+	}
+	off++;
+	c = *outc++;
+	if(outc == &bufc[SIZE])
+		outc = &bufc[0];
+	return c;
+}
+
+int
+getrune(void)
+{
+	int c, n;
+	Rune r;
+	char buf[UTFmax];
+
+	for(n=0; !fullrune(buf, n); n++){
+		c = getc();
+		if(c == Beof)
+			return Beof;
+		buf[n] = c;
+	}
+	chartorune(&r, buf);
+	return r;
+}
+
+int
+nbuf(void)	/* return number of buffered characters */
+{
+	int ini, outi;
+
+	ini = inc-bufc;
+	outi = outc-bufc;
+	if(ini < outi)
+		ini += SIZE;
+	return ini-outi;
+}
+
+ulong
+seekc(ulong o)
+{
+	ulong avail;
+	long delta;
+
+	delta = off-o;
+	if(delta < 0)
+		return Beof;
+	avail = SIZE-nbuf();
+	if(delta < avail){
+		off = o;
+		outc -= delta;
+		if(outc < &bufc[0])
+			outc += SIZE;
+		return off;
+	}
+	return Beof;
+}
+
+void
+ungetc(void)
+{
+	if(off == 0)
+		return;
+	if(nbuf() == SIZE){
+		fprint(2, "backup buffer overflow\n");
+		return;
+	}
+	if(outc == &bufc[0])
+		outc = &bufc[SIZE];
+	--outc;
+	--off;
+}
+
+ulong
+offsetc(void)
+{
+	return off;
+}
+
+char*
+rdlinec(void)
+{
+	static char buf[2048];
+	int c, i;
+
+	for(i=0; i<sizeof buf; ){
+		c = getc();
+		if(c == Beof)
+			break;
+		buf[i++] = c;
+		if(c == '\n')
+			break;
+	}
+
+	if(i == 0)
+		return nil;
+	return buf;
+}
diff --git a/src/cmd/proof/mkfile b/src/cmd/proof/mkfile
new file mode 100644
index 0000000..c0e877b
--- /dev/null
+++ b/src/cmd/proof/mkfile
@@ -0,0 +1,14 @@
+<$PLAN9/src/mkhdr
+
+TARG=proof
+OFILES=main.$O\
+	font.$O\
+	htroff.$O\
+	screen.$O\
+
+HFILES=proof.h
+
+<$PLAN9/src/mkone
+
+$O.pout: $OFILES
+	$LD -o $O.pout -p $OFILES
diff --git a/src/cmd/proof/portdate b/src/cmd/proof/portdate
new file mode 100644
index 0000000..e076200
--- /dev/null
+++ b/src/cmd/proof/portdate
@@ -0,0 +1,5 @@
+font.c		2004/1225
+htroff.c		2004/1225
+main.c		2004/1225
+proof.h		2004/1225
+screen.c		2004/1225
diff --git a/src/cmd/proof/proof.h b/src/cmd/proof/proof.h
new file mode 100644
index 0000000..73f39b8
--- /dev/null
+++ b/src/cmd/proof/proof.h
@@ -0,0 +1,48 @@
+#include <cursor.h>
+#undef isspace
+#define	NPAGES	500
+#define NFONT	33
+#define NSIZE	40
+#define MINSIZE 4
+#define	DEFMAG	(10.0/11.0)	/* was (10.0/11.0), then 1 */
+#define MAXVIEW 40
+
+#define	ONES	~0
+
+extern	char	devname[];
+extern	double	mag;
+extern	int	nview;
+extern	int	hpos, vpos, curfont, cursize;
+extern	int	DIV, res;
+extern	int	Mode;
+
+extern	Point	offset;		/* for small pages within big page */
+extern	Point	xyoffset;	/* for explicit x,y move */
+extern	Cursor	deadmouse;
+
+extern	char	*libfont;
+
+void	mapscreen(void);
+void	clearscreen(void);
+char	*getcmdstr(void);
+
+void	readmapfile(char *);
+void	dochar(Rune*);
+void	bufput(void);
+void	loadfontname(int, char *);
+void	allfree(void);
+void	readpage(void);
+int	isspace(int);
+
+extern	int	getc(void);
+extern	int	getrune(void);
+extern	void	ungetc(void);
+extern	ulong	offsetc(void);
+extern	ulong	seekc(ulong);
+extern	char*	rdlinec(void);
+
+
+#define	dprint	if (dbg) fprint
+
+extern	int	dbg;
+extern	int	resized;
diff --git a/src/cmd/proof/screen.c b/src/cmd/proof/screen.c
new file mode 100644
index 0000000..dccfe01
--- /dev/null
+++ b/src/cmd/proof/screen.c
@@ -0,0 +1,315 @@
+#include <u.h>
+#include <libc.h>
+#include <draw.h>
+#include <cursor.h>
+#include <event.h>
+#include <bio.h>
+#include "proof.h"
+
+static	int	checkmouse(void);
+/* static	int	buttondown(void); */
+static	char	*getmousestr(void);
+static	char	*getkbdstr(int);
+
+extern	Cursor	blot;
+extern	char	*track;
+
+Mouse	mouse;
+
+void
+mapscreen(void)
+{
+	if(initdraw(0, 0, "proof") < 0){
+		fprint(2, "proof: initdraw failed: %r\n");
+		exits("initdraw");
+	}
+	einit(Ekeyboard|Emouse);
+}
+
+void
+clearscreen(void)
+{
+	draw(screen, screen->r, display->black, nil, ZP);
+}
+
+void
+screenprint(char *fmt, ...)
+{
+	char buf[100];
+	Point p;
+	va_list args;
+
+	va_start(args, fmt);
+	vseprint(buf, &buf[sizeof buf], fmt, args);
+	va_end(args);
+	p = Pt(screen->clipr.min.x+40, screen->clipr.max.y-40);
+	string(screen, p, display->black, ZP, font, buf);
+}
+
+#define	Viewkey	0xb2
+#define etimer(x, y) 0
+
+char *
+getcmdstr(void)
+{
+	Event ev;
+	int e;
+	static ulong timekey = 0;
+	ulong tracktm = 0;
+	Dir *dir;
+
+	if(track){
+		if(timekey == 0)
+			timekey = etimer(0, 5000);
+		dir = dirstat(track);
+		if(dir != nil){
+			tracktm = dir->mtime;
+			free(dir);
+		}
+	}
+	for (;;) {
+		e = event(&ev);
+		if(resized){
+			resized = 0;
+			return "p";
+		}
+		if ((e & Emouse) && ev.mouse.buttons) {
+			mouse = ev.mouse;
+			return getmousestr();
+		} else if (e & Ekeyboard)
+			return getkbdstr(ev.kbdc);	/* sadly, no way to unget */
+		else if (e & timekey) {
+			if((dir = dirstat(track)) != nil){
+				if(tracktm < dir->mtime){
+					free(dir);
+					return "q";
+				}
+				free(dir);
+			}
+		}
+	}
+	return nil;
+}
+
+static char *
+getkbdstr(int c0)
+{
+	static char buf[100];
+	char *p;
+	int c;
+
+	if (c0 == '\n')
+		return "";
+	buf[0] = c0;
+	buf[1] = 0;
+	screenprint("%s", buf);
+	for (p = buf+1; (c = ekbd()) != '\n' && c != '\r' && c != -1 && c != Viewkey; ) {
+		if (c == '\b' && p > buf) {
+			*--p = ' ';
+		} else {
+			*p++ = c;
+			*p = 0;
+		}
+		screenprint("%s", buf);
+	}
+	*p = 0;
+	return buf;
+}
+
+
+#define button3(b)	((b) & 4)
+#define button2(b)	((b) & 2)
+#define button1(b)	((b) & 1)
+#define button23(b)	((b) & 6)
+#define button123(b)	((b) & 7)
+
+#define	butcvt(b)	(1 << ((b) - 1))
+
+#if 0
+static int buttondown(void)	/* report state of buttons, if any */
+{
+	if (!ecanmouse())	/* no event pending */
+		return 0;
+	mouse = emouse();	/* something, but it could be motion */
+	return mouse.buttons & 7;
+}
+#endif
+
+int waitdown(void)	/* wait until some button is down */
+{
+	while (!(mouse.buttons & 7))
+		mouse = emouse();
+	return mouse.buttons & 7;
+}
+
+int waitup(void)
+{
+	while (mouse.buttons & 7)
+		mouse = emouse();
+	return mouse.buttons & 7;
+}
+
+char *m3[]	= { "next", "prev", "page n", "again", "bigger", "smaller", "pan", "quit?", 0 };
+char *m2[]	= { 0 };
+
+enum { Next = 0, Prev, Page, Again, Bigger, Smaller, Pan, Quit };
+
+Menu	mbut3	= { m3, 0, 0 };
+Menu	mbut2	= { m2, 0, 0 };
+
+int	last_hit;
+int	last_but;
+
+char *pan(void)
+{
+	Point dd, xy, lastxy, min, max;
+
+	esetcursor(&blot);
+	waitdown();
+	xy = mouse.xy;
+	do{
+		lastxy = mouse.xy;
+		mouse = emouse();
+		dd = subpt(mouse.xy, lastxy);
+		min = addpt(screen->clipr.min, dd);
+		max = addpt(screen->clipr.max, dd);
+		draw(screen, rectaddpt(screen->r, subpt(mouse.xy, lastxy)),
+			screen, nil, screen->r.min);
+		if(mouse.xy.x < lastxy.x)	/* moved left, clear right */
+			draw(screen, Rect(max.x, screen->r.min.y, screen->r.max.x, screen->r.max.y),
+				display->white, nil, ZP);
+		else	/* moved right, clear left*/
+			draw(screen, Rect(screen->r.min.x, screen->r.min.y, min.x, screen->r.max.y),
+				display->white, nil, ZP);
+		if(mouse.xy.y < lastxy.y)	/* moved up, clear down */
+			draw(screen, Rect(screen->r.min.x, max.y, screen->r.max.x, screen->r.max.y),
+				display->white, nil, ZP);
+		else		/* moved down, clear up */
+			draw(screen, Rect(screen->r.min.x, screen->r.min.y, screen->r.max.x, min.y),
+				display->white, nil, ZP);
+		flushimage(display, 1);
+	}while(mouse.buttons);
+
+	xyoffset = addpt(xyoffset, subpt(mouse.xy, xy));
+
+	esetcursor(0);
+	return "p";
+}
+
+static char *getmousestr(void)
+{
+	static char buf[20];
+
+	checkmouse();
+	if (last_but == 1)
+		return "p";	/* repaint after panning */
+	if (last_but == 2) {
+		return "c";
+	} else if (last_but == 3) {
+		switch (last_hit) {
+		case Next:
+			return "";
+		case Prev:
+			return "-1";
+		case Page:
+			screenprint("page? ");
+			return "c";
+		case Again:
+			return "p";
+		case Bigger:
+			sprint(buf, "m%g", mag * 1.1);
+			return buf;
+		case Smaller:
+			sprint(buf, "m%g", mag / 1.1);
+			return buf;
+		case Pan:
+			return pan();
+		case Quit:
+			return "q";
+		default:
+			return "c";
+		}
+	} else {		/* button 1 or bail out */
+		return "c";
+	}
+}
+
+static int
+checkmouse(void)	/* return button touched if any */
+{
+	int c, b;
+	char *p;
+	extern int confirm(int);
+
+	b = waitdown();
+	last_but = 0;
+	last_hit = -1;
+	c = 0;
+	if (button3(b)) {
+		last_hit = emenuhit(3, &mouse, &mbut3);
+		last_but = 3;
+	} else if (button2(b)) {
+		last_hit = emenuhit(2, &mouse, &mbut2);
+		last_but = 2;
+	} else {		/* button1() */
+		pan();
+		last_but = 1;
+	}
+	waitup();
+	if (last_but == 3 && last_hit >= 0) {
+		p = m3[last_hit];
+		c = p[strlen(p) - 1];
+	}
+	if (c == '?' && !confirm(last_but))
+		last_hit = -1;
+	return last_but;
+}
+
+Cursor deadmouse = {
+	{ 0, 0},	/* offset */
+	{ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+	  0x00, 0x00, 0x00, 0x0C, 0x00, 0x82, 0x04, 0x41,
+	  0xFF, 0xE1, 0x5F, 0xF1, 0x3F, 0xFE, 0x17, 0xF0,
+	  0x03, 0xE0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, },
+	{ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
+	  0x00, 0x00, 0x00, 0x0C, 0x00, 0x82, 0x04, 0x41,
+	  0xFF, 0xE1, 0x5F, 0xF1, 0x3F, 0xFE, 0x17, 0xF0,
+	  0x03, 0xE0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, }
+};
+
+Cursor blot ={
+	{ 0, 0 },
+	{ 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
+	  0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
+	  0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
+	  0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, },
+	{ 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
+	  0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
+	  0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF,
+	  0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, 0xFF, }
+};
+
+Cursor skull ={
+	{ 0, 0 },
+	{ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xC0, 0x03,
+	  0xE7, 0xE7, 0x3F, 0xFC, 0x0F, 0xF0, 0x0D, 0xB0,
+	  0x07, 0xE0, 0x06, 0x60, 0x37, 0xEC, 0xE4, 0x27,
+	  0xC3, 0xC3, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, },
+	{ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xC0, 0x03,
+	  0xE7, 0xE7, 0x3F, 0xFC, 0x0F, 0xF0, 0x0D, 0xB0,
+	  0x07, 0xE0, 0x06, 0x60, 0x37, 0xEC, 0xE4, 0x27,
+	  0xC3, 0xC3, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, }
+};
+
+int
+confirm(int but)	/* ask for confirmation if menu item ends with '?' */
+{
+	int c;
+	static int but_cvt[8] = { 0, 1, 2, 0, 3, 0, 0, 0 };
+
+	esetcursor(&skull);
+	c = waitdown();
+	waitup();
+	esetcursor(0);
+	return but == but_cvt[c];
+}