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

Makarius makarius at sketis.net
Sat Jan 16 15:41:03 CET 2016

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"

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>}}"})

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


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.


More information about the isabelle-dev mailing list