[isabelle-dev] NEWS: mixfix annotations and Unicode

[Makarius]

On Sat, 2 Apr 2016, Makarius wrote:

> I am considering to force Isabelle/jEdit text into Unicode 
> non-conformance, to make logical sense.  Or we could disallow Unicode 
> notation altogether -- it is hardly ever used, apart from some exotic 
> demos.
>
> A similar problem will show up again, if/when Unicode is supported in 
> HOL string literals.

I have made bidirectional Unicode display a bit more robust in 
Isabelle/ce22e5c3d4ce. If this sufficient is unclear; the Unicode standard 
is vast and complex.

Details about bidirectional text display are in Annex #9: 
http://unicode.org/reports/tr9

Anybody wants to formalize this?


 	Makarius