# HG changeset patch
# User wenzelm
# Date 1273183075 -7200
# Node ID 97d2780ad6f0deda2821af15a92f680ed049b3e8
# Parent  379f5b1e7f91772e8d527c52d3331b3cbdbf5bb7
uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;

diff -r 379f5b1e7f91 -r 97d2780ad6f0 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu May 06 23:52:20 2010 +0200
+++ b/src/Pure/General/pretty.ML	Thu May 06 23:57:55 2010 +0200
@@ -119,7 +119,7 @@
 val str = String o Output.output_width;
 
 fun brk wd = Break (false, wd);
-val fbrk = Break (true, 2);
+val fbrk = Break (true, 1);
 
 fun breaks prts = Library.separate (brk 1) prts;
 fun fbreaks prts = Library.separate fbrk prts;
@@ -256,7 +256,7 @@
 
 (*Search for the next break (at this or higher levels) and force it to occur.*)
 fun forcenext [] = []
-  | forcenext (Break _ :: es) = Break (true, 0) :: es
+  | forcenext (Break _ :: es) = fbrk :: es
   | forcenext (e :: es) = e :: forcenext es;
 
 (*es is list of expressions to print;
@@ -317,8 +317,7 @@
   let
     fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
       | fmt (String (s, _)) = Buffer.add s
-      | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
-      | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
+      | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
   in fmt (prune prt) Buffer.empty end;