diff -r d1535ba3b1ca -r d4eb94b46e83 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Wed May 01 12:30:53 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed May 01 12:34:53 2024 +0200
@@ -337,7 +337,7 @@
   def output_xml(xml: XML.Tree): String =
     output_text(XML.content(xml))
 
-  def output_pretty(body: XML.Body, margin: Int): String =
+  def output_pretty(body: XML.Body, margin: Double): String =
     output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
   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)