On Sat, 9 Jan 2016, Tobias Nipkow wrote:
One page in Concrete Semantics contains the following output that is a
pretty-printed HOL formula:
step S27
(x ::= Plus (V x) (N 1) {{}};;
x ::= Plus (V x) (N 2) {Q}) =
...
With db9996a84166 it prints like this:
step S27 (x ::= Plus (V x) (N 1) {{}};;
x ::= Plus (V x) (N 2) {Q}) =
...
While I welcome this change(!), it seems to go against formatting in, for
example, the Isabelle sources. Not an important point, just curious.
I am also curious. Are these sources easily accessible, so that I can
look more closely?
Guessing from a distance, it might be the following change:
changeset: 61880:c0f34fe6aa61
user:wenzelm
date:Mon Dec 21 13:39:45 2015 +0100
files: src/Pure/General/pretty.ML src/Pure/General/pretty.scala
src/Pure/library.scala
description:
clarified length of block with pre-existant forced breaks;
There were a number of related changes of fine points, either due to the
xsymbols vs. ASCII print mode update, or due to better unification with
the Poly/ML PP model. As a consequence of the latter we now also have
blocks with "consistent breaks", but that feature presently unused in
Isabelle syntax. The Poly/ML compiler requires that, e.g. for structures,
functors, signatures.
When changing such details after 20-30 years, there is always a danger
that something breaks elsewhere. So it is relevant to take another look.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
