tuned whitespace;

--- a/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 15:00:43 2024 +0100
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala	Sat Dec 07 16:03:05 2024 +0100
@@ -30,7 +30,7 @@
   private val delay_margin = Delay.last(resources.output_delay, channel.Error_Logger) {
     refresh(current_output)
   }
-  
+
   def update_margin(new_margin: Double): Unit = {
     margin = new_margin
     delay_margin.invoke()
@@ -88,4 +88,3 @@
     }
   }
 }
-