1.1 --- a/src/Pure/PIDE/markup.scala	Mon Aug 10 20:25:04 2015 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Aug 10 20:42:59 2015 +0200
     1.3 @@ -264,7 +264,6 @@
     1.4    val ML_TYPING = "ML_typing"
     1.5  
     1.6    val ML_BREAKPOINT = "ML_breakpoint"
     1.7 -  val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
     1.8  
     1.9  
    1.10    /* outer syntax */

     2.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 10 20:25:04 2015 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 10 20:42:59 2015 +0200
     2.3 @@ -238,6 +238,18 @@
     2.4      !(is_result(msg) || is_tracing(msg) || is_state(msg))
     2.5  
     2.6  
     2.7 +  /* breakpoints */
     2.8 +
     2.9 +  object ML_Breakpoint
    2.10 +  {
    2.11 +    def unapply(tree: XML.Tree): Option[Long] =
    2.12 +    tree match {
    2.13 +      case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
    2.14 +      case _ => None
    2.15 +    }
    2.16 +  }
    2.17 +
    2.18 +
    2.19    /* dialogs */
    2.20  
    2.21    object Dialog_Args

     3.1 --- a/src/Pure/Tools/debugger.scala	Mon Aug 10 20:25:04 2015 +0200
     3.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 20:42:59 2015 +0200
     3.3 @@ -141,12 +141,15 @@
     3.4    def inc_active(): Unit = global_state.change(_.inc_active)
     3.5    def dec_active(): Unit = global_state.change(_.dec_active)
     3.6  
     3.7 -  def breakpoint_active(breakpoint: Long): Option[Boolean] =
     3.8 +  def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
     3.9    {
    3.10      val state = current_state()
    3.11      if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None
    3.12    }
    3.13  
    3.14 +  def breakpoint_state(breakpoint: Long): Boolean =
    3.15 +    current_state().active_breakpoints(breakpoint)
    3.16 +
    3.17    def toggle_breakpoint(command: Command, breakpoint: Long)
    3.18    {
    3.19      global_state.change(state =>

     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:25:04 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:42:59 2015 +0200
     4.3 @@ -155,7 +155,7 @@
     4.4      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
     4.5        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
     4.6        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     4.7 -      Markup.VAR, Markup.TFREE, Markup.TVAR)
     4.8 +      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT)
     4.9  
    4.10    private val hyperlink_elements =
    4.11      Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
    4.12 @@ -182,7 +182,7 @@
    4.13  
    4.14    private val tooltip_elements =
    4.15      Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    4.16 -      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
    4.17 +      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL) ++
    4.18      Markup.Elements(tooltip_descriptions.keySet)
    4.19  
    4.20    private val gutter_elements =
    4.21 @@ -348,9 +348,9 @@
    4.22      else
    4.23        snapshot.select(range, Rendering.breakpoint_elements, command_states =>
    4.24          {
    4.25 -          case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
    4.26 +          case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
    4.27              command_states match {
    4.28 -              case st :: _ => Some((st.command, serial))
    4.29 +              case st :: _ => Some((st.command, breakpoint))
    4.30                case _ => None
    4.31              }
    4.32            case _ => None
    4.33 @@ -539,6 +539,11 @@
    4.34              Some(add(prev, r, (true, pretty_typing("::", body))))
    4.35            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    4.36              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    4.37 +          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
    4.38 +            val text =
    4.39 +              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
    4.40 +              else "breakpoint (disabled)"
    4.41 +            Some(add(prev, r, (true, XML.Text(text))))
    4.42            case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
    4.43              Some(add(prev, r, (true, XML.Text("language: " + language))))
    4.44            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    4.45 @@ -675,9 +680,8 @@
    4.46                    Some((Nil, Some(bad_color)))
    4.47                  case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    4.48                    Some((Nil, Some(intensify_color)))
    4.49 -                case (_, Text.Info(_,
    4.50 -                    XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _))) =>
    4.51 -                  Debugger.breakpoint_active(serial).map(active =>
    4.52 +                case (_, Text.Info(_, Protocol.ML_Breakpoint(breakpoint))) =>
    4.53 +                  Debugger.active_breakpoint_state(breakpoint).map(active =>
    4.54                      (Nil, Some(if (active) breakpoint_active_color else breakpoint_color)))
    4.55                  case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
    4.56                    command_states.collectFirst(