src/Pure/Tools/debugger.scala
changeset 60880 fa958e24ff24
parent 60878 1f0d2bbcf38b
child 60882 45bfd18835f1
     1.1 --- a/src/Pure/Tools/debugger.scala	Mon Aug 10 19:17:49 2015 +0200
     1.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 20:22:49 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): (Boolean, State) =
     1.8 +    def toggle_breakpoint(breakpoint: 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 -      (active_breakpoints1(serial), copy(active_breakpoints = active_breakpoints1))
    1.14 +        if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
    1.15 +      else active_breakpoints + breakpoint
    1.16 +      (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
    1.17      }
    1.18  
    1.19      def set_focus(new_focus: Option[Position.T]): State =
    1.20 @@ -141,19 +141,23 @@
    1.21    def inc_active(): Unit = global_state.change(_.inc_active)
    1.22    def dec_active(): Unit = global_state.change(_.dec_active)
    1.23  
    1.24 -  def breakpoint_active(serial: Long): Option[Boolean] =
    1.25 +  def breakpoint_active(breakpoint: Long): Option[Boolean] =
    1.26    {
    1.27      val state = current_state()
    1.28 -    if (state.active > 0) Some(state.active_breakpoints(serial)) else None
    1.29 +    if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None
    1.30    }
    1.31  
    1.32 -  def toggle_breakpoint(serial: Long)
    1.33 +  def toggle_breakpoint(command: Command, breakpoint: Long)
    1.34    {
    1.35      global_state.change(state =>
    1.36      {
    1.37 -      val (b, state1) = state.toggle_breakpoint(serial)
    1.38 +      val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint)
    1.39        state1.session.protocol_command(
    1.40 -        "Debugger.breakpoint", Properties.Value.Long(serial), Properties.Value.Boolean(b))
    1.41 +        "Debugger.breakpoint",
    1.42 +        Symbol.encode(command.node_name.node),
    1.43 +        Document_ID(command.id),
    1.44 +        Properties.Value.Long(breakpoint),
    1.45 +        Properties.Value.Boolean(breakpoint_state))
    1.46        state1
    1.47      })
    1.48    }