equal
deleted
inserted
replaced
136 g.fillPolygon(down_x,down_y,3); |
136 g.fillPolygon(down_x,down_y,3); |
137 } |
137 } |
138 g.setColor(Color.black); |
138 g.setColor(Color.black); |
139 } |
139 } |
140 |
140 |
141 public void PS(PrintStream p) { |
141 public void PS(PrintWriter p) { |
142 p.print(leftX()+" "+getY()+" "+gra.box_width+" "+ |
142 p.print(leftX()+" "+getY()+" "+gra.box_width+" "+ |
143 gra.box_height+" ("); |
143 gra.box_height+" ("); |
144 for (int i=0;i<label.length();i++) |
144 for (int i=0;i<label.length();i++) |
145 { |
145 { |
146 if (("()\\").indexOf(label.charAt(i))>=0) |
146 if (("()\\").indexOf(label.charAt(i))>=0) |