lib/browser/GraphBrowser/TreeBrowser.java

--- a/lib/browser/GraphBrowser/TreeBrowser.java	Mon Oct 22 14:51:39 2001 +0200
+++ b/lib/browser/GraphBrowser/TreeBrowser.java	Mon Oct 22 14:52:12 2001 +0200
@@ -2,7 +2,7 @@
   Title:      GraphBrowser/TreeBrowser.java
   ID:         $Id$
   Author:     Stefan Berghofer, TU Muenchen
-  Copyright   1997  TU Muenchen
+  License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
   This class defines the browser window which is used to display directory
   trees. It contains methods for handling events.
@@ -23,9 +23,10 @@
 	long timestamp;
 	Dimension size;
 	boolean parent_needs_layout;
+	Font font;
 
-	public TreeBrowser(TreeNode tn, GraphView gr) {
-		t=tn;gv=gr;
+	public TreeBrowser(TreeNode tn, GraphView gr, Font f) {
+		t = tn; gv = gr; font = f;
 		size = new Dimension(0, 0);
 		parent_needs_layout = true;
 		addMouseListener(this);
@@ -82,6 +83,7 @@
 
 	public void paint(Graphics g)
 	{
+		g.setFont(font);
 		Dimension d = t.draw(g,5,5,selected);
 		if (parent_needs_layout) {
 			size = new Dimension(5+d.width, 5+d.height);