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?<div dir="auto"><br></div>