# 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)
 }