lib/browser/GraphBrowser/GraphView.java

 	TreeBrowser tb;
 	long timestamp;
 	Vertex highlighted = null;
 	Dimension size;
 	boolean parent_needs_layout;
+	Font font;
 
 	public void setTreeBrowser(TreeBrowser br) {
 		tb=br;
 	}
 

 
 	public Graph getGraph() { return gra; }
 
 	public Graph getOriginalGraph() { return gra2; }
 
-	public GraphView(Graph gr,GraphBrowser br) {
+	public GraphView(Graph gr, GraphBrowser br, Font f) {
 		gra2=gr;
 		browser=br;
 		gra=(Graph)(gra2.clone());
 		parent_needs_layout = true;
 		size = new Dimension(0, 0);
+		font = f;
 		addMouseListener(this);
 		addMouseMotionListener(this);
 	}
 
 	public void PS(String fname,boolean printable) throws IOException {

 	    gra3.layout(null);
 	    gra3.PS(fname,printable);
 	}
 
 	public void paint(Graphics g) {
+		g.setFont(font);
 		gra.draw(g);
 		if (highlighted!=null) highlighted.drawBox(g,Color.white);
 		size = new Dimension(gra.max_x-gra.min_x, gra.max_y-gra.min_y);
 		if (parent_needs_layout) {
 			parent_needs_layout = false;

 		int x = evt.getX() + gra.min_x;
 		int y = evt.getY() + gra.min_y;
 
 		Vertex v2=gra.vertexAt(x,y);
 		Graphics g=getGraphics();
+		g.setFont(font);
 		g.translate(-gra.min_x,-gra.min_y);
 		if (highlighted!=null) {
 			highlighted.drawBox(g,Color.lightGray);
 			highlighted=null;
 		}

 		collapseNodes();
 		relayout();
 	}
 
 	public void relayout() {
+		Graphics g = getGraphics();
+		g.setFont(font);
 		browser.showWaitMessage();
 		highlighted=null;
-		gra.layout(getGraphics());
+		gra.layout(g);
 		v=null;
 		parent_needs_layout = true;
-		update(getGraphics());
+		update(g);
 		browser.showReadyMessage();
 	}
 
 	public void focusToVertex(int n) {
 		Vertex vx=gra.getVertexByNum(n);

 				Math.max(0,x-vpsize.width/2));
 			int offset_y = Math.min(scrollp.getVAdjustable().getMaximum(),
 				Math.max(0,y-vpsize.height/2));
 
 			Graphics g=getGraphics();
+			g.setFont(font);
 			g.translate(-gra.min_x,-gra.min_y);
 			if (highlighted!=null) highlighted.drawBox(g,Color.lightGray);
 			vx.drawBox(g,Color.white);
 			highlighted=vx;
 			scrollp.setScrollPosition(offset_x, offset_y);

 		}
 	}
 
 	public void mouseExited(MouseEvent evt) {
 		Graphics g=getGraphics();
+		g.setFont(font);
 		g.translate(-gra.min_x,-gra.min_y);
 		if (highlighted!=null) {
 			highlighted.drawBox(g,Color.lightGray);
 			highlighted=null;
 		}