src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue, 18 Feb 2014 15:38:50 +0100
changeset 55551 5c40782f68b3
parent 53786 064cb0458071
child 55690 d73949233c2e
permissions -rw-r--r--
clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit_lib.scala
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     3
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     4
Misc library functions for jEdit.
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     5
*/
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     6
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     8
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
     9
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    10
import isabelle._
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    11
53712
ea51046be71b tuned signature;
wenzelm
parents: 53274
diff changeset
    12
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension}
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
    13
import java.awt.event.{InputEvent, KeyEvent, KeyListener}
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    14
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
49710
21d88a631fcc refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents: 49409
diff changeset
    15
21d88a631fcc refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents: 49409
diff changeset
    16
import scala.annotation.tailrec
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    17
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
    18
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
    19
import org.gjt.sp.jedit.gui.KeyEventWorkaround
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    20
import org.gjt.sp.jedit.buffer.JEditBuffer
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
    21
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    22
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    23
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    24
object JEdit_Lib
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    25
{
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    26
  /* location within multi-screen environment */
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    27
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    28
  final case class Screen_Location(point: Point, bounds: Rectangle)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    29
  {
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    30
    def relative(parent: Component, size: Dimension): Point =
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    31
    {
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    32
      val w = size.width
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    33
      val h = size.height
50554
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    34
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    35
      val x0 = parent.getLocationOnScreen.x
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    36
      val y0 = parent.getLocationOnScreen.y
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    37
      val x1 = x0 + parent.getWidth - w
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    38
      val y1 = y0 + parent.getHeight - h
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    39
      val x2 = point.x min (bounds.x + bounds.width - w)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    40
      val y2 = point.y min (bounds.y + bounds.height - h)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    41
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    42
      val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    43
      SwingUtilities.convertPointFromScreen(location, parent)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    44
      location
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    45
    }
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    46
  }
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    47
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    48
  def screen_location(component: Component, point: Point): Screen_Location =
50554
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    49
  {
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    50
    val screen_point = new Point(point.x, point.y)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    51
    SwingUtilities.convertPointToScreen(screen_point, component)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    52
50554
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    53
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    54
    val screen_bounds =
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    55
      (for {
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    56
        device <- ge.getScreenDevices.iterator
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    57
        config <- device.getConfigurations.iterator
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    58
        bounds = config.getBounds
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    59
      } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    60
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53237
diff changeset
    61
    Screen_Location(screen_point, screen_bounds)
50554
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    62
  }
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    63
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    64
53019
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    65
  /* window geometry measurement */
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    66
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    67
  private lazy val dummy_window = new JWindow
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    68
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    69
  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    70
  {
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    71
    def deco_width: Int = width - inner_width
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    72
    def deco_height: Int = height - inner_height
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    73
  }
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    74
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    75
  def window_geometry(outer: Container, inner: Component): Window_Geometry =
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    76
  {
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    77
    Swing_Thread.require()
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    78
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    79
    val old_content = dummy_window.getContentPane
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    80
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    81
    dummy_window.setContentPane(outer)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    82
    dummy_window.pack
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    83
    dummy_window.revalidate
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    84
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    85
    val geometry =
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    86
      Window_Geometry(
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    87
        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    88
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    89
    dummy_window.setContentPane(old_content)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    90
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    91
    geometry
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    92
  }
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    93
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    94
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    95
  /* buffers */
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    96
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    97
  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    98
    Swing_Thread.now { buffer_lock(buffer) { body } }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    99
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   100
  def buffer_text(buffer: JEditBuffer): String =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   101
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   102
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   103
  def buffer_mode(buffer: JEditBuffer): String =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   104
  {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   105
    val mode = buffer.getMode
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   106
    if (mode == null) ""
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   107
    else {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   108
      val name = mode.getName
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   109
      if (name == null) "" else name
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   110
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   111
  }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
   112
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   113
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   114
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   115
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   116
  /* main jEdit components */
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   117
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   118
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   119
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   120
  def jedit_buffer(name: String): Option[Buffer] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   121
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   122
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   123
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   124
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   125
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   126
    view.getEditPanes().iterator.map(_.getTextArea)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   127
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   128
  def jedit_text_areas(): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   129
    jedit_views().flatMap(jedit_text_areas(_))
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   130
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   131
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   132
    jedit_text_areas().filter(_.getBuffer == buffer)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   133
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   134
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   135
  {
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   136
    try { buffer.readLock(); body }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   137
    finally { buffer.readUnlock() }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   138
  }
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   139
50195
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   140
  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   141
  {
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   142
    try { buffer.beginCompoundEdit(); body }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   143
    finally { buffer.endCompoundEdit() }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   144
  }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   145
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   146
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   147
  /* get text */
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   148
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   149
  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   150
    try { Some(buffer.getText(range.start, range.length)) }
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   151
    catch { case _: ArrayIndexOutOfBoundsException => None }
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   152
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   153
  def try_get_text(text: String, range: Text.Range): Option[String] =
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   154
    try { Some(text.substring(range.start, range.stop)) }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   155
    catch { case _: IndexOutOfBoundsException => None }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   156
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   157
50363
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   158
  /* buffer range */
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   159
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   160
  def buffer_range(buffer: JEditBuffer): Text.Range =
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   161
    Text.Range(0, (buffer.getLength - 1) max 0)
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   162
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   163
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   164
  /* point range */
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   165
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   166
  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   167
    buffer_lock(buffer) {
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   168
      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   169
      try {
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   170
        val c = text(offset)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   171
        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   172
          Text.Range(offset, offset + 2)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   173
        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   174
          Text.Range(offset - 1, offset + 1)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   175
        else Text.Range(offset, offset + 1)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   176
      }
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   177
      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   178
    }
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   179
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   180
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   181
  /* visible text range */
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   182
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   183
  def visible_range(text_area: TextArea): Option[Text.Range] =
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   184
  {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   185
    val buffer = text_area.getBuffer
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   186
    val n = text_area.getVisibleLines
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   187
    if (n > 0) {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   188
      val start = text_area.getScreenLineStartOffset(0)
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   189
      val raw_end = text_area.getScreenLineEndOffset(n - 1)
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49712
diff changeset
   190
      val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49712
diff changeset
   191
      Some(Text.Range(start, end))
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   192
    }
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   193
    else None
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   194
  }
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   195
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   196
  def invalidate_range(text_area: TextArea, range: Text.Range)
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   197
  {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   198
    val buffer = text_area.getBuffer
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   199
    text_area.invalidateLineRange(
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   200
      buffer.getLineOfOffset(range.start),
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   201
      buffer.getLineOfOffset(range.stop))
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   202
  }
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   203
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   204
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   205
  /* graphics range */
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   206
50115
8cde6f1a0106 tuned signature;
wenzelm
parents: 49941
diff changeset
   207
  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   208
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49712
diff changeset
   209
  // NB: jEdit always normalizes \r\n and \r to \n
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   210
  // NB: last line lacks \n
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   211
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   212
  {
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   213
    val metric = pretty_metric(text_area.getPainter)
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
   214
    val char_width = (metric.unit * metric.average).round.toInt
50849
70f7483df9cb more uniform Pretty.char_width;
wenzelm
parents: 50658
diff changeset
   215
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   216
    val buffer = text_area.getBuffer
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   217
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   218
    val end = buffer.getLength
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   219
    val stop = range.stop
51078
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   220
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   221
    val (p, q, r) =
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   222
      try {
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   223
        val p = text_area.offsetToXY(range.start)
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   224
        val (q, r) =
55551
5c40782f68b3 clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
wenzelm
parents: 53786
diff changeset
   225
          if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
51078
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   226
            (text_area.offsetToXY(stop - 1), char_width)
55551
5c40782f68b3 clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
wenzelm
parents: 53786
diff changeset
   227
          else if (stop >= end)
5c40782f68b3 clarified special eol treatment (amending 3d55ef732cd7): allow last line to be empty, which means stop == end for second-last line;
wenzelm
parents: 53786
diff changeset
   228
            (text_area.offsetToXY(end), char_width * (stop - end))
51078
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   229
          else (text_area.offsetToXY(stop), 0)
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   230
        (p, q, r)
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   231
      }
4e1c940b1fb2 more robust JEdit_Lib.pixel_range, which could crash via Rich_Text_Area.tooltip_painter with bad mouse coordinates;
wenzelm
parents: 50849
diff changeset
   232
      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   233
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   234
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
50115
8cde6f1a0106 tuned signature;
wenzelm
parents: 49941
diff changeset
   235
      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   236
    else None
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   237
  }
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   238
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   239
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   240
  /* pixel range */
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   241
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   242
  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   243
  {
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   244
    // coordinates wrt. inner painter component
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   245
    val painter = text_area.getPainter
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   246
    if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   247
      val offset = text_area.xyToOffset(x, y, false)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   248
      if (offset >= 0) {
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   249
        val range = point_range(text_area.getBuffer, offset)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   250
        gfx_range(text_area, range) match {
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   251
          case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   252
          case _ => None
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   253
        }
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   254
      }
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   255
      else None
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   256
    }
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   257
    else None
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   258
  }
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
   259
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
   260
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
   261
  /* pretty text metric */
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
   262
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   263
  abstract class Pretty_Metric extends Pretty.Metric
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   264
  {
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   265
    def average: Double
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   266
  }
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
   267
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   268
  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   269
    new Pretty_Metric {
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   270
      def string_width(s: String): Double =
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   271
        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   272
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   273
      val unit = string_width(Pretty.space)
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   274
      val average = string_width("mix") / (3 * unit)
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   275
      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
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
   276
    }
52873
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   277
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   278
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   279
  /* icons */
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   280
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   281
  def load_icon(name: String): Icon =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   282
  {
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   283
    val name1 =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   284
      if (name.startsWith("idea-icons/")) {
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   285
        val file =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   286
          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   287
        "jar:" + file + "!/" + name
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   288
      }
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   289
      else name
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   290
    val icon = GUIUtilities.loadIcon(name1)
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   291
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   292
    else icon
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   293
  }
52874
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   294
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   295
  def load_image_icon(name: String): ImageIcon =
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   296
    load_icon(name) match {
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   297
      case icon: ImageIcon => icon
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   298
      case _ => error("Bad image icon: " + name)
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   299
    }
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   300
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   301
53231
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   302
  /* key event handling */
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   303
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   304
  def request_focus_view
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   305
  {
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   306
    val view = jEdit.getActiveView()
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   307
    if (view != null) {
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   308
      val text_area = view.getTextArea
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   309
      if (text_area != null) text_area.requestFocus
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   310
    }
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   311
  }
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   312
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   313
  def propagate_key(view: View, evt: KeyEvent)
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   314
  {
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   315
    if (view != null && !evt.isConsumed)
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   316
      view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
423e29f1f304 avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
wenzelm
parents: 53226
diff changeset
   317
  }
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   318
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   319
  def key_listener(
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   320
    key_typed: KeyEvent => Unit = _ => (),
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   321
    key_pressed: KeyEvent => Unit = _ => (),
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   322
    key_released: KeyEvent => Unit = _ => ()): KeyListener =
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   323
  {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   324
    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   325
    {
53237
6bfe54791591 enable jEdit KeyEventWorkaround uniformly;
wenzelm
parents: 53231
diff changeset
   326
      val evt = KeyEventWorkaround.processKeyEvent(evt0)
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   327
      if (evt != null) handle(evt)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   328
    }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   329
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   330
    new KeyListener
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   331
    {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   332
      def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   333
      def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   334
      def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   335
    }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   336
  }
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   337
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   338
  def special_key(evt: KeyEvent): Boolean =
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   339
  {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   340
    // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   341
    val mod = evt.getModifiers
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   342
    (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   343
    (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   344
      !Debug.ALT_KEY_PRESSED_DISABLED ||
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   345
    (mod & InputEvent.META_MASK) != 0
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   346
  }
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   347
}
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   348