# HG changeset patch # User wenzelm # Date 1488660446 -3600 # Node ID 70b0113fa4efab159fbf153e921e27e4343bcc41 # Parent a57794dbe0af5e7d64a597fb5b84c1a885274398 clarified pretty margin; diff -r a57794dbe0af -r 70b0113fa4ef src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Mar 04 21:04:44 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Sat Mar 04 21:47:26 2017 +0100 @@ -134,7 +134,6 @@ /* tooltips */ - def tooltip_margin: Int def timing_threshold: Double def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] = diff -r a57794dbe0af -r 70b0113fa4ef src/Tools/VSCode/etc/options --- a/src/Tools/VSCode/etc/options Sat Mar 04 21:04:44 2017 +0100 +++ b/src/Tools/VSCode/etc/options Sat Mar 04 21:47:26 2017 +0100 @@ -12,7 +12,7 @@ option vscode_tooltip_margin : int = 60 -- "margin for pretty-printing of tooltips" -option vscode_diagnostics_margin : int = 80 +option vscode_message_margin : int = 80 -- "margin for pretty-printing of diagnostic messages" option vscode_timing_threshold : real = 0.1 diff -r a57794dbe0af -r 70b0113fa4ef src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sat Mar 04 21:04:44 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sat Mar 04 21:47:26 2017 +0100 @@ -300,8 +300,7 @@ val doc = rendering.model.content.doc val range = doc.range(info.range) val contents = - info.info.map(tree => - Protocol.MarkedString(resources.output_pretty(List(tree), rendering.tooltip_margin))) + info.info.map(t => Protocol.MarkedString(resources.output_pretty_tooltip(List(t)))) (range, contents) } channel.write(Protocol.Hover.reply(id, result)) diff -r a57794dbe0af -r 70b0113fa4ef src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 21:04:44 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Mar 04 21:47:26 2017 +0100 @@ -93,8 +93,6 @@ case _ => None }).filterNot(info => info.info.is_empty) - val diagnostics_margin = options.int("vscode_diagnostics_margin") - def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] = { (for { @@ -102,7 +100,7 @@ range = model.content.doc.range(text_range) (_, XML.Elem(Markup(name, _), body)) <- res.iterator } yield { - val message = resources.output_pretty(body, diagnostics_margin) + val message = resources.output_pretty_message(body) val severity = VSCode_Rendering.message_severity.get(name) Protocol.Diagnostic(range, message, severity = severity) }).toList @@ -144,8 +142,7 @@ yield { val range = model.content.doc.range(text_range) Protocol.DecorationOptions(range, - msgs.map(msg => - Protocol.MarkedString(resources.output_pretty(msg, diagnostics_margin)))) + msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg)))) } Protocol.Decoration(decoration.typ, content) } @@ -153,7 +150,6 @@ /* tooltips */ - def tooltip_margin: Int = options.int("vscode_tooltip_margin") def timing_threshold: Double = options.real("vscode_timing_threshold") diff -r a57794dbe0af -r 70b0113fa4ef src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sat Mar 04 21:04:44 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sat Mar 04 21:47:26 2017 +0100 @@ -259,13 +259,17 @@ /* output text */ def decode_text: Boolean = options.bool("vscode_unicode_symbols") + def tooltip_margin: Int = options.int("vscode_tooltip_margin") + def message_margin: Int = options.int("vscode_message_margin") def output_text(s: String): String = if (decode_text) Symbol.decode(s) else Symbol.encode(s) + def output_xml(xml: XML.Tree): String = + output_text(XML.content(xml)) + def output_pretty(body: XML.Body, margin: Int): String = output_text(Pretty.string_of(body, margin)) - - def output_xml(xml: XML.Tree): String = - output_text(XML.content(xml)) + def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) + def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) }