[isabelle] Isabelle2016-RC0: font size of diamond symbol

Dear Makarius,

While trying out Isabelle2016-RC0, I noticed that the symbol for \<diamond> is now typeset much larger than in Isabelle2015. Has this change been intentional? I use the diamond symbol a lot (for applicative functor syntax) and I found the smaller symbol much less invasive. (I feel it is also closer to the standard \diamond symbol in LaTeX.) I've attached a screenshot with both versions of Isabelle. (Ubuntu Linux 14.04, jEdit text font is IsabelleText at size 14).


Attachment: diamond.png
Description: PNG image

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.