# HG changeset patch
# User wenzelm
# Date 1439232179 -7200
# Node ID 45bfd18835f1ad028f224c0b01a6d20331463655
# Parent  91a9a439590383204e4ebf15ee1d8370f7b5e842
tuned signature;
more rendering;

diff -r 91a9a4395903 -r 45bfd18835f1 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Aug 10 20:25:04 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Aug 10 20:42:59 2015 +0200
@@ -264,7 +264,6 @@
   val ML_TYPING = "ML_typing"
 
   val ML_BREAKPOINT = "ML_breakpoint"
-  val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
 
 
   /* outer syntax */
diff -r 91a9a4395903 -r 45bfd18835f1 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Aug 10 20:25:04 2015 +0200
+++ b/src/Pure/PIDE/protocol.scala	Mon Aug 10 20:42:59 2015 +0200
@@ -238,6 +238,18 @@
     !(is_result(msg) || is_tracing(msg) || is_state(msg))
 
 
+  /* breakpoints */
+
+  object ML_Breakpoint
+  {
+    def unapply(tree: XML.Tree): Option[Long] =
+    tree match {
+      case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
+      case _ => None
+    }
+  }
+
+
   /* dialogs */
 
   object Dialog_Args
diff -r 91a9a4395903 -r 45bfd18835f1 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Mon Aug 10 20:25:04 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 20:42:59 2015 +0200
@@ -141,12 +141,15 @@
   def inc_active(): Unit = global_state.change(_.inc_active)
   def dec_active(): Unit = global_state.change(_.dec_active)
 
-  def breakpoint_active(breakpoint: Long): Option[Boolean] =
+  def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
   {
     val state = current_state()
     if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None
   }
 
+  def breakpoint_state(breakpoint: Long): Boolean =
+    current_state().active_breakpoints(breakpoint)
+
   def toggle_breakpoint(command: Command, breakpoint: Long)
   {
     global_state.change(state =>
diff -r 91a9a4395903 -r 45bfd18835f1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:25:04 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:42:59 2015 +0200
@@ -155,7 +155,7 @@
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
       Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
-      Markup.VAR, Markup.TFREE, Markup.TVAR)
+      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT)
 
   private val hyperlink_elements =
     Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
@@ -182,7 +182,7 @@
 
   private val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
-      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
+      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL) ++
     Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
@@ -348,9 +348,9 @@
     else
       snapshot.select(range, Rendering.breakpoint_elements, command_states =>
         {
-          case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
+          case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
             command_states match {
-              case st :: _ => Some((st.command, serial))
+              case st :: _ => Some((st.command, breakpoint))
               case _ => None
             }
           case _ => None
@@ -539,6 +539,11 @@
             Some(add(prev, r, (true, pretty_typing("::", body))))
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(add(prev, r, (false, pretty_typing("ML:", body))))
+          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
+            val text =
+              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
+              else "breakpoint (disabled)"
+            Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
             Some(add(prev, r, (true, XML.Text("language: " + language))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
@@ -675,9 +680,8 @@
                   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 =>
+                case (_, Text.Info(_, Protocol.ML_Breakpoint(breakpoint))) =>
+                  Debugger.active_breakpoint_state(breakpoint).map(active =>
                     (Nil, Some(if (active) breakpoint_active_color else breakpoint_color)))
                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                   command_states.collectFirst(