equal
deleted
inserted
replaced
125 |
125 |
126 public boolean isEmpty() { |
126 public boolean isEmpty() { |
127 return tb==null; |
127 return tb==null; |
128 } |
128 } |
129 |
129 |
130 public void initBrowser(InputStream is) { |
130 public void initBrowser(InputStream is, boolean noAWT) { |
131 try { |
131 try { |
132 TreeNode tn=new TreeNode("Root","",-1,true); |
132 Font font = noAWT ? null : new Font("Helvetica", Font.PLAIN, 12); |
133 gv=new GraphView(new Graph(is,tn),this); |
133 TreeNode tn = new TreeNode("Root", "", -1, true); |
134 tb=new TreeBrowser(tn,gv); |
134 gv = new GraphView(new Graph(is, tn), this, font); |
|
135 tb = new TreeBrowser(tn, gv, font); |
135 gv.setTreeBrowser(tb); |
136 gv.setTreeBrowser(tb); |
136 Vector v = new Vector(10,10); |
137 Vector v = new Vector(10,10); |
137 tn.collapsedDirectories(v); |
138 tn.collapsedDirectories(v); |
138 gv.collapseDir(v); |
139 gv.collapseDir(v); |
139 |
140 |
173 public void init() { |
174 public void init() { |
174 isApplet=true; |
175 isApplet=true; |
175 gfname=getParameter("graphfile"); |
176 gfname=getParameter("graphfile"); |
176 try { |
177 try { |
177 InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream(); |
178 InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream(); |
178 initBrowser(is); |
179 initBrowser(is, false); |
179 is.close(); |
180 is.close(); |
180 } catch (MalformedURLException exn) { |
181 } catch (MalformedURLException exn) { |
181 System.err.println("Invalid URL: "+gfname); |
182 System.err.println("Invalid URL: "+gfname); |
182 } catch (IOException exn) { |
183 } catch (IOException exn) { |
183 System.err.println("I/O error while reading "+gfname+"."); |
184 System.err.println("I/O error while reading "+gfname+"."); |
188 isApplet=false; |
189 isApplet=false; |
189 try { |
190 try { |
190 GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : ""); |
191 GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : ""); |
191 if (args.length > 0) { |
192 if (args.length > 0) { |
192 InputStream is=new FileInputStream(args[0]); |
193 InputStream is=new FileInputStream(args[0]); |
193 gb.initBrowser(is); |
194 gb.initBrowser(is, args.length > 1); |
194 is.close(); |
195 is.close(); |
195 } |
196 } |
196 if (args.length > 1) { |
197 if (args.length > 1) { |
197 try { |
198 try { |
198 if (args[1].endsWith(".ps")) { |
199 if (args[1].endsWith(".ps")) |
199 gb.gv.PS(args[1], true); |
200 gb.gv.PS(args[1], true); |
200 } else if (args[1].endsWith(".eps")) { |
201 else if (args[1].endsWith(".eps")) |
201 gb.gv.PS(args[1], false); |
202 gb.gv.PS(args[1], false); |
202 } else { |
203 else |
203 System.err.println("Unknown file type: " + args[1]); |
204 System.err.println("Unknown file type: " + args[1]); |
204 } |
|
205 } catch (IOException exn) { |
205 } catch (IOException exn) { |
206 System.err.println("Unable to write file " + args[1]); |
206 System.err.println("Unable to write file " + args[1]); |
207 } |
207 } |
208 System.exit(0); |
|
209 } else { |
208 } else { |
210 f=new GraphBrowserFrame(gb); |
209 f=new GraphBrowserFrame(gb); |
211 f.setSize(700,500); |
210 f.setSize(700,500); |
212 f.show(); |
211 f.show(); |
213 } |
212 } |