Re: [GITGRUB] New menu interface (implementation)

[Michal Suchanek]

2009/10/7 Bean <address@hidden>:
> On Wed, Oct 7, 2009 at 6:16 AM, Michal Suchanek <address@hidden> wrote:
>> 2009/10/6 Bean <address@hidden>:
>>> On Tue, Oct 6, 2009 at 11:18 PM, Michal Suchanek <address@hidden> wrote:
>>
>>>>
>>>> I think there are these common uses for borders:
>>>>
>>>> - line border in graphics, box drawing char border in text
>>>>  This is the simplest case which does not require any support media.
>>>>  This should be well supported so that creating layout that just
>>>> works is easy (think fixing grub configuration, posting on pastebin,
>>>> etc)
>>>
>>> Yes, you can archive it with this:
>>>
>>> top_left = ",,cyan/blue,#0x250F:,,green/blue,#0x2554"
>>
>> This gives box drawing characters in both graphics and text. Perhaps
>> this is an acceptable solution for single border but I would like this
>> to be the default grub configuration when no theme is applied and
>> having a distinct more precise border in graphics mode would be a
>> bonus.
>>
>> The extend alignment does not seem to work quite well, nor does
>> setting absolute size and margins (which is slightly more ugly).
>
> Hi,
>
> The extend attribute extends  in the orthogonal direction, for example
>
> screen
> {
>  direction = "left_to_right"
>  panel { width=50% id="aa"  valign=top }
>  panel { width=50% id="bb" valign=extend}
> }
>

This might make switching the direction of a panel more difficult but
there may be other issues. Either way the method with margin does not
work either.

Thanks

Mchal