3799 |
screensize = screen_size * 2; |
screensize = screen_size * 2; |
3800 |
faces[0] |
faces[0] |
3801 |
= lookup_derived_face (sf, intern ("msdos-menu-passive-face"), |
= lookup_derived_face (sf, intern ("msdos-menu-passive-face"), |
3802 |
0, DEFAULT_FACE_ID); |
0, DEFAULT_FACE_ID, 1); |
3803 |
faces[1] |
faces[1] |
3804 |
= lookup_derived_face (sf, intern ("msdos-menu-active-face"), |
= lookup_derived_face (sf, intern ("msdos-menu-active-face"), |
3805 |
0, DEFAULT_FACE_ID); |
0, DEFAULT_FACE_ID, 1); |
3806 |
selectface = intern ("msdos-menu-select-face"); |
selectface = intern ("msdos-menu-select-face"); |
3807 |
faces[2] = lookup_derived_face (sf, selectface, |
faces[2] = lookup_derived_face (sf, selectface, |
3808 |
0, faces[0]); |
0, faces[0], 1); |
3809 |
faces[3] = lookup_derived_face (sf, selectface, |
faces[3] = lookup_derived_face (sf, selectface, |
3810 |
0, faces[1]); |
0, faces[1], 1); |
3811 |
|
|
3812 |
/* Make sure the menu title is always displayed with |
/* Make sure the menu title is always displayed with |
3813 |
`msdos-menu-active-face', no matter where the mouse pointer is. */ |
`msdos-menu-active-face', no matter where the mouse pointer is. */ |