[isabelle-dev] Script characters in words

[Makarius]

On 06/03/2024 15:01, Lawrence Paulson wrote:
> Thanks for the explanation. I guess you are saying this is outside of our 
> control.

It would mean to submit patches to the jEdit project. I did this for really 
important things in the past: it does work, but can take a long time.


> You do have to wonder how they did not introduce the entire script 
> alphabet at the same time.

The Unicode committee has always been a bit of a mess. I guess the problem is 
that US-centric mentality has tried to rule over the world's languages, with 
limited success.

In recent years, related to the STIX project, much of the mathematical 
repertoire from TeX/LaTeX has been added in a post-hoc fashion.


	Makarius