# HG changeset patch
# User wenzelm
# Date 1364506938 -3600
# Node ID 2b58d7b139d60de4309202de0ea3c428da023b0f
# Parent  acc4bd79e2e97d880bf6a9448c1398dfa747d21a
ghost bullet via markup, which is painted as bar under text (normally space);

diff -r acc4bd79e2e9 -r 2b58d7b139d6 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 28 22:42:18 2013 +0100
@@ -74,7 +74,7 @@
   val FBreak = XML.Text("\n")
 
   def item(body: XML.Body): XML.Tree =
-    Block(2, XML.Text(Symbol.decode("\\<bullet>") + " ") :: body)
+    Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
 
   val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
   def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
diff -r acc4bd79e2e9 -r 2b58d7b139d6 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Mar 28 22:42:18 2013 +0100
@@ -87,6 +87,7 @@
   val BREAK = "break"
 
   val ITEM = "item"
+  val BULLET = "bullet"
 
   val SEPARATOR = "separator"
 
diff -r acc4bd79e2e9 -r 2b58d7b139d6 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Tools/jEdit/etc/options	Thu Mar 28 22:42:18 2013 +0100
@@ -39,6 +39,7 @@
 option running_color : string = "610061FF"
 option running1_color : string = "61006164"
 option light_color : string = "F0F0F0FF"
+option bullet_color : string = "000000FF"
 option tooltip_color : string = "FFFFE9FF"
 option writeln_color : string = "C0C0C0FF"
 option warning_color : string = "FF8C00FF"
diff -r acc4bd79e2e9 -r 2b58d7b139d6 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Mar 28 22:42:18 2013 +0100
@@ -121,6 +121,7 @@
   val running_color = color_value("running_color")
   val running1_color = color_value("running1_color")
   val light_color = color_value("light_color")
+  val bullet_color = color_value("bullet_color")
   val tooltip_color = color_value("tooltip_color")
   val writeln_color = color_value("writeln_color")
   val warning_color = color_value("warning_color")
@@ -501,6 +502,13 @@
       })
 
 
+  def bullet(range: Text.Range): Stream[Text.Info[Color]] =
+    snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
+      })
+
+
   def foreground(range: Text.Range): Stream[Text.Info[Color]] =
     snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
       {
diff -r acc4bd79e2e9 -r 2b58d7b139d6 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 28 16:11:48 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 28 22:42:18 2013 +0100
@@ -243,7 +243,15 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
-        val ascent = text_area.getPainter.getFontMetrics.getAscent
+        val fm = text_area.getPainter.getFontMetrics
+
+        val (bullet_x, bullet_y, bullet_w, bullet_h) =
+        {
+          val w = fm.charWidth(' ')
+          val h = fm.getAscent
+          val b = (if (w >= 8) w / 2 else w - 2) max 1
+          ((w - b + 1) / 2, (h - b + 1) / 2, w - b, line_height - b)
+        }
 
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
@@ -285,6 +293,16 @@
               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
             }
 
+            // 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)
+            }
+
             // squiggly underline
             for {
               Text.Info(range, color) <- rendering.squiggly_underline(line_range)
@@ -292,7 +310,7 @@
             } {
               gfx.setColor(color)
               val x0 = (r.x / 2) * 2
-              val y0 = r.y + ascent + 1
+              val y0 = r.y + fm.getAscent + 1
               for (x1 <- Range(x0, x0 + r.length, 2)) {
                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
                 gfx.drawLine(x1, y1, x1 + 1, y1)