indexing
	description: "Constants for the Application editor."
	date: "$Date$"
	id: "$Id$"
	revision: "$Revision$"

class APPLICATION_CONSTANTS

feature -- Integer constants

	Arrow_head_w: INTEGER is 6
	Arrow_head_h: INTEGER is 10
	Arrow_head_line_w: INTEGER is 1
	Arrow_thickness: INTEGER is 4
	State_circle_radius: INTEGER is 27
	Initial_state_line_thickness: INTEGER is 3
	Standard_thickness: INTEGER is 1
	Large_thickness: INTEGER is 3

end -- class APPLICATION_CONSTANTS