src/Pure/Tools/debugger.scala
changeset 60878 1f0d2bbcf38b
parent 60876 52edced9cce5
child 60880 fa958e24ff24
     1.1 --- a/src/Pure/Tools/debugger.scala	Mon Aug 10 16:14:50 2015 +0200
     1.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 17:49:36 2015 +0200
     1.3 @@ -29,12 +29,12 @@
     1.4      def inc_active: State = copy(active = active + 1)
     1.5      def dec_active: State = copy(active = active - 1)
     1.6  
     1.7 -    def toggle_breakpoint(serial: Long): State =
     1.8 +    def toggle_breakpoint(serial: Long): (Boolean, State) =
     1.9      {
    1.10        val active_breakpoints1 =
    1.11          if (active_breakpoints(serial)) active_breakpoints - serial
    1.12        else active_breakpoints + serial
    1.13 -      copy(active_breakpoints = active_breakpoints1)
    1.14 +      (active_breakpoints1(serial), copy(active_breakpoints = active_breakpoints1))
    1.15      }
    1.16  
    1.17      def set_focus(new_focus: Option[Position.T]): State =
    1.18 @@ -147,8 +147,16 @@
    1.19      if (state.active > 0) Some(state.active_breakpoints(serial)) else None
    1.20    }
    1.21  
    1.22 -  def toggle_breakpoint(serial: Long): Unit =
    1.23 -    global_state.change(_.toggle_breakpoint(serial))
    1.24 +  def toggle_breakpoint(serial: Long)
    1.25 +  {
    1.26 +    global_state.change(state =>
    1.27 +    {
    1.28 +      val (b, state1) = state.toggle_breakpoint(serial)
    1.29 +      state1.session.protocol_command(
    1.30 +        "Debugger.breakpoint", Properties.Value.Long(serial), Properties.Value.Boolean(b))
    1.31 +      state1
    1.32 +    })
    1.33 +  }
    1.34  
    1.35    def focus(new_focus: Option[Position.T]): Boolean =
    1.36      global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))