3868 |
screensize = screen_size * 2; |
screensize = screen_size * 2; |
3869 |
faces[0] |
faces[0] |
3870 |
= lookup_derived_face (sf, intern ("msdos-menu-passive-face"), |
= lookup_derived_face (sf, intern ("msdos-menu-passive-face"), |
3871 |
0, DEFAULT_FACE_ID); |
DEFAULT_FACE_ID); |
3872 |
faces[1] |
faces[1] |
3873 |
= lookup_derived_face (sf, intern ("msdos-menu-active-face"), |
= lookup_derived_face (sf, intern ("msdos-menu-active-face"), |
3874 |
0, DEFAULT_FACE_ID); |
DEFAULT_FACE_ID); |
3875 |
selectface = intern ("msdos-menu-select-face"); |
selectface = intern ("msdos-menu-select-face"); |
3876 |
faces[2] = lookup_derived_face (sf, selectface, |
faces[2] = lookup_derived_face (sf, selectface, |
3877 |
0, faces[0]); |
faces[0]); |
3878 |
faces[3] = lookup_derived_face (sf, selectface, |
faces[3] = lookup_derived_face (sf, selectface, |
3879 |
0, faces[1]); |
faces[1]); |
3880 |
|
|
3881 |
/* Make sure the menu title is always displayed with |
/* Make sure the menu title is always displayed with |
3882 |
`msdos-menu-active-face', no matter where the mouse pointer is. */ |
`msdos-menu-active-face', no matter where the mouse pointer is. */ |