leanprover-community / lean4-mode

Emacs major mode for Lean 4
https://leanprover.github.io/
Apache License 2.0
62 stars 27 forks source link

Some unicode symbols are displayed as squares #67

Open Yuhta opened 1 month ago

Yuhta commented 1 month ago

When I commented out lean4-mode, 𝕜 can be displayed without problem. However when I enable lean4-mode, 𝕜 becomes square with unicode value (01D55C) in it. There are other symbols also having this problem. This happens even I comment out everything in init.el and turn on lean4-mode only.

mekeor commented 1 month ago

@Yuhta, I suspect that the font you are using does not support the unicode character "mathematical double-struck small k" in bold weight (or in italics or so). Could you please move the point onto the character and type C-u C-x = (which is bound to what-cursor-position by default), and share the output with us? Here's an example output. We'd especially need the list of face-related text-properties as it is mentioned at the bottom of the output.

              position: 13836 of 13836 (100%), column: 2
            character: 𝕜 (displayed as 𝕜) (codepoint 120156, #o352534, #x1d55c)
              charset: unicode (Unicode (ISO10646))
code point in charset: 0x1D55C
               script: mathematical
               syntax: w    which means: word
             category: .:Base, L:Strong L2R
             to input: type "C-x 8 RET 1d55c" or "C-x 8 RET MATHEMATICAL DOUBLE-STRUCK SMALL K"
          buffer code: #xF0 #x9D #x95 #x9C
            file code: #xF0 #x9D #x95 #x9C (encoded by coding system utf-8-unix)
              display: by this font (glyph code):
    ftcrhb:-UKWN-Iosevka Fixed-regular-normal-normal-*-16-*-*-*-m-0-iso10646-1 (#xF5D)

Character code properties: customize what to show
  name: MATHEMATICAL DOUBLE-STRUCK SMALL K
  general-category: Ll (Letter, Lowercase)
  canonical-combining-class: 0 (Spacing, split, enclosing, reordrant, and Tibetan subjoined)
  bidi-class: L (Left-to-Right)
  decomposition: (font 107) (font 'k')
  mirrored: N
  bracket-type: n (Not a paired bracket character.)

There are text properties here:
  fontified            t
  rear-nonsticky       t

Additionally, it'd be useful to see active set of face-attributes defined for the mentioned face. If, for example, the face $FOO is mentioned as face, you could evaluate (face-all-attributes '$FOO) and share the output with us.

Yuhta commented 1 month ago

Here is the output of what-cursor-position when 𝕜 can be displayed (lean4-mode turned-off):

``` position: 898 of 5816 (15%), column: 9 character: 𝕜 (displayed as 𝕜) (codepoint 120156, #o352534, #x1d55c) charset: unicode (Unicode (ISO10646)) code point in charset: 0x1D55C script: mathematical syntax: w which means: word category: .:Base, L:Strong L2R to input: type "C-x 8 RET 1d55c" or "C-x 8 RET MATHEMATICAL DOUBLE-STRUCK SMALL K" buffer code: #xF0 #x9D #x95 #x9C file code: #xF0 #x9D #x95 #x9C (encoded by coding system utf-8-unix) display: by this font (glyph code): ftcrhb:-STIX-STIXGeneral-normal-normal-normal-*-17-*-*-*-*-0-iso10646-1 (#xA47) Character code properties: customize what to show name: MATHEMATICAL DOUBLE-STRUCK SMALL K general-category: Ll (Letter, Lowercase) decomposition: (font 107) (font 'k') ```

When 𝕜 cannot be displayed:

``` position: 898 of 5816 (15%), column: 9 character: 𝕜 (displayed as 𝕜) (codepoint 120156, #o352534, #x1d55c) charset: unicode (Unicode (ISO10646)) code point in charset: 0x1D55C script: mathematical syntax: w which means: word category: .:Base, L:Strong L2R to input: type "\bbk" with Lean input method buffer code: #xF0 #x9D #x95 #x9C file code: #xF0 #x9D #x95 #x9C (encoded by coding system utf-8-unix) display: no font available Character code properties: customize what to show name: MATHEMATICAL DOUBLE-STRUCK SMALL K general-category: Ll (Letter, Lowercase) decomposition: (font 107) (font 'k') There is an overlay here: From 898 to 900 face lsp-face-highlight-textual lsp-highlight t There are text properties here: face lsp-face-semhl-variable fontified t ```

Both (face-all-attributes 'lsp-face-highlight-textual) and (face-all-attributes 'lsp-face-semhl-variable) are:

((:family . unspecified) (:foundry . unspecified) (:width . unspecified) (:height . unspecified) (:weight . unspecified) (:slant . unspecified) (:underline . unspecified) (:overline . unspecified) (:extend . unspecified) (:strike-through . unspecified) (:box . unspecified) (:inverse-video . unspecified) (:foreground . unspecified) (:background . unspecified) (:stipple . unspecified) (:inherit . unspecified))