src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue, 27 Aug 2013 12:35:32 +0200
changeset 53226 9cf8e2263ca7
parent 53183 018d71bee930
child 53231 423e29f1f304
permissions -rw-r--r--
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
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
50658
0464c2007a25 tuned signature;
wenzelm
parents: 50566
diff changeset
    12
import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
    13
import java.awt.event.{KeyEvent, KeyListener}
53019
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    14
import javax.swing.{Icon, ImageIcon, JWindow}
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
52873
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
    18
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
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
{
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
    26
  /* bounds within multi-screen environment */
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    27
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    28
  def screen_bounds(screen_point: Point): Rectangle =
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    29
  {
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    30
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    31
    (for {
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    32
      device <- ge.getScreenDevices.iterator
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    33
      config <- device.getConfigurations.iterator
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
      bounds = config.getBounds
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    35
    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    36
  }
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    37
0493efcc97e9 more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents: 50363
diff changeset
    38
53019
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    39
  /* window geometry measurement */
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    40
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    41
  private lazy val dummy_window = new JWindow
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    42
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    43
  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
    44
  {
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    45
    def deco_width: Int = width - inner_width
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    46
    def deco_height: Int = height - inner_height
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    47
  }
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    48
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    49
  def window_geometry(outer: Container, inner: Component): Window_Geometry =
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    50
  {
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    51
    Swing_Thread.require()
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    52
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    53
    val old_content = dummy_window.getContentPane
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    54
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    55
    dummy_window.setContentPane(outer)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    56
    dummy_window.pack
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    57
    dummy_window.revalidate
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    58
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    59
    val geometry =
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    60
      Window_Geometry(
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    61
        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    62
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    63
    dummy_window.setContentPane(old_content)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    64
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    65
    geometry
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    66
  }
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    67
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    68
49712
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    69
  /* GUI components */
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    70
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    71
  def get_parent(component: Component): Option[Container] =
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    72
    component.getParent match {
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    73
      case null => None
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    74
      case parent => Some(parent)
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    75
    }
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    76
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    77
  def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    78
    private var next_elem = get_parent(component)
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    79
    def hasNext(): Boolean = next_elem.isDefined
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    80
    def next(): Container =
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    81
      next_elem match {
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    82
        case Some(parent) =>
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    83
          next_elem = get_parent(parent)
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    84
          parent
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    85
        case None => Iterator.empty.next()
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    86
      }
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    87
  }
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    88
a1bd8fe5131b further support for nested tooltips;
wenzelm
parents: 49710
diff changeset
    89
  def parent_window(component: Component): Option[Window] =
52478
0a1db0d02628 manage popup windows via PopupFactory, which prefers light-weight JComponent, but might fall back on JWindow (despite JPanel of 0f88591478e6);
wenzelm
parents: 51507
diff changeset
    90
    ancestors(component).collectFirst({ case x: Window => x })
49710
21d88a631fcc refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents: 49409
diff changeset
    91
21d88a631fcc refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents: 49409
diff changeset
    92
50186
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    93
  /* basic tooltips, with multi-line support */
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    94
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    95
  def wrap_tooltip(text: String): String =
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    96
    if (text == "") null
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    97
    else "<html><pre>" + HTML.encode(text) + "</pre></html>"
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    98
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50116
diff changeset
    99
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   100
  /* buffers */
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   101
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   102
  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   103
    Swing_Thread.now { buffer_lock(buffer) { body } }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   104
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   105
  def buffer_text(buffer: JEditBuffer): String =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   106
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   107
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   108
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   109
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   110
53003
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   111
  /* focus of main window */
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   112
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   113
  def request_focus_view: Unit =
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   114
  {
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   115
    jEdit.getActiveView() match {
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   116
      case null =>
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   117
      case view =>
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   118
        view.getTextArea match {
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   119
          case null =>
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   120
          case text_area => text_area.requestFocus
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   121
        }
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   122
    }
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   123
  }
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   124
39da27fc6101 attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);
wenzelm
parents: 52874
diff changeset
   125
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   126
  /* main jEdit components */
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   127
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   128
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   129
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   130
  def jedit_buffer(name: String): Option[Buffer] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   131
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   132
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   133
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   134
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   135
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   136
    view.getEditPanes().iterator.map(_.getTextArea)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   137
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   138
  def jedit_text_areas(): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   139
    jedit_views().flatMap(jedit_text_areas(_))
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   140
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   141
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   142
    jedit_text_areas().filter(_.getBuffer == buffer)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   143
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   144
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   145
  {
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   146
    try { buffer.readLock(); body }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   147
    finally { buffer.readUnlock() }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   148
  }
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   149
50195
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   150
  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   151
  {
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   152
    try { buffer.beginCompoundEdit(); body }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   153
    finally { buffer.endCompoundEdit() }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   154
  }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   155
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   156
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   157
  /* get text */
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   158
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   159
  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   160
    try { Some(buffer.getText(range.start, range.length)) }
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   161
    catch { case _: ArrayIndexOutOfBoundsException => None }
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   162
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   163
50363
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   164
  /* buffer range */
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   165
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   166
  def buffer_range(buffer: JEditBuffer): Text.Range =
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   167
    Text.Range(0, (buffer.getLength - 1) max 0)
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   168
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50215
diff changeset
   169
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   170
  /* point range */
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   171
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   172
  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   173
    buffer_lock(buffer) {
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   174
      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   175
      try {
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   176
        val c = text(offset)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   177
        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   178
          Text.Range(offset, offset + 2)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   179
        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   180
          Text.Range(offset - 1, offset + 1)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   181
        else Text.Range(offset, offset + 1)
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   182
      }
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   183
      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   184
    }
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   185
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   186
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   187
  /* visible text range */
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   188
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   189
  def visible_range(text_area: TextArea): Option[Text.Range] =
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   190
  {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   191
    val buffer = text_area.getBuffer
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   192
    val n = text_area.getVisibleLines
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   193
    if (n > 0) {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   194
      val start = text_area.getScreenLineStartOffset(0)
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   195
      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
   196
      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
   197
      Some(Text.Range(start, end))
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   198
    }
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   199
    else None
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   200
  }
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   201
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   202
  def invalidate_range(text_area: TextArea, range: Text.Range)
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   203
  {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   204
    val buffer = text_area.getBuffer
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   205
    text_area.invalidateLineRange(
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   206
      buffer.getLineOfOffset(range.start),
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   207
      buffer.getLineOfOffset(range.stop))
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   208
  }
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   209
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   210
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   211
  /* graphics range */
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   212
50115
8cde6f1a0106 tuned signature;
wenzelm
parents: 49941
diff changeset
   213
  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   214
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49712
diff changeset
   215
  // NB: jEdit always normalizes \r\n and \r to \n
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   216
  // NB: last line lacks \n
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   217
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   218
  {
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   219
    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
   220
    val char_width = (metric.unit * metric.average).round.toInt
50849
70f7483df9cb more uniform Pretty.char_width;
wenzelm
parents: 50658
diff changeset
   221
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   222
    val buffer = text_area.getBuffer
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   223
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   224
    val end = buffer.getLength
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   225
    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
   226
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
   227
    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
   228
      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
   229
        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
   230
        val (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
          if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
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
          else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
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
   233
            (text_area.offsetToXY(stop - 1), char_width)
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
   234
          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
   235
        (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
   236
      }
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
   237
      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   238
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   239
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
50115
8cde6f1a0106 tuned signature;
wenzelm
parents: 49941
diff changeset
   240
      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   241
    else None
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   242
  }
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   243
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   244
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   245
  /* pixel range */
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   246
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   247
  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
   248
  {
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   249
    // coordinates wrt. inner painter component
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   250
    val painter = text_area.getPainter
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   251
    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
   252
      val offset = text_area.xyToOffset(x, y, false)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   253
      if (offset >= 0) {
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   254
        val range = point_range(text_area.getBuffer, offset)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   255
        gfx_range(text_area, range) match {
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   256
          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
   257
          case _ => None
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   258
        }
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   259
      }
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   260
      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
   261
    }
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   262
    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
   263
  }
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
   264
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
   265
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
   266
  /* 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
   267
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   268
  abstract class Pretty_Metric extends Pretty.Metric
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   269
  {
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   270
    def average: Double
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   271
  }
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
   272
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   273
  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   274
    new Pretty_Metric {
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   275
      def string_width(s: String): Double =
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   276
        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   277
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   278
      val unit = string_width(Pretty.space)
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   279
      val average = string_width("mix") / (3 * unit)
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   280
      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
   281
    }
52873
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   282
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   283
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   284
  /* icons */
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   285
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   286
  def load_icon(name: String): Icon =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   287
  {
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   288
    val name1 =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   289
      if (name.startsWith("idea-icons/")) {
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   290
        val file =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   291
          Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   292
        "jar:" + file + "!/" + name
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   293
      }
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   294
      else name
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   295
    val icon = GUIUtilities.loadIcon(name1)
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   296
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   297
    else icon
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   298
  }
52874
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   299
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   300
  def load_image_icon(name: String): ImageIcon =
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   301
    load_icon(name) match {
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   302
      case icon: ImageIcon => icon
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   303
      case _ => error("Bad image icon: " + name)
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   304
    }
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   305
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   306
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   307
  /* key listener */
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   308
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   309
  def key_listener(
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   310
    workaround: Boolean = true,
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   311
    key_typed: KeyEvent => Unit = _ => (),
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   312
    key_pressed: KeyEvent => Unit = _ => (),
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   313
    key_released: KeyEvent => Unit = _ => ()): KeyListener =
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   314
  {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   315
    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   316
    {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   317
      val evt = if (workaround) KeyEventWorkaround.processKeyEvent(evt0) else evt0
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   318
      if (evt != null) handle(evt)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   319
    }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   320
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   321
    new KeyListener
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   322
    {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   323
      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
   324
      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
   325
      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
   326
    }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   327
  }
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   328
}
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   329