equal
deleted
inserted
replaced
343 |
343 |
344 def output_xml(xml: XML.Tree): String = |
344 def output_xml(xml: XML.Tree): String = |
345 output_text(XML.content(xml)) |
345 output_text(XML.content(xml)) |
346 |
346 |
347 def output_pretty(body: XML.Body, margin: Int): String = |
347 def output_pretty(body: XML.Body, margin: Int): String = |
348 output_text(Pretty.string_of(body, margin = margin)) |
348 output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric)) |
349 def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) |
349 def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) |
350 def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) |
350 def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) |
351 |
351 |
352 |
352 |
353 /* caret handling */ |
353 /* caret handling */ |