# 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