[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#38485: Customizing glyph widths
From: |
Clément Pit-Claudel |
Subject: |
bug#38485: Customizing glyph widths |
Date: |
Wed, 4 Dec 2019 15:53:43 -0500 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.2.1 |
On 2019-12-04 13:45, Eli Zaretskii wrote:
>> Cc: casouri@gmail.com, 38485@debbugs.gnu.org
>> From: Clément Pit-Claudel <cpitclaudel@gmail.com>
>> Date: Wed, 4 Dec 2019 13:14:19 -0500
>>
>>>> I'm thinking something like `:display-width 3' or maybe `display-width
>>>> "~~>"' (the former would mean "as wide as three spaces in the default
>>>> font"; the later, "as wide as `~~>' in the default font").
>>>> These properties would be applied by prettify-symbols-mode in addition to
>>>> composition.
>>>
>>> I don't understand why would prettify-symbols-mode want to do this via
>>> a text property, instead of via a buffer-local variable.
>>
>> Would this buffer-local variable be an alist mapping each character to the
>> desired width?
>
> No, it will simply make each prettified symbol take up the same width
> as the original characters of the symbol that were composed. Isn't
> that what everyone would want, and want for _all_ prettified symbols?
Probably not. In proof-general, we display 'forall' as ∀ and 'exists' as ∃.
In my own configuration I also change "Qed" to ■ "Defined" to □, and "Admitted"
to 😱. These shouldn't be widened, I think — especially not the last ones
(there is a case to be made for widening forall, since otherwise we might get
indentation issues, but in Coq Qed, Defined and Admitted don't introduce
indentation changes, so it's safe not to widen them.
Clément.
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/03
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/04
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths,
Clément Pit-Claudel <=
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/04
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/05
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: Customizing glyph widths, Eli Zaretskii, 2019/12/05
- bug#38485: Customizing glyph widths, Clément Pit-Claudel, 2019/12/05
- bug#38485: "prettified" symbols, Richard Stallman, 2019/12/05
- bug#38485: "prettified" symbols, Eli Zaretskii, 2019/12/06
- bug#38485: "prettified" symbols, Richard Stallman, 2019/12/06
- bug#38485: "prettified" symbols, Clément Pit-Claudel, 2019/12/06