<div dir="auto">I changed those methods but still couldn’t get it to work. Now I see this is hardcoded in the VectorEngine plugin. Juan, could we make this configurable?</div><div> <div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 17 Oct 2022 at 04:23 Gerald Klix <<a href="mailto:cuis.01@klix.ch">cuis.01@klix.ch</a>> wrote: </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;padding-left:1ex;border-left-color:rgb(204,204,204)">On 16.10.22 22:54, Luciano Notarfrancesco wrote: > I don’t mean to change the current behavior. I just would like that the > user could easily choose the code points of the glyphs to be used for those > characters. Right now they are hardcoded in TTFFontReader and VectorEngine. > As a preference they would be more flexible, but I can just change those > methods in my image for now. I’m using all DejaVu Sans and the thick arrows > look nice. Yes, that was my initial impression; I even started to write an encouraging E-mail. Then I tried some other fonts and discovered that the fonts mentioned below do not have the necessary glyphs. Perhaps a dictionary that maps the font-name to code-point substitution mapping, would be a general solution. Actually we also have to look at the syntactic context ... Anyway, I like the thicker arrows that DejaVu provides and I am willing to help to find a solution. > > On Mon, 17 Oct 2022 at 03:38 Gerald Klix <<a href="mailto:cuis.01@klix.ch" target="_blank">cuis.01@klix.ch</a>> wrote: > >> Luciano, >> >> I see your problem, >> but these Characters only have glyphs in the >> DejaVu, JetBrainsMono, KiwiMaru and KurintoSans fonts. >> >> To make this work properly, we need some means >> to discover the aforementioned situation >> and switch back to the current behavior. >> >> >> Sorry and HTH, >> >> Gerald >> >> >> On 06.10.22 12:55, Luciano Notarfrancesco via Cuis-dev wrote: >>> What do you think about adding two preferences to set the unicode >>> characters to be used for displaying ^ and _? The problem I’m having is >>> that the arrows that we currently use are the same that are commonly used >>> in mathematics for morphisms, and the code gets a bit confusing in my >>> system, so I’d like to use the thick arrow 16r2B05 for _ and 16r2B06 for >> ^, >>> and to avoid annoying people who like the current arrows I think we could >>> make this a preference. Is this reasonable? >>> >>> >> > </blockquote></div></div>