# HG changeset patch
# User kleing
# Date 1052318335 -7200
# Node ID 689868b99bde9b61cf4c921d23359ea9900513d0
# Parent  9cdab3186c0bbd5ab82c2e891a61e957bd652797
eliminated dependencies on AWT for batch mode

diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/AWTFontMetrics.java
--- /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();
+  }
+}
diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/AbstractFontMetrics.java
--- /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();
+
+}
diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/Box.java
--- /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;
+  }
+}
diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/Console.java
--- /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]);
+		}
+	}
+}
+
diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/DefaultFontMetrics.java
--- 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;
+  }
 }
diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/Graph.java
--- 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);
 		}
diff -r 9cdab3186c0b -r 689868b99bde lib/browser/GraphBrowser/Vertex.java
--- 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 "";}