# HG changeset patch
# User wenzelm
# Date 1439215541 -7200
# Node ID 52edced9cce584452d9502788debbf47b9f1ab23
# Parent  ee23c1d21ac337c118009f257c315be5c68744d1
rendering for debugger/breakpoint active state;

diff -r ee23c1d21ac3 -r 52edced9cce5 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Aug 10 14:14:49 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 16:05:41 2015 +0200
@@ -17,6 +17,8 @@
 
   sealed case class State(
     session: Session = new Session(Resources.empty),
+    active: Int = 0,
+    active_breakpoints: Set[Long] = Set.empty,
     focus: Option[Position.T] = None,  // position of active GUI component
     threads: Map[String, List[Debug_State]] = Map.empty,  // thread name ~> stack of debug states
     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
@@ -24,6 +26,17 @@
     def set_session(new_session: Session): State =
       copy(session = new_session)
 
+    def inc_active: State = copy(active = active + 1)
+    def dec_active: State = copy(active = active - 1)
+
+    def toggle_breakpoint(serial: Long): State =
+    {
+      val active_breakpoints1 =
+        if (active_breakpoints(serial)) active_breakpoints - serial
+      else active_breakpoints + serial
+      copy(active_breakpoints = active_breakpoints1)
+    }
+
     def set_focus(new_focus: Option[Position.T]): State =
       copy(focus = new_focus)
 
@@ -124,6 +137,19 @@
     current_state().session.protocol_command("Debugger.init")
   }
 
+  def is_active(): Boolean = current_state().active > 0
+  def inc_active(): Unit = global_state.change(_.inc_active)
+  def dec_active(): Unit = global_state.change(_.dec_active)
+
+  def breakpoint_active(serial: Long): Option[Boolean] =
+  {
+    val state = current_state()
+    if (state.active > 0) Some(state.active_breakpoints(serial)) else None
+  }
+
+  def toggle_breakpoint(serial: Long): Unit =
+    global_state.change(_.toggle_breakpoint(serial))
+
   def focus(new_focus: Option[Position.T]): Boolean =
     global_state.change_result(state => (state.focus != new_focus, state.set_focus(new_focus)))
 
diff -r ee23c1d21ac3 -r 52edced9cce5 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Aug 10 14:14:49 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Aug 10 16:05:41 2015 +0200
@@ -100,6 +100,8 @@
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
+option breakpoint_color : string = "00CC0032"
+option breakpoint_active_color : string = "00CC0064"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
 option antiquote_color : string = "6600CCFF"
diff -r ee23c1d21ac3 -r 52edced9cce5 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:14:49 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 16:05:41 2015 +0200
@@ -325,7 +325,9 @@
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
     Debugger.init(PIDE.session)
+    Debugger.inc_active()
     handle_update()
+    jEdit.propertiesChanged()
   }
 
   override def exit()
@@ -334,6 +336,8 @@
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
     update_focus(None)
+    Debugger.dec_active()
+    jEdit.propertiesChanged()
   }
 
 
diff -r ee23c1d21ac3 -r 52edced9cce5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 14:14:49 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 16:05:41 2015 +0200
@@ -202,7 +202,7 @@
       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
-      Markup.BAD + Markup.INTENSIFY ++ active_elements
+      Markup.BAD + Markup.INTENSIFY + Markup.ML_BREAKPOINT ++ active_elements
 
   private val foreground_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
@@ -247,6 +247,8 @@
   val spell_checker_color = color_value("spell_checker_color")
   val bad_color = color_value("bad_color")
   val intensify_color = color_value("intensify_color")
+  val breakpoint_color = color_value("breakpoint_color")
+  val breakpoint_active_color = color_value("breakpoint_active_color")
   val quoted_color = color_value("quoted_color")
   val antiquoted_color = color_value("antiquoted_color")
   val antiquote_color = color_value("antiquote_color")
@@ -655,6 +657,10 @@
                   Some((Nil, Some(bad_color)))
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                   Some((Nil, Some(intensify_color)))
+                case (_, Text.Info(_,
+                    XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _))) =>
+                  Debugger.breakpoint_active(serial).map(active =>
+                    (Nil, Some(if (active) breakpoint_active_color else breakpoint_color)))
                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                   command_states.collectFirst(
                     { case st if st.results.defined(serial) => st.results.get(serial).get }) match