# HG changeset patch
# User wenzelm
# Date 1648756279 -7200
# Node ID 2cb2606ce0753549efdcbd6d6747ebe3d2fcc0b6
# Parent  4f6a6ba7387df4b80c59248343dc08767f5908f0
tuned: avoid problems with scala3;

diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Pure/Concurrent/delay.scala
--- a/src/Pure/Concurrent/delay.scala	Thu Mar 31 21:48:08 2022 +0200
+++ b/src/Pure/Concurrent/delay.scala	Thu Mar 31 21:51:19 2022 +0200
@@ -33,8 +33,7 @@
     }
   }
 
-  def invoke(): Unit = synchronized
-  {
+  def invoke(): Unit = synchronized {
     val new_run =
       running match {
         case Some(request) => if (first) false else { request.cancel(); true }
@@ -44,16 +43,14 @@
       running = Some(Event_Timer.request(Time.now() + delay)(run))
   }
 
-  def revoke(): Unit = synchronized
-  {
+  def revoke(): Unit = synchronized {
     running match {
       case Some(request) => request.cancel(); running = None
       case None =>
     }
   }
 
-  def postpone(alt_delay: Time): Unit = synchronized
-  {
+  def postpone(alt_delay: Time): Unit = synchronized {
     running match {
       case Some(request) =>
         val alt_time = Time.now() + alt_delay
diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Pure/Concurrent/isabelle_thread.scala	Thu Mar 31 21:48:08 2022 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala	Thu Mar 31 21:51:19 2022 +0200
@@ -148,22 +148,19 @@
   // synchronized, with concurrent changes
   private var interrupt_postponed: Boolean = false
 
-  def clear_interrupt: Boolean = synchronized
-  {
+  def clear_interrupt: Boolean = synchronized {
     val was_interrupted = isInterrupted || interrupt_postponed
     Exn.Interrupt.dispose()
     interrupt_postponed = false
     was_interrupted
   }
 
-  def raise_interrupt: Unit = synchronized
-  {
+  def raise_interrupt: Unit = synchronized {
     interrupt_postponed = false
     super.interrupt()
   }
 
-  def postpone_interrupt: Unit = synchronized
-  {
+  def postpone_interrupt: Unit = synchronized {
     interrupt_postponed = true
     Exn.Interrupt.dispose()
   }
diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Pure/GUI/wrap_panel.scala
--- a/src/Pure/GUI/wrap_panel.scala	Thu Mar 31 21:48:08 2022 +0200
+++ b/src/Pure/GUI/wrap_panel.scala	Thu Mar 31 21:51:19 2022 +0200
@@ -35,8 +35,7 @@
 
     private def layout_size(target: Container, preferred: Boolean): Dimension =
     {
-      target.getTreeLock.synchronized
-      {
+      target.getTreeLock.synchronized {
         val target_width =
           if (target.getSize.width == 0) Integer.MAX_VALUE
           else target.getSize.width
diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Thu Mar 31 21:48:08 2022 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Thu Mar 31 21:51:19 2022 +0200
@@ -80,27 +80,23 @@
     private var session: Session = null
     private var monitoring: Future[Unit] = Future.value(())
 
-    override def init(session: Session): Unit = synchronized
-    {
+    override def init(session: Session): Unit = synchronized {
       this.session = session
     }
 
-    override def exit(): Unit = synchronized
-    {
+    override def exit(): Unit = synchronized {
       session = null
       monitoring.cancel()
     }
 
-    private def consume(props: Properties.T): Unit = synchronized
-    {
+    private def consume(props: Properties.T): Unit = synchronized {
       if (session != null) {
         val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
         session.runtime_statistics.post(Session.Runtime_Statistics(props1))
       }
     }
 
-    private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
-    {
+    private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.ML_Statistics(pid, stats_dir) =>
           monitoring =
diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Thu Mar 31 21:48:08 2022 +0200
+++ b/src/Pure/System/scala.scala	Thu Mar 31 21:51:19 2022 +0200
@@ -202,15 +202,13 @@
     override def init(session: Session): Unit =
       synchronized { this.session = session }
 
-    override def exit(): Unit = synchronized
-    {
+    override def exit(): Unit = synchronized {
       for ((id, future) <- futures) cancel(id, future)
       futures = Map.empty
     }
 
     private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
-      synchronized
-      {
+      synchronized {
         if (futures.isDefinedAt(id)) {
           session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
           futures -= id
@@ -223,8 +221,7 @@
       result(id, Scala.Tag.INTERRUPT, Nil)
     }
 
-    private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
-    {
+    private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Invoke_Scala(name, id) =>
           def body: Unit =
@@ -243,8 +240,7 @@
       }
     }
 
-    private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
-    {
+    private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Cancel_Scala(id) =>
           futures.get(id) match {
diff -r 4f6a6ba7387d -r 2cb2606ce075 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 31 21:48:08 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 31 21:51:19 2022 +0200
@@ -606,8 +606,7 @@
         else Nil
       }
 
-    def edit(edits: List[Text.Edit]): Unit = synchronized
-    {
+    def edit(edits: List[Text.Edit]): Unit = synchronized {
       GUI_Thread.require {}
 
       reset_blob()