Moved font settings from Vertex to GraphView.

--- a/lib/browser/GraphBrowser/GraphView.java	Mon Oct 22 12:11:00 2001 +0200
+++ b/lib/browser/GraphBrowser/GraphView.java	Mon Oct 22 14:51:39 2001 +0200
@@ -28,6 +28,7 @@
 	Vertex highlighted = null;
 	Dimension size;
 	boolean parent_needs_layout;
+	Font font;
 
 	public void setTreeBrowser(TreeBrowser br) {
 		tb=br;
@@ -39,12 +40,13 @@
 
 	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);
 	}
@@ -56,6 +58,7 @@
 	}
 
 	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);
@@ -75,6 +78,7 @@
 
 		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);
@@ -140,12 +144,14 @@
 	}
 
 	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();
 	}
 
@@ -163,6 +169,7 @@
 				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);
@@ -253,6 +260,7 @@
 
 	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);

--- a/lib/browser/GraphBrowser/NormalVertex.java	Mon Oct 22 12:11:00 2001 +0200
+++ b/lib/browser/GraphBrowser/NormalVertex.java	Mon Oct 22 14:51:39 2001 +0200
@@ -2,7 +2,7 @@
   Title:      GraphBrowser/NormalVertex.java
   ID:         $Id$
   Author:     Stefan Berghofer, TU Muenchen
-  Copyright   1997  TU Muenchen
+  License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
   This class represents an ordinary vertex. It contains methods for
   drawing and PostScript output.
@@ -65,8 +65,7 @@
 	public int rightX() { return getX()+gra.box_width2; }
 
 	public void drawBox(Graphics g,Color boxColor) {
-		FontMetrics fm=g.getFontMetrics(font);
-		g.setFont(font);
+		FontMetrics fm = g.getFontMetrics(g.getFont());
 		int h=fm.getAscent()+fm.getDescent();
 
 		g.setColor(boxColor);

--- a/lib/browser/GraphBrowser/Vertex.java	Mon Oct 22 12:11:00 2001 +0200
+++ b/lib/browser/GraphBrowser/Vertex.java	Mon Oct 22 14:51:39 2001 +0200
@@ -2,7 +2,7 @@
   Title:      GraphBrowser/Vertex.java
   ID:         $Id$
   Author:     Stefan Berghofer, TU Muenchen
-  Copyright   1997  TU Muenchen
+  License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
   This class contains attributes and methods common to all kinds of
   vertices (e.g. coordinates, successors, predecessors).
@@ -15,8 +15,6 @@
 import java.io.*;
 
 abstract class Vertex {
-	protected static final Font font=new Font("Helvetica",Font.PLAIN,12);
-
 	Vector children=new Vector(10,10);
 	Vector parents=new Vector(10,10);
 	int degree=0;
@@ -70,7 +68,7 @@
 
 	public Dimension getLabelSize(Graphics g) {
 		FontMetrics fm = g == null ? 
-		    new DefaultFontMetrics(font) : g.getFontMetrics(font);
+		    new DefaultFontMetrics(12) : g.getFontMetrics(g.getFont());
 		
 		return new Dimension(
 		        Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),