ghost bullet via markup, which is painted as bar under text (normally space);
authorwenzelm
Thu Mar 28 22:42:18 2013 +0100 (2013-03-28 ago)
changeset 515742b58d7b139d6
parent 51573 acc4bd79e2e9
child 51575 907efc894051
ghost bullet via markup, which is painted as bar under text (normally space);
src/Pure/General/pretty.scala
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/General/pretty.scala	Thu Mar 28 16:11:48 2013 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Thu Mar 28 22:42:18 2013 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4    val FBreak = XML.Text("\n")
     1.5  
     1.6    def item(body: XML.Body): XML.Tree =
     1.7 -    Block(2, XML.Text(Symbol.decode("\\<bullet>") + " ") :: body)
     1.8 +    Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
     1.9  
    1.10    val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
    1.11    def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
     2.1 --- a/src/Pure/PIDE/markup.scala	Thu Mar 28 16:11:48 2013 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Thu Mar 28 22:42:18 2013 +0100
     2.3 @@ -87,6 +87,7 @@
     2.4    val BREAK = "break"
     2.5  
     2.6    val ITEM = "item"
     2.7 +  val BULLET = "bullet"
     2.8  
     2.9    val SEPARATOR = "separator"
    2.10  
     3.1 --- a/src/Tools/jEdit/etc/options	Thu Mar 28 16:11:48 2013 +0100
     3.2 +++ b/src/Tools/jEdit/etc/options	Thu Mar 28 22:42:18 2013 +0100
     3.3 @@ -39,6 +39,7 @@
     3.4  option running_color : string = "610061FF"
     3.5  option running1_color : string = "61006164"
     3.6  option light_color : string = "F0F0F0FF"
     3.7 +option bullet_color : string = "000000FF"
     3.8  option tooltip_color : string = "FFFFE9FF"
     3.9  option writeln_color : string = "C0C0C0FF"
    3.10  option warning_color : string = "FF8C00FF"
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Mar 28 16:11:48 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Mar 28 22:42:18 2013 +0100
     4.3 @@ -121,6 +121,7 @@
     4.4    val running_color = color_value("running_color")
     4.5    val running1_color = color_value("running1_color")
     4.6    val light_color = color_value("light_color")
     4.7 +  val bullet_color = color_value("bullet_color")
     4.8    val tooltip_color = color_value("tooltip_color")
     4.9    val writeln_color = color_value("writeln_color")
    4.10    val warning_color = color_value("warning_color")
    4.11 @@ -501,6 +502,13 @@
    4.12        })
    4.13  
    4.14  
    4.15 +  def bullet(range: Text.Range): Stream[Text.Info[Color]] =
    4.16 +    snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
    4.17 +      {
    4.18 +        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
    4.19 +      })
    4.20 +
    4.21 +
    4.22    def foreground(range: Text.Range): Stream[Text.Info[Color]] =
    4.23      snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)), _ =>
    4.24        {
     5.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 28 16:11:48 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Mar 28 22:42:18 2013 +0100
     5.3 @@ -243,7 +243,15 @@
     5.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     5.5      {
     5.6        robust_rendering { rendering =>
     5.7 -        val ascent = text_area.getPainter.getFontMetrics.getAscent
     5.8 +        val fm = text_area.getPainter.getFontMetrics
     5.9 +
    5.10 +        val (bullet_x, bullet_y, bullet_w, bullet_h) =
    5.11 +        {
    5.12 +          val w = fm.charWidth(' ')
    5.13 +          val h = fm.getAscent
    5.14 +          val b = (if (w >= 8) w / 2 else w - 2) max 1
    5.15 +          ((w - b + 1) / 2, (h - b + 1) / 2, w - b, line_height - b)
    5.16 +        }
    5.17  
    5.18          for (i <- 0 until physical_lines.length) {
    5.19            if (physical_lines(i) != -1) {
    5.20 @@ -285,6 +293,16 @@
    5.21                gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
    5.22              }
    5.23  
    5.24 +            // bullet bar
    5.25 +            for {
    5.26 +              Text.Info(range, color) <- rendering.bullet(line_range)
    5.27 +              r <- JEdit_Lib.gfx_range(text_area, range)
    5.28 +            } {
    5.29 +              gfx.setColor(color)
    5.30 +              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
    5.31 +                r.length - bullet_w, line_height - bullet_h)
    5.32 +            }
    5.33 +
    5.34              // squiggly underline
    5.35              for {
    5.36                Text.Info(range, color) <- rendering.squiggly_underline(line_range)
    5.37 @@ -292,7 +310,7 @@
    5.38              } {
    5.39                gfx.setColor(color)
    5.40                val x0 = (r.x / 2) * 2
    5.41 -              val y0 = r.y + ascent + 1
    5.42 +              val y0 = r.y + fm.getAscent + 1
    5.43                for (x1 <- Range(x0, x0 + r.length, 2)) {
    5.44                  val y1 = if (x1 % 4 < 2) y0 else y0 + 1
    5.45                  gfx.drawLine(x1, y1, x1 + 1, y1)