src/Tools/jEdit/src/rich_text_area.scala
author wenzelm
Mon, 01 Jul 2013 14:30:56 +0200
changeset 52494 a1e09340c0f4
parent 52483 478ef4fa3d5a
child 52495 bf45606912e3
permissions -rw-r--r--
clarified tooltip timing of pending event and active state;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
     1
/*  Title:      Tools/jEdit/src/rich_text_area.scala
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
     3
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
     4
Enhanced version of jEdit text area, with rich text rendering,
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
     5
tooltips, hyperlinks etc.
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
     6
*/
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
     7
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
     8
package isabelle.jedit
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
     9
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    10
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    11
import isabelle._
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    12
50657
57abb2a814ab tuned imports;
wenzelm
parents: 50641
diff changeset
    13
import java.awt.{Graphics2D, Shape, Color, Point, Toolkit}
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    14
import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    15
  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
43392
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    16
import java.awt.font.TextAttribute
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    17
import java.text.AttributedString
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    18
import java.util.ArrayList
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    19
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    20
import org.gjt.sp.util.Log
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    21
import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    22
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    23
import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    24
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    25
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
    26
class Rich_Text_Area(
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
    27
  view: View,
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
    28
  text_area: TextArea,
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
    29
  get_rendering: () => Rendering,
50915
12de8ea66f54 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents: 50849
diff changeset
    30
  close_action: () => Unit,
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50216
diff changeset
    31
  caret_visible: Boolean,
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
    32
  hovering: Boolean)
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    33
{
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    34
  private val buffer = text_area.getBuffer
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    35
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    36
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    37
  /* robust extension body */
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    38
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    39
  def robust_body[A](default: A)(body: => A): A =
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    40
  {
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    41
    try {
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    42
      Swing_Thread.require()
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    43
      if (buffer == text_area.getBuffer) body
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    44
      else {
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    45
        Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    46
        default
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    47
      }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    48
    }
50641
wenzelm
parents: 50553
diff changeset
    49
    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    50
  }
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
    51
43392
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    52
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    53
  /* original painters */
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    54
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    55
  private def pick_extension(name: String): TextAreaExtension =
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    56
  {
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    57
    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    58
    match {
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    59
      case List(x) => x
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    60
      case _ => error("Expected exactly one " + name)
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    61
    }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    62
  }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    63
43392
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    64
  private val orig_text_painter =
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    65
    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    66
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
    67
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
    68
  /* common painter state */
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    69
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
    70
  @volatile private var painter_rendering: Rendering = null
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
    71
  @volatile private var painter_clip: Shape = null
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    72
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
    73
  private val set_state = new TextAreaExtension
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    74
  {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    75
    override def paintScreenLineRange(gfx: Graphics2D,
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    76
      first_line: Int, last_line: Int, physical_lines: Array[Int],
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    77
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    78
    {
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    79
      painter_rendering = get_rendering()
46220
663251a395c2 more explicit/robust treatment of common snapshot;
wenzelm
parents: 46205
diff changeset
    80
      painter_clip = gfx.getClip
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    81
    }
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    82
  }
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    83
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
    84
  private val reset_state = new TextAreaExtension
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
    85
  {
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    86
    override def paintScreenLineRange(gfx: Graphics2D,
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    87
      first_line: Int, last_line: Int, physical_lines: Array[Int],
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    88
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    89
    {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
    90
      painter_rendering = null
46220
663251a395c2 more explicit/robust treatment of common snapshot;
wenzelm
parents: 46205
diff changeset
    91
      painter_clip = null
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    92
    }
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    93
  }
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
    94
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
    95
  def robust_rendering(body: Rendering => Unit)
46220
663251a395c2 more explicit/robust treatment of common snapshot;
wenzelm
parents: 46205
diff changeset
    96
  {
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    97
    robust_body(()) { body(painter_rendering) }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    98
  }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
    99
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   100
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   101
  /* active areas within the text */
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   102
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
   103
  private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]])
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   104
  {
49493
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   105
    private var the_text_info: Option[(String, Text.Info[A])] = None
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   106
49493
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   107
    def text_info: Option[(String, Text.Info[A])] = the_text_info
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   108
    def info: Option[Text.Info[A]] = the_text_info.map(_._2)
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   109
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   110
    def update(new_info: Option[Text.Info[A]])
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   111
    {
49493
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   112
      val old_text_info = the_text_info
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   113
      val new_text_info =
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   114
        new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   115
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   116
      if (new_text_info != old_text_info) {
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   117
        for {
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   118
          r0 <- JEdit_Lib.visible_range(text_area)
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   119
          opt <- List(old_text_info, new_text_info)
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   120
          (_, Text.Info(r1, _)) <- opt
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   121
          r2 <- r1.try_restrict(r0)  // FIXME more precise?!
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   122
        } JEdit_Lib.invalidate_range(text_area, r2)
db58490a68ac more realistic sendback: pick exec_id from message position and text from buffer;
wenzelm
parents: 49492
diff changeset
   123
        the_text_info = new_text_info
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   124
      }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   125
    }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   126
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
   127
    def update_rendering(r: Rendering, range: Text.Range)
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   128
    { update(rendering(r)(range)) }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   129
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   130
    def reset { update(None) }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   131
  }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   132
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   133
  // owned by Swing thread
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   134
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   135
  private var control: Boolean = false
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   136
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
   137
  private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
   138
  private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50306
