--- 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(