style "default" {
       fontset = "-*-helvetica-medium-r-normal--12-*-*-*-*-*-iso8859-1,\
		  -*-phaisarn-medium-r-normal--12-*-*-*-*-*-tis620.2533-0,\
		  -*-*-medium-r-normal--12-*-*-*-*-*-tis620.2533-1,\
		  -*-*-medium-r-normal--12-*-*-*-*-*-tis620.2529-0,\
		  -*-*-medium-r-normal--12-*-*-*-*-*-tis620.2529-1,\
		  -*-*-medium-r-normal--12-*-*-*-*-*-iso8859-11"
}
class "GtkWidget" style "default"