rendering for debugger/breakpoint active state;
authorwenzelm
Mon Aug 10 16:05:41 2015 +0200 (2015-08-10)
changeset 6087652edced9cce5
parent 60875 ee23c1d21ac3
child 60877 8d00ff5a052e
rendering for debugger/breakpoint active state;
src/Pure/Tools/debugger.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/Tools/debugger.scala	Mon Aug 10 14:14:49 2015 +0200
     1.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 16:05:41 2015 +0200
     1.3 @@ -17,6 +17,8 @@
     1.4  
     1.5    sealed case class State(
     1.6      session: Session = new Session(Resources.empty),
     1.7 +    active: Int = 0,
     1.8 +    active_breakpoints: Set[Long] = Set.empty,
     1.9      focus: Option[Position.T] = None,  // position of active GUI component
    1.10      threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
    1.11      output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    1.12 @@ -24,6 +26,17 @@
    1.13      def set_session(new_session: Session): State =
    1.14        copy(session = new_session)
    1.15  
    1.16 +    def inc_active: State = copy(active = active + 1)
    1.17 +    def dec_active: State = copy(active = active - 1)
    1.18 +
    1.19 +    def toggle_breakpoint(serial: Long): State =
    1.20 +    {
    1.21 +      val active_breakpoints1 =
    1.22 +        if (active_breakpoints(serial)) active_breakpoints - serial
    1.23 +      else active_breakpoints + serial
    1.24 +      copy(active_breakpoints = active_breakpoints1)
    1.25 +    }
    1.26 +
    1.27      def set_focus(new_focus: Option[Position.T]): State =
    1.28        copy(focus = new_focus)
    1.29  
    1.30 @@ -124,6 +137,19 @@
    1.31      current_state().session.protocol_command("Debugger.init")
    1.32    }
    1.33  
    1.34 +  def is_active(): Boolean = current_state().active > 0
    1.35 +  def inc_active(): Unit = global_state.change(_.inc_active)
    1.36 +  def dec_active(): Unit = global_state.change(_.dec_active)
    1.37 +
    1.38 +  def breakpoint_active(serial: Long): Option[Boolean] =
    1.39 +  {
    1.40 +    val state = current_state()
    1.41 +    if (state.active > 0) Some(state.active_breakpoints(serial)) else None
    1.42 +  }
    1.43 +
    1.44 +  def toggle_breakpoint(serial: Long): Unit =
    1.45 +    global_state.change(_.toggle_breakpoint(serial))
    1.46 +
    1.47    def focus(new_focus: Option[Position.T]): Boolean =
    1.48      global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
    1.49  
     2.1 --- a/src/Tools/jEdit/etc/options	Mon Aug 10 14:14:49 2015 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Mon Aug 10 16:05:41 2015 +0200
     2.3 @@ -100,6 +100,8 @@
     2.4  option spell_checker_color : string = "0000FFFF"
     2.5  option bad_color : string = "FF6A6A64"
     2.6  option intensify_color : string = "FFCC6664"
     2.7 +option breakpoint_color : string = "00CC0032"
     2.8 +option breakpoint_active_color : string = "00CC0064"
     2.9  option quoted_color : string = "8B8B8B19"
    2.10  option antiquoted_color : string = "FFC83219"
    2.11  option antiquote_color : string = "6600CCFF"
     3.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:14:49 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 16:05:41 2015 +0200
     3.3 @@ -325,7 +325,9 @@
     3.4      PIDE.session.global_options += main
     3.5      PIDE.session.debugger_updates += main
     3.6      Debugger.init(PIDE.session)
     3.7 +    Debugger.inc_active()
     3.8      handle_update()
     3.9 +    jEdit.propertiesChanged()
    3.10    }
    3.11  
    3.12    override def exit()
    3.13 @@ -334,6 +336,8 @@
    3.14      PIDE.session.debugger_updates -= main
    3.15      delay_resize.revoke()
    3.16      update_focus(None)
    3.17 +    Debugger.dec_active()
    3.18 +    jEdit.propertiesChanged()
    3.19    }
    3.20  
    3.21  
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 14:14:49 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 16:05:41 2015 +0200
     4.3 @@ -202,7 +202,7 @@
     4.4        Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
     4.5        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
     4.6        Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
     4.7 -      Markup.BAD + Markup.INTENSIFY ++ active_elements
     4.8 +      Markup.BAD + Markup.INTENSIFY + Markup.ML_BREAKPOINT ++ active_elements
     4.9  
    4.10    private val foreground_elements =
    4.11      Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    4.12 @@ -247,6 +247,8 @@
    4.13    val spell_checker_color = color_value("spell_checker_color")
    4.14    val bad_color = color_value("bad_color")
    4.15    val intensify_color = color_value("intensify_color")
    4.16 +  val breakpoint_color = color_value("breakpoint_color")
    4.17 +  val breakpoint_active_color = color_value("breakpoint_active_color")
    4.18    val quoted_color = color_value("quoted_color")
    4.19    val antiquoted_color = color_value("antiquoted_color")
    4.20    val antiquote_color = color_value("antiquote_color")
    4.21 @@ -655,6 +657,10 @@
    4.22                    Some((Nil, Some(bad_color)))
    4.23                  case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    4.24                    Some((Nil, Some(intensify_color)))
    4.25 +                case (_, Text.Info(_,
    4.26 +                    XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _))) =>
    4.27 +                  Debugger.breakpoint_active(serial).map(active =>
    4.28 +                    (Nil, Some(if (active) breakpoint_active_color else breakpoint_color)))
    4.29                  case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    4.30                    command_states.collectFirst(
    4.31                      { case st if st.results.defined(serial) => st.results.get(serial).get }) match