1    import javax.swing.*;
2    import java.awt.event.*;
3    import java.awt.*;
4    import java.util.*;
5    
6    public class PrefSize extends PrefDef {
7    
8      private static final long serialVersionUID = Version.getSUID();
9    
10     public TreeSet sizes;      //Legacy only. Do not use.
11     public Carto target;       //Legacy
12   
13     public PrefSize() {
14       name = name+"Sizes";
15       defname = "size";
16     }
17   
18     public PrefSize(Carto target) {
19       super(target);
20       name = "Sizes";         //don't use file name - it could change.
21       defname = "size";
22     }
23   
24     public Class getDefClass() {
25       return(Size.class);
26     }
27   
28     private void readObject(java.io.ObjectInputStream stream)
29         throws java.io.IOException,java.lang.ClassNotFoundException {
30       stream.defaultReadObject();
31       if (sizes!=null) mine=sizes;  //fix legacies from before PrefDef existed
32       if (target!=null) deftarget = target;
33     }
34   
35   }
36