src/Tools/VSCode/src/preview_panel.scala

--- a/src/Tools/VSCode/src/preview_panel.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Tools/VSCode/src/preview_panel.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -12,17 +12,14 @@
 import java.io.{File => JFile}
 
 
-class Preview_Panel(resources: VSCode_Resources)
-{
+class Preview_Panel(resources: VSCode_Resources) {
   private val pending = Synchronized(Map.empty[JFile, Int])
 
   def request(file: JFile, column: Int): Unit =
     pending.change(map => map + (file -> column))
 
-  def flush(channel: Channel): Boolean =
-  {
-    pending.change_result(map =>
-    {
+  def flush(channel: Channel): Boolean = {
+    pending.change_result(map => {
       val map1 =
         map.iterator.foldLeft(map) {
           case (m, (file, column)) =>