pt.ua.gboard
Class GBoardInputHandler

java.lang.Object
  pt.ua.gboard.GBoardInputHandler

public abstract class GBoardInputHandler
extends java.lang.Object

This module implements input handling for GBoard.

An input handler class should inherit from this (abstract) class, call the constructor with the desired mask, and implement the run procedure. To activate input handler a pushInputHandler on the GBoard object is required.

invariant: validInputMask(mask())

This class follows DbC(tm) methodology. Where possible, contracts are implement with JML and native's Java assert.

Author:

Miguel Oliveira e Silva (mos@ua.pt)

Field Summary

static int	gboardClosingMask
static int	keyEventType
static int	keyPressedMask
static int	keyReleasedMask
static int	keyTypedMask
static int	maxMaskValue
static int	mouseClickedMask
static int	mouseEventType
static int	mousePressedMask
static int	mouseReleasedMask
static int	windowEventType

Constructor Summary

GBoardInputHandler(int mask)
Constructs a new GBoardInputHandler accepting the events defined by the mask.

Method Summary

boolean	activated(int event) Is current input handler object activated by event?
int	mask() The current mask value.
abstract void	run(GBoard board, int line, int column, int layer, int type, int code, Gelem gelem) Procedure to be automatically executed by GBoard when the input handler object is activated.
void	setMask(int mask) Defines a new input mask.
boolean	validEventType(int type)
static boolean	validInputMask(int mask) Checks if input mask is valid.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

keyPressedMask

public static final int keyPressedMask

See Also:

Constant Field Values

keyReleasedMask

public static final int keyReleasedMask

See Also:

Constant Field Values

keyTypedMask

public static final int keyTypedMask

See Also:

Constant Field Values

mousePressedMask

public static final int mousePressedMask

See Also:

Constant Field Values

mouseReleasedMask

public static final int mouseReleasedMask

See Also:

Constant Field Values

mouseClickedMask

public static final int mouseClickedMask

See Also:

Constant Field Values

gboardClosingMask

public static final int gboardClosingMask

See Also:

Constant Field Values

maxMaskValue

public static final int maxMaskValue

See Also:

Constant Field Values

keyEventType

public static final int keyEventType

See Also:

Constant Field Values

mouseEventType

public static final int mouseEventType

See Also:

Constant Field Values

windowEventType

public static final int windowEventType

See Also:

Constant Field Values

Constructor Detail

GBoardInputHandler

public GBoardInputHandler(int mask)

Constructs a new GBoardInputHandler accepting the events defined by the mask.

requires: validInputMask(mask)

ensures: mask() == mask

Parameters:

mask - the desired mask

Method Detail

validInputMask

public static boolean validInputMask(int mask)

Checks if input mask is valid.

Parameters:

mask - the mask

Returns:

boolean true if mask ok

validEventType

public boolean validEventType(int type)

mask

public int mask()

The current mask value.

Returns:

int mask

setMask

public void setMask(int mask)

Defines a new input mask.

requires: validInputMask(mask)

ensures: mask() == mask

Parameters:

mask - the new mask

activated

public boolean activated(int event)

Is current input handler object activated by event?

Parameters:

event - the event mask value

Returns:

boolean true if activated, false otherwise

run

public abstract void run(GBoard board,
                         int line,
                         int column,
                         int layer,
                         int type,
                         int code,
                         Gelem gelem)

Procedure to be automatically executed by GBoard when the input handler object is activated.

Parameters:

board - GBoard object

line - the line number

column - the column number

layer - the layer number

type - the event type (keyEventType or mouseEventType or windowEventType)

code - the event code (KeyEvent.getKeyCode() or MouseEvent.getButton() or WindowEvent.WINDOW_CLOSED)

gelem - object