src/Pure/Tools/debugger.scala
changeset 60880 fa958e24ff24
parent 60878 1f0d2bbcf38b
child 60882 45bfd18835f1
equal deleted inserted replaced
60879:3dc649cfd512 60880:fa958e24ff24
    27       copy(session = new_session)
    27       copy(session = new_session)
    28 
    28 
    29     def inc_active: State = copy(active = active + 1)
    29     def inc_active: State = copy(active = active + 1)
    30     def dec_active: State = copy(active = active - 1)
    30     def dec_active: State = copy(active = active - 1)
    31 
    31 
    32     def toggle_breakpoint(serial: Long): (Boolean, State) =
    32     def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
    33     {
    33     {
    34       val active_breakpoints1 =
    34       val active_breakpoints1 =
    35         if (active_breakpoints(serial)) active_breakpoints - serial
    35         if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
    36       else active_breakpoints + serial
    36       else active_breakpoints + breakpoint
    37       (active_breakpoints1(serial), copy(active_breakpoints = active_breakpoints1))
    37       (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
    38     }
    38     }
    39 
    39 
    40     def set_focus(new_focus: Option[Position.T]): State =
    40     def set_focus(new_focus: Option[Position.T]): State =
    41       copy(focus = new_focus)
    41       copy(focus = new_focus)
    42 
    42 
   139 
   139 
   140   def is_active(): Boolean = current_state().active > 0
   140   def is_active(): Boolean = current_state().active > 0
   141   def inc_active(): Unit = global_state.change(_.inc_active)
   141   def inc_active(): Unit = global_state.change(_.inc_active)
   142   def dec_active(): Unit = global_state.change(_.dec_active)
   142   def dec_active(): Unit = global_state.change(_.dec_active)
   143 
   143 
   144   def breakpoint_active(serial: Long): Option[Boolean] =
   144   def breakpoint_active(breakpoint: Long): Option[Boolean] =
   145   {
   145   {
   146     val state = current_state()
   146     val state = current_state()
   147     if (state.active > 0) Some(state.active_breakpoints(serial)) else None
   147     if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None
   148   }
   148   }
   149 
   149 
   150   def toggle_breakpoint(serial: Long)
   150   def toggle_breakpoint(command: Command, breakpoint: Long)
   151   {
   151   {
   152     global_state.change(state =>
   152     global_state.change(state =>
   153     {
   153     {
   154       val (b, state1) = state.toggle_breakpoint(serial)
   154       val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint)
   155       state1.session.protocol_command(
   155       state1.session.protocol_command(
   156         "Debugger.breakpoint", Properties.Value.Long(serial), Properties.Value.Boolean(b))
   156         "Debugger.breakpoint",
       
   157         Symbol.encode(command.node_name.node),
       
   158         Document_ID(command.id),
       
   159         Properties.Value.Long(breakpoint),
       
   160         Properties.Value.Boolean(breakpoint_state))
   157       state1
   161       state1
   158     })
   162     })
   159   }
   163   }
   160 
   164 
   161   def focus(new_focus: Option[Position.T]): Boolean =
   165   def focus(new_focus: Option[Position.T]): Boolean =