253 | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after) |
253 | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after) |
254 | breakdist (String (_, len) :: es, after) = len + breakdist (es, after) |
254 | breakdist (String (_, len) :: es, after) = len + breakdist (es, after) |
255 | breakdist ([], after) = after; |
255 | breakdist ([], after) = after; |
256 |
256 |
257 (*Search for the next break (at this or higher levels) and force it to occur.*) |
257 (*Search for the next break (at this or higher levels) and force it to occur.*) |
|
258 val forcebreak = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e; |
258 fun forcenext [] = [] |
259 fun forcenext [] = [] |
259 | forcenext (Break _ :: es) = fbrk :: es |
260 | forcenext ((e as Break _) :: es) = forcebreak e :: es |
260 | forcenext (e :: es) = e :: forcenext es; |
261 | forcenext (e :: es) = e :: forcenext es; |
261 |
262 |
262 in |
263 in |
263 |
264 |
264 fun formatted margin input = |
265 fun formatted margin input = |