Email Gateway (Aug 22 2022 at 12:27): Email Gateway (Aug 22 2022 at 12:27):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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).
Best,
Andreas
diamond.png
Email Gateway (Aug 22 2022 at 12:29):From: Makarius <makarius@sketis.net>
On Fri, 8 Jan 2016, Andreas Lochbihler wrote:
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?
Yes, see
changeset: 62006:ebb03c0fa686
user: wenzelm
date: Thu Dec 31 12:20:10 2015 +0100
files: lib/fonts/IsabelleText.sfd lib/fonts/IsabelleTextBold.sfd
description:
proper diamond from lasy10;
"Proper" means the rendering of \<diamond> corresponds to \<box>, for
typical use in temporal logics. The traditional situation in
lib/texinputs/isabellesym.sty and its group "logic" in etc/symbols
supports this interpretation.
I use the diamond symbol a lot (for applicative functor syntax) and I
found the smaller symbol much less invasive.
There is a small diamond in the IsabelleText font as well. Historically
it was assigned to \<struct> but that has lost its purpose. So in
Isabelle/0046bacc5f5b, I have now added a newly interpreted symbol
\<diamondop> to use that glyph.
The very few applications that did use \<diamond> as infix operator are
already updated, notably in AFP/363fdbc2f28c.
Makarius
Last updated: Apr 25 2024 at 08:20 UTC