/* diajava.cc 02/09/2004 13.28.08 */
void diajava_lastmousestate (UISTATE&state);
void diajava_setlastmousestate (UISTATE&state);
const char *diajava_getextrareport (void);
/* _dict.cc 31/03/1998 10.44.48 */
/* guidump.cc 12/04/1998 08.06.28 */
/* guispy.cc 07/01/1998 00.04.42 */