# HG changeset patch
# User wenzelm
# Date 1670512245 -3600
# Node ID aaedcdfa2154f746bff4edb906d8ee096766ccf4
# Parent  f10e6af0264fcdf179e74176998267ce66eecc62
tuned;

diff -r f10e6af0264f -r aaedcdfa2154 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Thu Dec 08 16:05:02 2022 +0100
+++ b/src/Pure/Tools/debugger.scala	Thu Dec 08 16:10:45 2022 +0100
@@ -26,8 +26,7 @@
     def thread_state: Option[Debug_State] = debug_states.headOption
 
     def stack_state: Option[Debug_State] =
-      if (1 <= index && index <= debug_states.length)
-        Some(debug_states(index - 1))
+      if (1 <= index && index <= debug_states.length) Some(debug_states(index - 1))
       else None
 
     def debug_index: Option[Int] =
@@ -165,24 +164,24 @@
 
   def is_active(): Boolean = session.is_ready && state.value.is_active
 
-  def ready(): Unit = {
-    if (is_active())
-      session.protocol_command("Debugger.init")
-  }
+  def ready(): Unit =
+    if (is_active()) session.protocol_command("Debugger.init")
 
   def init(): Unit =
     state.change { st =>
       val st1 = st.inc_active
-      if (session.is_ready && !st.is_active && st1.is_active)
+      if (session.is_ready && !st.is_active && st1.is_active) {
         session.protocol_command("Debugger.init")
+      }
       st1
     }
 
   def exit(): Unit =
     state.change { st =>
       val st1 = st.dec_active
-      if (session.is_ready && st.is_active && !st1.is_active)
+      if (session.is_ready && st.is_active && !st1.is_active) {
         session.protocol_command("Debugger.exit")
+      }
       st1
     }