# HG changeset patch
# User wenzelm
# Date 1439338860 -7200
# Node ID 7432d6bb4195bfefb9fc9cd8010c5d8a4c524234
# Parent  3852e87e9b8801216c0523b15db2ff30523121f5
clarified breakpoint rendering;

diff -r 3852e87e9b88 -r 7432d6bb4195 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Aug 12 02:20:06 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Aug 12 02:21:00 2015 +0200
@@ -12,6 +12,17 @@
 
 (* parse trees *)
 
+fun breakpoint_position loc =
+  let val pos = Position.reset_range (Exn_Properties.position_of loc) in
+    (case Position.offset_of pos of
+      NONE => pos
+    | SOME 1 => pos
+    | SOME j =>
+        Position.properties_of pos
+        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
+        |> Position.of_properties)
+  end;
+
 fun report_parse_tree redirect depth space parse_tree =
   let
     val is_visible =
@@ -90,7 +101,7 @@
       | breakpoints loc pt =
           (case ML_Parse_Tree.breakpoint pt of
             SOME b =>
-              let val pos = Position.reset_range (Exn_Properties.position_of loc) in
+              let val pos = breakpoint_position loc in
                 if is_reported pos then
                   let val id = serial ();
                   in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
diff -r 3852e87e9b88 -r 7432d6bb4195 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Aug 12 02:20:06 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Aug 12 02:21:00 2015 +0200
@@ -100,8 +100,8 @@
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
-option breakpoint_color : string = "00CC0014"
-option breakpoint_active_color : string = "00CC0032"
+option breakpoint_disabled_color : string = "00CC66FF"
+option breakpoint_enabled_color : string = "CC6600FF"
 option quoted_color : string = "8B8B8B19"
 option antiquoted_color : string = "FFC83219"
 option antiquote_color : string = "6600CCFF"
diff -r 3852e87e9b88 -r 7432d6bb4195 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 12 02:20:06 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 12 02:21:00 2015 +0200
@@ -204,14 +204,14 @@
       Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
       Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
       Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
-      Markup.BAD + Markup.INTENSIFY + Markup.ML_BREAKPOINT ++ active_elements
+      Markup.BAD + Markup.INTENSIFY ++ active_elements
 
   private val foreground_elements =
     Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.ANTIQUOTED)
 
   private val bullet_elements =
-    Markup.Elements(Markup.BULLET)
+    Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
 
   private val fold_depth_elements =
     Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
@@ -249,8 +249,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 breakpoint_disabled_color = color_value("breakpoint_disabled_color")
+  val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
   val quoted_color = color_value("quoted_color")
   val antiquoted_color = color_value("antiquoted_color")
   val antiquote_color = color_value("antiquote_color")
@@ -680,9 +680,6 @@
                   Some((Nil, Some(bad_color)))
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                   Some((Nil, Some(intensify_color)))
-                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(
                     { case st if st.results.defined(serial) => st.results.get(serial).get }) match
@@ -774,7 +771,13 @@
   /* virtual bullets */
 
   def bullet(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
+    snapshot.select(range, Rendering.bullet_elements, _ =>
+      {
+        case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
+          Debugger.active_breakpoint_state(breakpoint).map(b =>
+            if (b) breakpoint_enabled_color else breakpoint_disabled_color)
+        case _ => Some(bullet_color)
+      })
 
 
   /* text folds */
diff -r 3852e87e9b88 -r 7432d6bb4195 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Aug 12 02:20:06 2015 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Aug 12 02:21:00 2015 +0200
@@ -463,16 +463,6 @@
           if (line != -1) {
             val line_range = Text.Range(start(i), end(i) min buffer.getLength)
 
-            // bullet bar
-            for {
-              Text.Info(range, color) <- rendering.bullet(line_range)
-              r <- JEdit_Lib.gfx_range(text_area, range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
-                r.length - bullet_w, line_height - bullet_h)
-            }
-
             // text chunks
             val screen_line = first_line + i
             val chunks = text_area.getChunksOfScreenLine(screen_line)
@@ -486,6 +476,16 @@
                   screen_line, line, start(i), end(i), y + line_height * i)
               } finally { gfx.setClip(clip) }
             }
+
+            // bullet bar
+            for {
+              Text.Info(range, color) <- rendering.bullet(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
+                r.length - bullet_w, line_height - bullet_h)
+            }
           }
           y0 += line_height
         }