`DisplayManager.java`

    // FILE. . . . . /home/hak/hlt/src/hlt/osfv2/io/DisplayManager.java
    // EDIT BY . . . Hassan Ait-Kaci
    // ON MACHINE. . Hak-Laptop
    // STARTED ON. . Mon Sep 02 15:36:40 2013

Author: |  | Hassan Aït-Kaci
Copyright: |  | © by the author
Version: |  | Last modified on Tue Jan 21 08:07:49 2014 by hak

    package hlt.osf.io;

    import hlt.osf.base.Sort;

    import hlt.language.util.ArrayList;

    import java.util.HashSet;

    import java.io.PrintStream;
    import java.io.IOException;

This class defines a display manager that consists of a display device manager and a display form manager.

    public class DisplayManager
    {
      private DisplayDeviceManager _device;
      private DisplayFormManager _formatter;

      public DisplayManager ()
        {
          _device = new DisplayDeviceManager();
          _formatter = new DisplayFormManager();
        }

      public DisplayManager (DisplayDeviceManager device)
        {
          _device = device;
          _formatter = new DisplayFormManager();
        }

      public DisplayManager (DisplayFormManager formatter)
        {
          _device = new DisplayDeviceManager();
          _formatter = formatter;
        }

      public DisplayManager (DisplayDeviceManager device, DisplayFormManager formatter)
        {
          _device = device;
          _formatter = formatter;
        }

      public DisplayManager (DisplayFormManager formatter, DisplayDeviceManager device)
        {
          _device = device;
          _formatter = formatter;
        }

      public final DisplayDeviceManager displayDeviceManager ()
        {
          return _device;
        }

      public final DisplayFormManager displayFormManager ()
        {
          return _formatter;
        }

      public final DisplayManager setDisplayDeviceManager (DisplayDeviceManager device)
        {
          _device = device;
          return this;
        }

      public final DisplayManager setDisplayFormManager (DisplayFormManager formatter)
        {
          _formatter = formatter;
          return this;
        }

      public void setOutputStream (PrintStream stream)
        {
          _device.setOutputStream(stream);
        }

      public PrintStream getOutputStream ()
        {
          return _device.getOutputStream();
        }

      public void close ()
        {
          _device.close();
        }

      public void flush () throws IOException
        {
          _device.flush();
        }

      public void print (String string)
        {
          _device.print(string);
        }

      public void println ()
        {
          _device.println();
        }

      public void println (String string)
        {
          _device.println(string);
        }

      public String displayTopForm ()
        {
          return _formatter.displayTopForm();
        }

      public String displayBottomForm ()
        {
          return _formatter.displayBottomForm();
        }

      public String displaySortsForm (Sort[] sorts)
        {
          return _formatter.displaySortsForm(sorts);
        }

      public String displaySortsForm (ArrayList sorts)
        {
          return _formatter.displaySortsForm(sorts);
        }

      public String quotedDisplayForm (double x)
        {
          return _formatter.quotedDisplayForm(x);
        }

      public String unquotedDisplayForm (double x)
        {
          return _formatter.unquotedDisplayForm(x);
        }

      public String displayForm (double x)
        {
          return _formatter.quotedDisplayForm(x);
        }

      public DisplayFormManager clearTags ()
        {
          return _formatter.clearTags();
        }

    }

This file was generated on Tue Jan 21 09:56:10 CET 2014 from file `DisplayManager.java`
by the `hlt.language.tools.Hilite` Java tool written by Hassan Aït-Kaci