diff changeset
   139
  private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   140
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   141
  private val active_areas =
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50306
diff changeset
   142
    List((highlight_area, true), (hyperlink_area, true), (active_area, false))
50216
de77cde57376 reset active areas on content update;
wenzelm
parents: 50215
diff changeset
   143
  def active_reset(): Unit = active_areas.foreach(_._1.reset)
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   144
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   145
  private val focus_listener = new FocusAdapter {
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   146
    override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   147
  }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   148
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   149
  private val window_listener = new WindowAdapter {
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   150
    override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   151
    override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   152
  }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   153
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   154
  private val mouse_listener = new MouseAdapter {
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   155
    override def mouseClicked(e: MouseEvent) {
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   156
      robust_body(()) {
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   157
        hyperlink_area.info match {
52482
5b7c4fb41511 explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
wenzelm
parents: 52480
diff changeset
   158
          case Some(Text.Info(_, link)) =>
5b7c4fb41511 explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
wenzelm
parents: 52480
diff changeset
   159
            Pretty_Tooltip.dismiss_all()
5b7c4fb41511 explicit Pretty_Tooltip.dismiss_all due to slightly changed focus mechanics;
wenzelm
parents: 52480
diff changeset
   160
            link.follow(view)
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   161
          case None =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   162
        }
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50306
diff changeset
   163
        active_area.text_info match {
50915
12de8ea66f54 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents: 50849
diff changeset
   164
          case Some((text, Text.Info(_, markup))) =>
12de8ea66f54 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents: 50849
diff changeset
   165
            Active.action(view, text, markup)
12de8ea66f54 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents: 50849
diff changeset
   166
            close_action()
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   167
          case None =>
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   168
        }
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   169
      }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   170
    }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   171
  }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   172
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   173
  private val mouse_motion_listener = new MouseMotionAdapter {
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   174
    override def mouseMoved(e: MouseEvent) {
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   175
      robust_body(()) {
50553
ce0398b766ce prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;
wenzelm
parents: 50502
diff changeset
   176
        control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   177
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   178
        if ((control || hovering) && !buffer.isLoading) {
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   179
          JEdit_Lib.buffer_lock(buffer) {
51441
37f699750430 more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm
parents: 50915
diff changeset
   180
            JEdit_Lib.pixel_range(text_area, e.getX, e.getY) match {
50211
2a3d6d760629 always reset active areas;
wenzelm
parents: 50199
diff changeset
   181
              case None => active_reset()
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   182
              case Some(range) =>
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   183
                val rendering = get_rendering()
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   184
                for ((area, require_control) <- active_areas)
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   185
                {
50165
24d47733975f reset active area for outdated snapshot (again?);
wenzelm
parents: 50164
diff changeset
   186
                  if (control == require_control && !rendering.snapshot.is_outdated)
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   187
                    area.update_rendering(rendering, range)
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   188
                  else area.reset
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   189
                }
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   190
            }
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   191
          }
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   192
        }
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   193
        else active_reset()
51441
37f699750430 more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm
parents: 50915
diff changeset
   194
52494
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   195
        if (e.getSource == text_area.getPainter) {
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   196
          Pretty_Tooltip.invoke(() =>
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   197
            {
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   198
              val rendering = get_rendering()
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   199
              val snapshot = rendering.snapshot
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   200
              if (!snapshot.is_outdated) {
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   201
                val x = e.getX
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   202
                val y = e.getY
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   203
                JEdit_Lib.pixel_range(text_area, x, y) match {
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   204
                  case None =>
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   205
                  case Some(range) =>
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   206
                    val result =
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   207
                      if (control) rendering.tooltip(range)
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   208
                      else rendering.tooltip_message(range)
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   209
                    result match {
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   210
                      case None =>
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   211
                      case Some(tip) =>
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   212
                        val painter = text_area.getPainter
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   213
                        val screen_point = e.getLocationOnScreen
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   214
                        screen_point.translate(0, painter.getFontMetrics.getHeight / 2)
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   215
                        val results = rendering.command_results(range)
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   216
                        Pretty_Tooltip(view, painter, rendering, screen_point, results, tip.info)
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   217
                    }
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   218
                }
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   219
              }
a1e09340c0f4 clarified tooltip timing of pending event and active state;
wenzelm
parents: 52483
diff changeset
   220
            })
51452
14e6d761ba1c extra tooltip_delay after window.dismiss operation, to avoid flickering of quick reactivation;
wenzelm
parents: 51449
diff changeset
   221
        }
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   222
      }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   223
    }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   224
  }
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   225
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   226
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   227
  /* text background */
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   228
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   229
  private val background_painter = new TextAreaExtension
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   230
  {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   231
    override def paintScreenLineRange(gfx: Graphics2D,
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   232
      first_line: Int, last_line: Int, physical_lines: Array[Int],
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   233
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   234
    {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   235
      robust_rendering { rendering =>
51581
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   236
        val fm = text_area.getPainter.getFontMetrics
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   237
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   238
        for (i <- 0 until physical_lines.length) {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   239
          if (physical_lines(i) != -1) {
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49730
diff changeset
   240
            val line_range = Text.Range(start(i), end(i))
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   241
49473
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49424
diff changeset
   242
            // line background color
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49424
diff changeset
   243
            for { (color, separator) <- rendering.line_background(line_range) }
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49424
diff changeset
   244
            {
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49424
diff changeset
   245
              gfx.setColor(color)
49475
8f3a3adadd5a tuned painter;
wenzelm
parents: 49473
diff changeset
   246
              val sep = if (separator) (2 min (line_height / 2)) else 0
8f3a3adadd5a tuned painter;
wenzelm
parents: 49473
diff changeset
   247
              gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
49473
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49424
diff changeset
   248
            }
ca7e2c21b104 tuned rendering;
wenzelm
parents: 49424
diff changeset
   249
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45665
diff changeset
   250
            // background color (1)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   251
            for {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   252
              Text.Info(range, color) <- rendering.background1(line_range)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   253
              r <- JEdit_Lib.gfx_range(text_area, range)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   254
            } {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   255
              gfx.setColor(color)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   256
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   257
            }
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   258
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50306
diff changeset
   259
            // active area -- potentially from other snapshot
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   260
            for {
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50306
diff changeset
   261
              info <- active_area.info
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   262
              Text.Info(range, _) <- info.try_restrict(line_range)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   263
              r <- JEdit_Lib.gfx_range(text_area, range)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   264
            } {
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50306
diff changeset
   265
              gfx.setColor(rendering.active_hover_color)
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   266
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   267
            }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49475
diff changeset
   268
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45665
diff changeset
   269
            // background color (2)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   270
            for {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   271
              Text.Info(range, color) <- rendering.background2(line_range)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   272
              r <- JEdit_Lib.gfx_range(text_area, range)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   273
            } {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   274
              gfx.setColor(color)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   275
              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   276
            }
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   277
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   278
            // squiggly underline
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   279
            for {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   280
              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   281
              r <- JEdit_Lib.gfx_range(text_area, range)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   282
            } {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   283
              gfx.setColor(color)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   284
              val x0 = (r.x / 2) * 2
51574
2b58d7b139d6 ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents: 51496
diff changeset
   285
              val y0 = r.y + fm.getAscent + 1
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   286
              for (x1 <- Range(x0, x0 + r.length, 2)) {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   287
                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   288
                gfx.drawLine(x1, y1, x1 + 1, y1)
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   289
              }
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   290
            }
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   291
          }
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   292
        }
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43375
diff changeset
   293
      }
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   294
    }
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   295
  }
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   296
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   297
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   298
  /* text */
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   299
50199
6d04e2422769 quasi-abstract module Rendering, with Isabelle-specific implementation;
wenzelm
parents: 50165
diff changeset
   300
  private def paint_chunk_list(rendering: Rendering,
43505
0aca4edbfa99 clarified chunk.offset, chunk.length;
wenzelm
parents: 43451
diff changeset
   301
    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   302
  {
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   303
    val clip_rect = gfx.getClipBounds
43392
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
   304
    val painter = text_area.getPainter
fe4b8c52b1cc paint caret according to precise font metrics;
wenzelm
parents: 43383
diff changeset
   305
    val font_context = painter.getFontRenderContext
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   306
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   307
    var w = 0.0f
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   308
    var chunk = head
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   309
    while (chunk != null) {
43505
0aca4edbfa99 clarified chunk.offset, chunk.length;
wenzelm
parents: 43451
diff changeset
   310
      val chunk_offset = line_start + chunk.offset
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   311
      if (x + w + chunk.width > clip_rect.x &&
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50216
diff changeset
   312
          x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   313
      {
43505
0aca4edbfa99 clarified chunk.offset, chunk.length;
wenzelm
parents: 43451
diff changeset
   314
        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
44662
c8f1d943bfc5 more robust chunk painting wrt. hard tabs, when chunk.str == null;
wenzelm
parents: 44545
diff changeset
   315
        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   316
        val chunk_font = chunk.style.getFont
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   317
        val chunk_color = chunk.style.getForegroundColor
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   318
44056
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   319
        def string_width(s: String): Float =
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   320
          if (s.isEmpty) 0.0f
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   321
          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   322
43448
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43435
diff changeset
   323
        val caret_range =
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50216
diff changeset
   324
          if (caret_visible && text_area.isCaretVisible)
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49357
diff changeset
   325
            JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
43448
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43435
diff changeset
   326
          else Text.Range(-1)
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43435
diff changeset
   327
43426
24e2e2f0032b more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
wenzelm
parents: 43419
diff changeset
   328
        val markup =
43428
b41dea5772c6 more robust treatment of partial range restriction;
wenzelm
parents: 43426
diff changeset
   329
          for {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   330
            r1 <- rendering.text_color(chunk_range, chunk_color)
43450
b6b09fc8d671 proper x1;
wenzelm
parents: 43448
diff changeset
   331
            r2 <- r1.try_restrict(chunk_range)
b6b09fc8d671 proper x1;
wenzelm
parents: 43448
diff changeset
   332
          } yield r2
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   333
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   334
        val padded_markup =
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   335
          if (markup.isEmpty)
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46178
diff changeset
   336
            Iterator(Text.Info(chunk_range, chunk_color))
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   337
          else
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46178
diff changeset
   338
            Iterator(
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46178
diff changeset
   339
              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   340
            markup.iterator ++
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46178
diff changeset
   341
            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   342
43450
b6b09fc8d671 proper x1;
wenzelm
parents: 43448
diff changeset
   343
        var x1 = x + w
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   344
        gfx.setFont(chunk_font)
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46178
diff changeset
   345
        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
44662
c8f1d943bfc5 more robust chunk painting wrt. hard tabs, when chunk.str == null;
wenzelm
parents: 44545
diff changeset
   346
          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46178
diff changeset
   347
          gfx.setColor(color)
43448
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43435
diff changeset
   348
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   349
          range.try_restrict(caret_range) match {
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   350
            case Some(r) if !r.is_singularity =>
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   351
              val i = r.start - range.start
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   352
              val j = r.stop - range.start
44056
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   353
              val s1 = str.substring(0, i)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   354
              val s2 = str.substring(i, j)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   355
              val s3 = str.substring(j)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   356
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   357
              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   358
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   359
              val astr = new AttributedString(s2)
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   360
              astr.addAttribute(TextAttribute.FONT, chunk_font)
44056
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   361
              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   362
              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   363
              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   364
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   365
              if (!s3.isEmpty)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   366
                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   367
43759
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   368
            case _ =>
d93a69672362 more uniform padded_markup, which is important for caret visibility despite absence of markup;
wenzelm
parents: 43506
diff changeset
   369
              gfx.drawString(str, x1, y)
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   370
          }
44056
be825a69fc67 less ambitious use of AttributedString, for proper caret painting within \<^sup>\<foobar>;
wenzelm
parents: 43759
diff changeset
   371
          x1 += string_width(str)
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   372
        }
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   373
      }
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   374
      w += chunk.width
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   375
      chunk = chunk.next.asInstanceOf[Chunk]
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   376
    }
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   377
    w
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   378
  }
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   379
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   380
  private val text_painter = new TextAreaExtension
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   381
  {
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   382
    override def paintScreenLineRange(gfx: Graphics2D,
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   383
      first_line: Int, last_line: Int, physical_lines: Array[Int],
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   384
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   385
    {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   386
      robust_rendering { rendering =>
51581
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   387
        val painter = text_area.getPainter
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   388
        val fm = painter.getFontMetrics
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   389
        val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   390
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   391
        val clip = gfx.getClip
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   392
        val x0 = text_area.getHorizontalOffset
43382
5d9d34bdec25 misc tuning and simplification;
wenzelm
parents: 43381
diff changeset
   393
        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
43372
2df2144b0910 use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents: 43371
diff changeset
   394
51581
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   395
        val (bullet_x, bullet_y, bullet_w, bullet_h) =
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   396
        {
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   397
          val w = fm.charWidth(' ')
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   398
          val b = (w / 2) max 1
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   399
          val c = (lm.getAscent + lm.getStrikethroughOffset).round.toInt
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   400
          ((w - b + 1) / 2, c - b / 2, w - b, line_height - b)
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   401
        }
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   402
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   403
        for (i <- 0 until physical_lines.length) {
49097
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   404
          val line = physical_lines(i)
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   405
          if (line != -1) {
51581
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   406
            val line_range = Text.Range(start(i), end(i))
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   407
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   408
            // bullet bar
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   409
            for {
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   410
              Text.Info(range, color) <- rendering.bullet(line_range)
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   411
              r <- JEdit_Lib.gfx_range(text_area, range)
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   412
            } {
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   413
              gfx.setColor(color)
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   414
              gfx.fillRect(r.x + bullet_x, y + i * line_height + bullet_y,
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   415
                r.length - bullet_w, line_height - bullet_h)
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   416
            }
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   417
587c917e8d36 paint bullet bar within text layer -- thus it remains visible with active selection etc.;
wenzelm
parents: 51577
diff changeset
   418
            // text chunks
49097
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   419
            val screen_line = first_line + i
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   420
            val chunks = text_area.getChunksOfScreenLine(screen_line)
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   421
            if (chunks != null) {
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   422
              val line_start = buffer.getLineStartOffset(line)
49097
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   423
              gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   424
              val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
49097
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   425
              gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   426
              orig_text_painter.paintValidLine(gfx,
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   427
                screen_line, line, start(i), end(i), y + line_height * i)
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   428
              gfx.setClip(clip)
4e5e48c589ea more direct access to all-important chunks for text painting;
wenzelm
parents: 48921
diff changeset
   429
            }
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   430
          }
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   431
          y0 += line_height
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   432
        }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   433
      }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   434
    }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   435
  }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   436
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   437
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   438
  /* foreground */
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   439
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   440
  private val foreground_painter = new TextAreaExtension
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   441
  {
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   442
    override def paintScreenLineRange(gfx: Graphics2D,
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   443
      first_line: Int, last_line: Int, physical_lines: Array[Int],
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   444
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   445
    {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   446
      robust_rendering { rendering =>
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   447
        for (i <- 0 until physical_lines.length) {
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   448
          if (physical_lines(i) != -1) {
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49730
diff changeset
   449
            val line_range = Text.Range(start(i), end(i))
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   450
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   451
            // foreground color
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   452
            for {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   453
              Text.Info(range, color) <- rendering.foreground(line_range)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   454
              r <- JEdit_Lib.gfx_range(text_area, range)
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   455
            } {
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   456
              gfx.setColor(color)
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   457
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   458
            }
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44056
diff changeset
   459
49357
34ac36642a31 more general Document_Model.point_range;
wenzelm
parents: 49356
diff changeset
   460
            // highlight range -- potentially from other snapshot
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46204
diff changeset
   461
            for {
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   462
              info <- highlight_area.info
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46204
diff changeset
   463
              Text.Info(range, color) <- info.try_restrict(line_range)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   464
              r <- JEdit_Lib.gfx_range(text_area, range)
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46204
diff changeset
   465
            } {
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46204
diff changeset
   466
              gfx.setColor(color)
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46204
diff changeset
   467
              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   468
            }
48921
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   469
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   470
            // hyperlink range -- potentially from other snapshot
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   471
            for {
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   472
              info <- hyperlink_area.info
48921
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   473
              Text.Info(range, _) <- info.try_restrict(line_range)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   474
              r <- JEdit_Lib.gfx_range(text_area, range)
48921
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   475
            } {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   476
              gfx.setColor(rendering.hyperlink_color)
48921
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   477
              gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
5d8d409b897e support for direct hyperlinks, without the Hyperlinks plugin;
wenzelm
parents: 47471
diff changeset
   478
            }
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   479
          }
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   480
        }
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   481
      }
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   482
    }
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   483
  }
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   484
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   485
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   486
  /* caret -- outside of text range */
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   487
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   488
  private class Caret_Painter(before: Boolean) extends TextAreaExtension
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   489
  {
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   490
    override def paintValidLine(gfx: Graphics2D,
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   491
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   492
    {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   493
      robust_rendering { _ =>
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43398
diff changeset
   494
        if (before) gfx.clipRect(0, 0, 0, 0)
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43398
diff changeset
   495
        else gfx.setClip(painter_clip)
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43398
diff changeset
   496
      }
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   497
    }
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   498
  }
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   499
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   500
  private val before_caret_painter1 = new Caret_Painter(true)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   501
  private val after_caret_painter1 = new Caret_Painter(false)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   502
  private val before_caret_painter2 = new Caret_Painter(true)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   503
  private val after_caret_painter2 = new Caret_Painter(false)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   504
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   505
  private val caret_painter = new TextAreaExtension
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   506
  {
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   507
    override def paintValidLine(gfx: Graphics2D,
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   508
      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   509
    {
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49355
diff changeset
   510
      robust_rendering { _ =>
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50216
diff changeset
   511
        if (caret_visible && text_area.isCaretVisible) {
43398
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   512
          val caret = text_area.getCaretPosition
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   513
          if (start <= caret && caret == end - 1) {
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   514
            val painter = text_area.getPainter
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   515
            val fm = painter.getFontMetrics
51492
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51469
diff changeset
   516
            val metric = JEdit_Lib.pretty_metric(painter)
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   517
43398
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   518
            val offset = caret - text_area.getLineStartOffset(physical_line)
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   519
            val x = text_area.offsetToXY(physical_line, offset).x
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   520
            gfx.setColor(painter.getCaretColor)
51492
eaa1c4cc1106 more explicit Pretty.Metric, with clear distinction of unit (space width) vs. average char width (for visual adjustments) -- NB: Pretty formatting works via full space characters (despite a981a5c8a505 and 70f7483df9cb);
wenzelm
parents: 51469
diff changeset
   521
            gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
43398
c3e2a361b418 more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
wenzelm
parents: 43396
diff changeset
   522
          }
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   523
        }
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   524
      }
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   525
    }
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   526
  }
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   527
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   528
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   529
  /* activation */
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   530
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   531
  def activate()
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   532
  {
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   533
    val painter = text_area.getPainter
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   534
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   535
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   536
    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   537
    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   538
    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   539
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   540
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   541
    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   542
    painter.addExtension(500, foreground_painter)
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   543
    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   544
    painter.removeExtension(orig_text_painter)
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   545
    painter.addMouseListener(mouse_listener)
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   546
    painter.addMouseMotionListener(mouse_motion_listener)
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   547
    text_area.addFocusListener(focus_listener)
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   548
    view.addWindowListener(window_listener)
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   549
  }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   550
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   551
  def deactivate()
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   552
  {
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   553
    val painter = text_area.getPainter
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   554
    view.removeWindowListener(window_listener)
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   555
    text_area.removeFocusListener(focus_listener)
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   556
    painter.removeMouseMotionListener(mouse_motion_listener)
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49409
diff changeset
   557
    painter.removeMouseListener(mouse_listener)
43396
548a68eafaea recovered orig_text_painter from f4141da52e92;
wenzelm
parents: 43393
diff changeset
   558
    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   559
    painter.removeExtension(reset_state)
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
   560
    painter.removeExtension(foreground_painter)
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   561
    painter.removeExtension(caret_painter)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   562
    painter.removeExtension(after_caret_painter2)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   563
    painter.removeExtension(before_caret_painter2)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   564
    painter.removeExtension(after_caret_painter1)
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   565
    painter.removeExtension(before_caret_painter1)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   566
    painter.removeExtension(text_painter)
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   567
    painter.removeExtension(background_painter)
43393
f4141da52e92 more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
wenzelm
parents: 43392
diff changeset
   568
    painter.removeExtension(set_state)
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   569
  }
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   570
}
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff changeset
   571