# HG changeset patch # User berghofe # Date 1003755099 -7200 # Node ID 4f24fd4dbcf5b8c88e5a33b5c1a055c373a1650f # Parent 0493188cff4240c2a020dfd81cf2e3e17f3c2cfb Moved font settings from Vertex to GraphView. diff -r 0493188cff42 -r 4f24fd4dbcf5 lib/browser/GraphBrowser/GraphView.java --- 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); diff -r 0493188cff42 -r 4f24fd4dbcf5 lib/browser/GraphBrowser/NormalVertex.java --- 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); diff -r 0493188cff42 -r 4f24fd4dbcf5 lib/browser/GraphBrowser/Vertex.java --- 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())),