What happens when you run this program? Do you see the white brackets at either (10,10) or (10,60) in the resulting window?
#lang racket/gui (define (draw c dc) (send dc set-font (send the-font-list find-or-create-font 12 'default 'normal 'normal)) (send dc draw-text "\u27e6\u27e7" 10 10) (send dc set-font (send the-font-list find-or-create-font 12 "Liberation Sans" 'default 'normal 'normal)) (send dc draw-text "\u27e6\u27e7" 10 60)) (define f (new frame% [label ""] [width 100] [height 200])) (define c (new canvas% [parent f] [paint-callback draw])) (send f show #t) On Tue, Aug 18, 2015 at 2:37 PM, Paul van der Walt <paul.vanderw...@inria.fr> wrote: > Hi Robby, > > On 2015-08-18 at 19:29, quoth Robby Findler: >>> c) can i make the Unicode approach work? It seems like The Right Thing >>> To Do. Not super important though. >> >> You would need to install a font that has that glyph, I believe. Maybe >> the STIX fonts are good ones to try. > > Does the PDF creating gizmo use (La)TeX somehow? Because it seems that > my installation of TeXLive does include the STIX fonts. If this is not > what you mean, i'm a bit stuck. > > This command: > > $ pdffonts fn:different.pdf > name type encoding emb > sub uni > ------------------------------------ ----------------- ---------------- --- > --- --- > XJNGZG+LiberationSans TrueType WinAnsi yes > yes yes > GGUMUO+LiberationSerif TrueType WinAnsi yes > yes yes > CTRDJA+LiberationSerif-Italic TrueType WinAnsi yes > yes yes > DQYGAE+LiberationSerif CID TrueType Identity-H yes > yes yes > > Gives me the impression that Liberation is being used. If i fire up > LibreOffice and select Liberation Sans for example, ⟦⟧ renders > correctly. > > Sorry for being dense, but i'm not sure where to look to help myself. > > Thanks for the pointers! > > p. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
