--- 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
--- 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()
}
--- 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
--- 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 =
--- 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 {
--- 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()