[isabelle-dev] NEWS: mixfix annotations and Unicode
makarius at sketis.net
Sat Apr 2 00:23:25 CEST 2016
*** 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
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
A similar problem will show up again, if/when Unicode is supported in HOL
More information about the isabelle-dev