WINDOW_BODY_IN_PIXELS 1045 src/window.c          : WINDOW_BODY_IN_PIXELS);
WINDOW_BODY_IN_PIXELS 2183 src/window.c       ? w->pixel_width : window_body_width (w, WINDOW_BODY_IN_PIXELS);
WINDOW_BODY_IN_PIXELS 3720 src/window.c   	    = window_body_width (w, WINDOW_BODY_IN_PIXELS);
WINDOW_BODY_IN_PIXELS 3722 src/window.c   	    = window_body_height (w, WINDOW_BODY_IN_PIXELS);
WINDOW_BODY_IN_PIXELS 3970 src/window.c   		 || (window_body_width (w, WINDOW_BODY_IN_PIXELS)
WINDOW_BODY_IN_PIXELS 3972 src/window.c   		 || (window_body_height (w, WINDOW_BODY_IN_PIXELS)
WINDOW_BODY_IN_PIXELS 4849 src/window.c   			- window_body_height (m, WINDOW_BODY_IN_PIXELS))
WINDOW_BODY_IN_PIXELS 5336 src/window.c     int old_height = window_body_height (w, WINDOW_BODY_IN_PIXELS);
WINDOW_BODY_IN_PIXELS 5370 src/window.c     int delta = (window_body_height (w, WINDOW_BODY_IN_PIXELS)