gui_redo_mouse_highlight 3863 src/dispextern.h extern void gui_redo_mouse_highlight (Display_Info *);
gui_redo_mouse_highlight 5647 src/w32term.c  	      gui_redo_mouse_highlight (dpyinfo);
gui_redo_mouse_highlight 19802 src/xterm.c              gui_redo_mouse_highlight (dpyinfo);