# Keys currently down, to be depressed if the pointer moves away
	private var down_names = new Set[String]