equal
deleted
inserted
replaced
1 /*************************************************************************** |
1 /*************************************************************************** |
2 Title: GraphBrowser/GraphView.java |
2 Title: GraphBrowser/GraphView.java |
3 ID: $Id$ |
3 ID: $Id$ |
4 Author: Stefan Berghofer, TU Muenchen |
4 Author: Stefan Berghofer, TU Muenchen |
5 Copyright 1997 TU Muenchen |
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 |
6 |
7 This class defines the window in which the graph is displayed. It |
7 This class defines the window in which the graph is displayed. It |
8 contains methods for handling events such as collapsing / uncollapsing |
8 contains methods for handling events such as collapsing / uncollapsing |
9 nodes of the graph. |
9 nodes of the graph. |
10 ***************************************************************************/ |
10 ***************************************************************************/ |
48 addMouseListener(this); |
48 addMouseListener(this); |
49 addMouseMotionListener(this); |
49 addMouseMotionListener(this); |
50 } |
50 } |
51 |
51 |
52 public void PS(String fname,boolean printable) throws IOException { |
52 public void PS(String fname,boolean printable) throws IOException { |
53 gra.PS(fname,printable); |
53 Graph gra3 = (Graph)gra.clone(); |
|
54 gra3.layout(null); |
|
55 gra3.PS(fname,printable); |
54 } |
56 } |
55 |
57 |
56 public void paint(Graphics g) { |
58 public void paint(Graphics g) { |
57 gra.draw(g); |
59 gra.draw(g); |
58 if (highlighted!=null) highlighted.drawBox(g,Color.white); |
60 if (highlighted!=null) highlighted.drawBox(g,Color.white); |