116 |
116 |
117 fun length (Block (_, _, _, _, len)) = len |
117 fun length (Block (_, _, _, _, len)) = len |
118 | length (Break (_, wd, _)) = wd |
118 | length (Break (_, wd, _)) = wd |
119 | length (Str (_, len)) = len; |
119 | length (Str (_, len)) = len; |
120 |
120 |
121 fun body_length [] len = len |
121 fun make_block markup consistent indent body = |
122 | body_length (e :: es) len = body_length es (length e + len); |
122 let |
123 |
123 fun body_length prts len = |
124 fun make_block m consistent indent es = Block (m, consistent, indent, es, body_length es 0); |
124 let |
125 fun markup_block m indent es = make_block (Markup.output m) false indent es; |
125 val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts; |
|
126 val len' = Int.max (fold (Integer.add o length) line 0, len); |
|
127 in |
|
128 (case rest of |
|
129 Break (true, _, ind) :: rest' => |
|
130 body_length (Break (false, indent + ind, 0) :: rest') len' |
|
131 | [] => len') |
|
132 end; |
|
133 in Block (markup, consistent, indent, body, body_length body 0) end; |
|
134 |
|
135 fun markup_block markup indent es = |
|
136 make_block (Markup.output markup) false indent es; |
126 |
137 |
127 |
138 |
128 |
139 |
129 (** derived operations to create formatting expressions **) |
140 (** derived operations to create formatting expressions **) |
130 |
141 |