// 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

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;

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 Sun Mar 29 11:34:23 CEST 2015 from file DisplayManager.java
by the hlt.language.tools.Hilite Java tool written by Hassan Aït-Kaci