# HG changeset patch
# User wenzelm
# Date 1450519154 -3600
# Node ID 931792ce2d83c789470dceb8e85b5146258e2f6a
# Parent  e2a9e46ac0fb2b7ac8f74e999a4a84f85a93ade1
preserve break indentation;

diff -r e2a9e46ac0fb -r 931792ce2d83 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Dec 17 17:32:01 2015 +0100
+++ b/src/Pure/General/pretty.ML	Sat Dec 19 10:59:14 2015 +0100
@@ -255,8 +255,9 @@
   | breakdist ([], after) = after;
 
 (*Search for the next break (at this or higher levels) and force it to occur.*)
+val forcebreak = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
 fun forcenext [] = []
-  | forcenext (Break _ :: es) = fbrk :: es
+  | forcenext ((e as Break _) :: es) = forcebreak e :: es
   | forcenext (e :: es) = e :: forcenext es;
 
 in