Enumeration pref_enum = taskToExamine.getPreferences();
Enumeration pref_enum; synchronized(taskToExamine) { pref_enum = taskToExamine.getPreferences(); }
  public Preference getPrefWithAspectType(Task taskToExamine, int aspect_type) {    Enumeration pref_enum = taskToExamine.getPreferences();    while (pref_enum.hasMoreElements()) {      Preference return_pref = (Preference)pref_enum.nextElement();      if (return_pref.getAspectType() == aspect_type)	return return_pref;    }        return null;  }