[isabelle-dev] NEWS: mixfix annotations and Unicode

[Makarius]

*** General ***

* Mixfix annotations support general block properties, with syntax
"(‹x=a y=b z …›". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
to "(‹indent=DIGITS›". The former notation "(00" for unbreakable blocks
is superseded by "(‹unbreabable›" --- rare INCOMPATIBILITY.


This refers to Isabelle/3c4e9a7937b1, which also contains more 
documentation.

The main use of block properties is to specify "consistent" or 
"unbreakable". General markup is still unclear: it might open 
possibilities for advanced PIDE (and LaTeX) output at some stage, but is 
presently somewhat speculative.


In Isabelle/288c309df28d I've added some markup reports for "Mixfix 
delimiter contains raw Unicode -- this is non-portable and unreliable".

Isabelle/4b8f08de2792 illustrates the scary consequences of true Unicode. 
Depending which browser is used to view that file, or whether 
Isabelle/jEdit has formal checking/markup on or off, the text rendering 
fluctuates between two states:

   * Unicode bidi conformance -- logical non-sense
   * Unicode bidi non-conformance -- logical sense

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.


 	Makarius