Group.java
Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022 package org.gecode.explorer.postscript;
00023
00024 import java.io.Writer;
00025 import java.io.IOException;
00026
00027 import java.util.ArrayList;
00028
00029 public class Group extends Path {
00030 private ArrayList<Path> ps;
00031
00032 public Group(ArrayList<Path> ps0) {
00033 ps = ps0;
00034 }
00035
00036 void emit(Writer out) throws IOException {
00037 for (Path p : ps) {
00038 p.emit(out);
00039 }
00040 }
00041
00042 BoundingBox bb() {
00043 BoundingBox b = new BoundingBox(100000,100000,0,0);
00044 for (Path p : ps) {
00045 b.merge(p.bb());
00046 }
00047 return b;
00048 }
00049 }