--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/AWTFontMetrics.java Wed May 07 16:38:55 2003 +0200
@@ -0,0 +1,23 @@
+package GraphBrowser;
+
+import java.awt.FontMetrics;
+
+public class AWTFontMetrics implements AbstractFontMetrics {
+ private FontMetrics fontMetrics;
+
+ public AWTFontMetrics(FontMetrics m) {
+ fontMetrics = m;
+ }
+
+ public int stringWidth(String str) {
+ return fontMetrics.stringWidth(str);
+ }
+
+ public int getAscent() {
+ return fontMetrics.getAscent();
+ }
+
+ public int getDescent() {
+ return fontMetrics.getDescent();
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/AbstractFontMetrics.java Wed May 07 16:38:55 2003 +0200
@@ -0,0 +1,9 @@
+package GraphBrowser;
+
+public interface AbstractFontMetrics {
+
+ public int stringWidth(String str);
+ public int getAscent();
+ public int getDescent();
+
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Box.java Wed May 07 16:38:55 2003 +0200
@@ -0,0 +1,13 @@
+// replacement for java.awt.Dimension
+
+package GraphBrowser;
+
+public class Box {
+ public int width;
+ public int height;
+
+ public Box(int w, int h) {
+ this.width = w;
+ this.height = h;
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/browser/GraphBrowser/Console.java Wed May 07 16:38:55 2003 +0200
@@ -0,0 +1,79 @@
+/***************************************************************************
+ Title: GraphBrowser/Console.java
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
+
+ This is the graph browser's main class when run as a console application.
+
+***************************************************************************/
+
+package GraphBrowser;
+
+import java.io.*;
+import java.util.*;
+import java.net.*;
+import awtUtilities.*;
+
+public class Console {
+ Graph g;
+ // TreeBrowser tb;
+ String gfname;
+
+ public Console(String name) {
+ gfname = name;
+ }
+
+ public void PS(String fname,boolean printable) throws IOException {
+ g.layout(null);
+ g.PS(fname,printable);
+ }
+
+ public void initBrowser(InputStream is) {
+ try {
+ TreeNode tn = new TreeNode("Root", "", -1, true);
+ g = new Graph(is, tn);
+
+ // gv = new GraphView(new Graph(is, tn), null, null);
+ // tb = new TreeBrowser(tn, gv, font);
+ // gv.setTreeBrowser(tb);
+ // Vector v = new Vector(10,10);
+ // tn.collapsedDirectories(v);
+ // gv.collapseDir(v);
+ } catch (IOException exn) {
+ System.err.println("\nI/O error while reading graph file.");
+ } catch (ParseError exn) {
+ System.err.println("\nParse error in graph file:");
+ System.err.println(exn.getMessage());
+ System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
+ }
+ }
+
+ public static void main(String[] args) {
+ try {
+ if (args.length <= 1) {
+ System.err.println("Graph and output file expected");
+ return;
+ }
+ Console console=new Console(args[0]);
+
+ InputStream is=new FileInputStream(args[0]);
+ console.initBrowser(is);
+ is.close();
+
+ try {
+ if (args[1].endsWith(".ps"))
+ console.PS(args[1], true);
+ else if (args[1].endsWith(".eps"))
+ console.PS(args[1], false);
+ else
+ System.err.println("Unknown file type: " + args[1]);
+ } catch (IOException exn) {
+ System.err.println("Unable to write file " + args[1]);
+ }
+ } catch (IOException exn) {
+ System.err.println("Can't open graph file "+args[0]);
+ }
+ }
+}
+
--- a/lib/browser/GraphBrowser/DefaultFontMetrics.java Wed May 07 14:53:35 2003 +0200
+++ b/lib/browser/GraphBrowser/DefaultFontMetrics.java Wed May 07 16:38:55 2003 +0200
@@ -10,11 +10,9 @@
package GraphBrowser;
-import java.awt.*;
+public class DefaultFontMetrics implements AbstractFontMetrics {
-public class DefaultFontMetrics extends FontMetrics
-{
- protected static int[] chars =
+ private static int[] chars =
{13, 13, 17, 27, 27, 43, 32, 11, 16, 16, 19, 28, 13, 28, 13, 13, 27,
27, 27, 27, 27, 27, 27, 27, 27, 27, 13, 13, 28, 28, 28, 27, 49, 32,
32, 35, 35, 32, 29, 37, 35, 13, 24, 32, 27, 40, 35, 37, 32, 37, 35,
@@ -22,30 +20,30 @@
27, 27, 13, 27, 27, 11, 11, 24, 11, 40, 27, 27, 27, 27, 16, 24, 13,
27, 24, 35, 24, 24, 24, 16, 12, 16, 28};
- int size;
-
- public DefaultFontMetrics(int size)
- { super(null); this.size = size; }
+ private int size;
- public int getLeading()
- { return 1; }
+ public DefaultFontMetrics(int size)
+ { this.size = size; }
- public int getAscent()
- { return (int)(Math.round(size * 46.0 / 48.0)); }
-
- public int getDescent()
- { return (int)(Math.round(size * 10.0 / 48.0)); }
+ public int getLeading()
+ { return 1; }
- public int charWidth(char c) {
- if (c < 32 || c > 126) { return 0; }
- else {
+ public int getAscent()
+ { return (int)(Math.round(size * 46.0 / 48.0)); }
+
+ public int getDescent()
+ { return (int)(Math.round(size * 10.0 / 48.0)); }
+
+ public int charWidth(char c) {
+ if (c < 32 || c > 126) { return 0; }
+ else {
return (int)(Math.round(chars[c - 32] * size / 48.0));
- }
}
-
- public int stringWidth(String s) {
- int l=0, i;
- for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
- return l;
- }
+ }
+
+ public int stringWidth(String s) {
+ int l=0, i;
+ for (i=0; i < s.length(); i++) { l += charWidth(s.charAt(i)); }
+ return l;
+ }
}
--- a/lib/browser/GraphBrowser/Graph.java Wed May 07 14:53:35 2003 +0200
+++ b/lib/browser/GraphBrowser/Graph.java Wed May 07 16:38:55 2003 +0200
@@ -195,7 +195,7 @@
h=w=Integer.MIN_VALUE;
while (e1.hasMoreElements()) {
- Dimension dim=((Vertex)(e1.nextElement())).getLabelSize(g);
+ Box dim=((Vertex)(e1.nextElement())).getLabelSize(g);
h=Math.max(h,dim.height);
w=Math.max(w,dim.width);
}
--- a/lib/browser/GraphBrowser/Vertex.java Wed May 07 14:53:35 2003 +0200
+++ b/lib/browser/GraphBrowser/Vertex.java Wed May 07 16:38:55 2003 +0200
@@ -66,13 +66,14 @@
public void setID(String s) {}
- public Dimension getLabelSize(Graphics g) {
- FontMetrics fm = g == null ?
- new DefaultFontMetrics(12) : g.getFontMetrics(g.getFont());
+ public Box getLabelSize(Graphics g) {
+ AbstractFontMetrics fm = g == null ?
+ (AbstractFontMetrics) new DefaultFontMetrics(12) :
+ (AbstractFontMetrics) new AWTFontMetrics(g.getFontMetrics(g.getFont()));
- return new Dimension(
- Math.max(fm.stringWidth("[. . . .]"),fm.stringWidth(getLabel())),
- fm.getAscent()+fm.getDescent());
+ return new Box(Math.max(fm.stringWidth("[. . . .]"),
+ fm.stringWidth(getLabel())),
+ fm.getAscent()+fm.getDescent());
}
public String getPath() { return "";}