[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces
From: |
Eli Zaretskii |
Subject: |
bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces |
Date: |
Wed, 05 Apr 2023 11:45:35 +0300 |
> From: Robert Pluim <rpluim@gmail.com>
> Date: Wed, 05 Apr 2023 09:38:32 +0200
>
>
> --begin--
> emacs -Q
> C-p C-p
> C-x 8 e + + + +
> C-u C-x =
> --end--
>
> Visually, this does the right thing: the ';' has its height increased,
> but the text properties look like this:
>
> face ((:height 1.1) font-lock-comment-delimiter-face
> :height 1.3310000000000004)
> fontified t
> rear-nonsticky t
>
> Thatʼs not a valid 'face property, unless Iʼm misreading (info
> "(elisp) Special Properties"), plus the ':height 1.331' bit is wrong,
> thatʼs (expt 1.1 3), not (expt 1.1 4). Yet it works, the height has
> been increased.
The first "+" doesn't increase the height, though.
> Is this a bug in our interpretation of 'face properties?
Face properties can be specified in many strange ways, and the fact
that some invalid specifications seem to "work" doesn't mean we have a
bug, it just means some invalid faces fall through the cracks.
> I can fix the code in `emoji-zoom-increase' to produce something like
>
> ((:height 1.4641000000000004) font-lock-comment-delimiter-face)
>
> instead
Please do, and thanks. We don't need to understand why some bug seems
to work, it is enough to fix the bug.
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Robert Pluim, 2023/04/05
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces,
Eli Zaretskii <=
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Robert Pluim, 2023/04/05
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Eli Zaretskii, 2023/04/05
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Robert Pluim, 2023/04/05
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Eli Zaretskii, 2023/04/05
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Robert Pluim, 2023/04/05
- bug#62675: 29.0.60; emoji-zoom-increase interacts badly with faces, Robert Pluim, 2023/04/06