equal
deleted
inserted
replaced
76 case XML.Text(text) => |
76 case XML.Text(text) => |
77 Library.separate(FBreak, |
77 Library.separate(FBreak, |
78 Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString))) |
78 Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString))) |
79 } |
79 } |
80 |
80 |
81 private val default_margin = 76 |
81 private val margin_default = 76 |
82 |
82 |
83 def formatted(input: List[XML.Tree], margin: Int = default_margin): List[XML.Tree] = |
83 def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] = |
84 { |
84 { |
85 val breakgain = margin / 20 |
85 val breakgain = margin / 20 |
86 val emergencypos = margin / 2 |
86 val emergencypos = margin / 2 |
87 |
87 |
88 def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text = |
88 def format(trees: List[XML.Tree], blockin: Int, after: Int, text: Text): Text = |
113 case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s)) |
113 case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s)) |
114 } |
114 } |
115 format(input.flatMap(standard_format), 0, 0, Text()).content |
115 format(input.flatMap(standard_format), 0, 0, Text()).content |
116 } |
116 } |
117 |
117 |
118 def string_of(input: List[XML.Tree], margin: Int = default_margin): String = |
118 def string_of(input: List[XML.Tree], margin: Int = margin_default): String = |
119 formatted(input).iterator.flatMap(XML.content).mkString |
119 formatted(input).iterator.flatMap(XML.content).mkString |
120 |
120 |
121 |
121 |
122 /* unformatted output */ |
122 /* unformatted output */ |
123 |
123 |