Class UserProperties

java.lang.Object
de.saar.chorus.domgraph.UserProperties

public class UserProperties extends Object
A class representing user-specific properties which are stored in a File ".utool" in the user's home directory. If there is no such file, all properties are initialized with a default value. If the file contains only some of the properties, the other properties are initialized with their default value. To add a new property type, 1) specify an enum with its name and default value in the PropertyNames 2) implement convenient / necessary getters and setters
Author:
Michaela Regneri
  • Constructor Details

    • UserProperties

      public UserProperties()
  • Method Details

    • saveProperties

      public static boolean saveProperties()
      If there have been changes, the properties are saved to the .utool file. TODO so far, "changes" mean the user has called one of the setters. perhaps one should be more precise here?
      Returns:
      true if updates have been stored; false if there went something wrong or there were no updates.
    • allowExperimentalCodecs

      public static boolean allowExperimentalCodecs()
      Returns:
      true if experimental codecs are integrated
    • getExampleDirectories

      public static List<String> getExampleDirectories()
      Returns:
      A List of the example directories represented as Strings.
    • setExampleDirectories

      public static void setExampleDirectories(String dirs)
      This changes all example directories to the path (or path list) specified in dirs. Multiple paths must be separated by the system specific path separator.
      Parameters:
      dirs -
    • addExampleDirectory

      public static void addExampleDirectory(String dir)
      This adds a single example directory to the current list of directories.
      Parameters:
      dir - the new directory
    • getDefaultInputCodec

      public static String getDefaultInputCodec()
      Returns:
      the name of the default input codec
    • setDefaultInputCodec

      public static void setDefaultInputCodec(String codec)
      This changes the current default input codec.
      Parameters:
      codec - the new default input codec
    • getDefaultOutputCodec

      public static String getDefaultOutputCodec()
      Returns:
      the name of the default output codec
    • setDefaultOutputCodec

      public static void setDefaultOutputCodec(String codec)
      This changes the current default output codec.
      Parameters:
      codec - the new default output codec
    • getWorkingDirectory

      public static String getWorkingDirectory()
      The "utool working directory" is the last directory checked manually for any kind of files. It is only used and changed in Ubench.
      Returns:
      the last directory in use
      See Also:
    • setWorkingDirectory

      public static void setWorkingDirectory(String dir)
      Indicates the last 'active' directory the user has accessed via Ubench.
      Parameters:
      dir - the last directory in use
      See Also:
      • Ubench#setLastPath()
    • getDefaults

      public static Properties getDefaults()
      Returns:
      A Properties object containing default values for all properties defined in PropertyNames