preserve break indentation;
authorwenzelm
Sat Dec 19 10:59:14 2015 +0100 (2015-12-19)
changeset 61863931792ce2d83
parent 61862 e2a9e46ac0fb
child 61864 3a5992c3410c
preserve break indentation;
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Thu Dec 17 17:32:01 2015 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Sat Dec 19 10:59:14 2015 +0100
     1.3 @@ -255,8 +255,9 @@
     1.4    | breakdist ([], after) = after;
     1.5  
     1.6  (*Search for the next break (at this or higher levels) and force it to occur.*)
     1.7 +val forcebreak = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
     1.8  fun forcenext [] = []
     1.9 -  | forcenext (Break _ :: es) = fbrk :: es
    1.10 +  | forcenext ((e as Break _) :: es) = forcebreak e :: es
    1.11    | forcenext (e :: es) = e :: forcenext es;
    1.12  
    1.13  in