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

[Makarius]

On Sat, 9 Jan 2016, Makarius wrote:

> 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;

It is indeed that change.  The difference can be seen in the PIDE output 
window with the following example:


theory Test
imports "~~/src/HOL/IMP/Collecting_Examples"
begin

ML \<open>
   val prt = (Syntax.pretty_term @{context}
   @{prop "step S27 (x ::= Plus (V x) (N 1) {{<x:=0>}};;
             x ::= Plus (V x) (N 2) {Q}) =
   x ::= Plus (V x) (N 1) {{<x:=3>, <x:=8>}};;
   x ::= Plus (V x) (N 2) {{<x:=2>}}"})
\<close>

ML_command \<open>Pretty.writeln prt\<close>

end


Changing the window size causes certain breaks.  The point of 
c0f34fe6aa61 is that already forced breaks (due to ";;") are counted as 
such.  So the optional break after "step S27" is not taken.

Before the change, a rather large window is required for that.

The miscalculation goes back to Sep-1993, when David Aspinall proposed to 
expose the Pretty.fbrk operation.  Before it was just auxiliary to the 
internal layout algorithm.

So it ended up in the bulky change c9ec452ff08f from 1993. More than 60000 
changesets later it hopefully works better now.


 	Makarius