[isabelle-dev] Line breaks in pretty-printed output

[Makarius]

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 := 0>}};;
>  x ::= Plus (V x) (N 2) {Q}) =
> ...
>
> With db9996a84166 it prints like this:
>
> step S27 (x ::= Plus (V x) (N 1) {{<x := 0>}};;
>          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