src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Wed, 03 Mar 2021 21:37:20 +0100
changeset 73354 79b120d1c1a3
parent 73340 0ffcad1f6130
child 73367 77ef8bef0593
permissions -rw-r--r--
tuned --- fewer warnings;
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
65469
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    12
import java.io.{File => JFile}
72899
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
    13
import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit}
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
    14
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
    15
import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
49710
21d88a631fcc refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents: 49409
diff changeset
    16
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56774
diff changeset
    17
import scala.util.parsing.input.CharSequenceReader
73354
79b120d1c1a3 tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
    18
import scala.jdk.CollectionConverters._
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    19
62264
340f98836fd9 re-init document views for the sake of Text_Overview size;
wenzelm
parents: 61865
diff changeset
    20
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
72927
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
    21
import org.gjt.sp.jedit.io.{FileVFS, VFSManager}
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
    22
import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
61192
98eba31c51f8 tuned signature;
wenzelm
parents: 60992
diff changeset
    23
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
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
    24
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    25
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    26
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    27
object JEdit_Lib
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    28
{
71861
1330fa4a2b85 clarified signature;
wenzelm
parents: 71601
diff changeset
    29
  /* jEdit directories */
1330fa4a2b85 clarified signature;
wenzelm
parents: 71601
diff changeset
    30
1330fa4a2b85 clarified signature;
wenzelm
parents: 71601
diff changeset
    31
  def directories: List[JFile] =
1330fa4a2b85 clarified signature;
wenzelm
parents: 71601
diff changeset
    32
    (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
1330fa4a2b85 clarified signature;
wenzelm
parents: 71601
diff changeset
    33
1330fa4a2b85 clarified signature;
wenzelm
parents: 71601
diff changeset
    34
53019
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    35
  /* window geometry measurement */
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    36
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    37
  private lazy val dummy_window = new JWindow
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    38
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    39
  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
    40
  {
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    41
    def deco_width: Int = width - inner_width
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    42
    def deco_height: Int = height - inner_height
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    43
  }
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    44
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    45
  def window_geometry(outer: Container, inner: Component): Window_Geometry =
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    46
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56930
diff changeset
    47
    GUI_Thread.require {}
53019
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    48
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    49
    val old_content = dummy_window.getContentPane
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    50
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    51
    dummy_window.setContentPane(outer)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    52
    dummy_window.pack
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    53
    dummy_window.revalidate
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    54
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    55
    val geometry =
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    56
      Window_Geometry(
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    57
        dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    58
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    59
    dummy_window.setContentPane(old_content)
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    60
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    61
    geometry
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    62
  }
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    63
be9e94594b96 more general window_geometry;
wenzelm
parents: 53003
diff changeset
    64
65469
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    65
  /* files */
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    66
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    67
  def is_file(name: String): Boolean =
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    68
    VFSManager.getVFSForPath(name).isInstanceOf[FileVFS]
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    69
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    70
  def check_file(name: String): Option[JFile] =
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    71
    if (is_file(name)) Some(new JFile(name)) else None
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    72
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    73
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    74
  /* buffers */
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    75
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    76
  def buffer_text(buffer: JEditBuffer): String =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    77
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    78
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56774
diff changeset
    79
  def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
64824
330ec9bc4b75 tuned signature;
wenzelm
parents: 64770
diff changeset
    80
    Scan.char_reader(buffer.getSegment(0, buffer.getLength))
56823
37be55461dbe more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents: 56774
diff changeset
    81
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    82
  def buffer_mode(buffer: JEditBuffer): String =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    83
  {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    84
    val mode = buffer.getMode
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    85
    if (mode == null) ""
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    86
    else {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    87
      val name = mode.getName
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    88
      if (name == null) "" else name
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    89
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    90
  }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53247
diff changeset
    91
65469
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    92
  def buffer_line_manager(buffer: JEditBuffer): LineManager =
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    93
    Untyped.get[LineManager](buffer, "lineMgr")
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    94
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    95
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
    96
65469
78ace4a14975 more explicit jEdit file operations;
wenzelm
parents: 64824
diff changeset
    97
  def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
61192
98eba31c51f8 tuned signature;
wenzelm
parents: 60992
diff changeset
    98
68060
3931ed905e93 avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents: 67014
diff changeset
    99
  def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A =
3931ed905e93 avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents: 67014
diff changeset
   100
  {
3931ed905e93 avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents: 67014
diff changeset
   101
    val undo_in_progress = buffer.isUndoInProgress
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   102
    def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
68060
3931ed905e93 avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents: 67014
diff changeset
   103
    try { set(true); body } finally { set(undo_in_progress) }
3931ed905e93 avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents: 67014
diff changeset
   104
  }
3931ed905e93 avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
wenzelm
parents: 67014
diff changeset
   105
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   106
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   107
  /* main jEdit components */
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   108
73354
79b120d1c1a3 tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   109
  def jedit_buffers(): Iterator[Buffer] =
79b120d1c1a3 tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   110
    jEdit.getBufferManager().getBuffers().asScala.iterator
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   111
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   112
  def jedit_buffer(name: String): Option[Buffer] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   113
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   114
56457
eea4bbe15745 tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents: 55812
diff changeset
   115
  def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
eea4bbe15745 tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents: 55812
diff changeset
   116
    jedit_buffer(name.node)
eea4bbe15745 tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents: 55812
diff changeset
   117
73354
79b120d1c1a3 tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   118
  def jedit_views(): Iterator[View] =
79b120d1c1a3 tuned --- fewer warnings;
wenzelm
parents: 73340
diff changeset
   119
    jEdit.getViewManager().getViews().asScala.iterator
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   120
69636
dd1e0e1570d2 clarified signature;
wenzelm
parents: 69380
diff changeset
   121
  def jedit_view(view: View = null): View =
dd1e0e1570d2 clarified signature;
wenzelm
parents: 69380
diff changeset
   122
    if (view == null) jEdit.getActiveView() else view
dd1e0e1570d2 clarified signature;
wenzelm
parents: 69380
diff changeset
   123
62264
340f98836fd9 re-init document views for the sake of Text_Overview size;
wenzelm
parents: 61865
diff changeset
   124
  def jedit_edit_panes(view: View): Iterator[EditPane] =
340f98836fd9 re-init document views for the sake of Text_Overview size;
wenzelm
parents: 61865
diff changeset
   125
    if (view == null) Iterator.empty
340f98836fd9 re-init document views for the sake of Text_Overview size;
wenzelm
parents: 61865
diff changeset
   126
    else view.getEditPanes().iterator.filter(_ != null)
340f98836fd9 re-init document views for the sake of Text_Overview size;
wenzelm
parents: 61865
diff changeset
   127
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   128
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56574
diff changeset
   129
    if (view == null) Iterator.empty
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56574
diff changeset
   130
    else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   131
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   132
  def jedit_text_areas(): Iterator[JEditTextArea] =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71502
diff changeset
   133
    jedit_views().flatMap(jedit_text_areas)
49406
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(buffer: JEditBuffer): Iterator[JEditTextArea] =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   136
    jedit_text_areas().filter(_.getBuffer == buffer)
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   137
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   138
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   139
  {
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   140
    try { buffer.readLock(); body }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   141
    finally { buffer.readUnlock() }
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   142
  }
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   143
50195
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   144
  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   145
  {
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   146
    try { buffer.beginCompoundEdit(); body }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   147
    finally { buffer.endCompoundEdit() }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   148
  }
863b1dfc396c prefer buffer_edit combinator over Java-style boilerplate;
wenzelm
parents: 50186
diff changeset
   149
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   150
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   151
  /* get text */
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   152
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66592
diff changeset
   153
  def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
50215
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   154
    try { Some(buffer.getText(range.start, range.length)) }
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   155
    catch { case _: ArrayIndexOutOfBoundsException => None }
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   156
97959912840a more general sendback properties;
wenzelm
parents: 50195
diff changeset
   157
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   158
  /* point range */
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   159
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   160
  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
56592
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   161
    if (offset < 0) Text.Range.offside
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   162
    else
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   163
      buffer_lock(buffer) {
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   164
        def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   165
        try {
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   166
          val c = text(offset)
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   167
          if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   168
            Text.Range(offset, offset + 2)
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   169
          else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   170
            Text.Range(offset - 1, offset + 1)
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   171
          else
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   172
            Text.Range(offset, offset + 1)
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   173
        }
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   174
        catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
49407
215ba6884bdf tuned signature;
wenzelm
parents: 49406
diff changeset
   175
      }
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   176
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   177
55812
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   178
  /* text ranges */
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   179
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   180
  def buffer_range(buffer: JEditBuffer): Text.Range =
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   181
    Text.Range(0, buffer.getLength)
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   182
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56574
diff changeset
   183
  def line_range(buffer: JEditBuffer, line: Int): Text.Range =
56589
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   184
    Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56574
diff changeset
   185
56592
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   186
  def caret_range(text_area: TextArea): Text.Range =
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   187
    point_range(text_area.getBuffer, text_area.getCaretPosition)
5157f7615e99 prefer direct caret_range for update_dictionary actions, which usually happen outside the flow of editing;
wenzelm
parents: 56589
diff changeset
   188
49408
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
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   202
  def invalidate_range(text_area: TextArea, range: Text.Range): Unit =
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   203
  {
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   204
    val buffer = text_area.getBuffer
55812
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   205
    buffer_range(buffer).try_restrict(range) match {
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   206
      case Some(range1) if !range1.is_singularity =>
56699
60ad80f5cb62 further robustification wrt. unclear ranges;
wenzelm
parents: 56662
diff changeset
   207
        try {
60ad80f5cb62 further robustification wrt. unclear ranges;
wenzelm
parents: 56662
diff changeset
   208
          text_area.invalidateLineRange(
60ad80f5cb62 further robustification wrt. unclear ranges;
wenzelm
parents: 56662
diff changeset
   209
            buffer.getLineOfOffset(range1.start),
60ad80f5cb62 further robustification wrt. unclear ranges;
wenzelm
parents: 56662
diff changeset
   210
            buffer.getLineOfOffset(range1.stop))
60ad80f5cb62 further robustification wrt. unclear ranges;
wenzelm
parents: 56662
diff changeset
   211
        }
60ad80f5cb62 further robustification wrt. unclear ranges;
wenzelm
parents: 56662
diff changeset
   212
        catch { case _: ArrayIndexOutOfBoundsException => }
55812
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   213
      case _ =>
59fcd209cc0c more regular buffer_range, despite 47e8c8daccae;
wenzelm
parents: 55767
diff changeset
   214
    }
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   215
  }
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   216
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   217
  def invalidate(text_area: TextArea): Unit =
62986
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62264
diff changeset
   218
  {
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62264
diff changeset
   219
    val visible_lines = text_area.getVisibleLines
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62264
diff changeset
   220
    if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62264
diff changeset
   221
  }
9d2fae6b31cc background color for entity def/ref focus;
wenzelm
parents: 62264
diff changeset
   222
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   223
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   224
  /* graphics range */
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   225
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59571
diff changeset
   226
  case class Gfx_Range(x: Int, y: Int, length: Int)
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   227
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49712
diff changeset
   228
  // NB: jEdit always normalizes \r\n and \r to \n
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   229
  // NB: last line lacks \n
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   230
  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   231
  {
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   232
    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
   233
    val char_width = (metric.unit * metric.average).round.toInt
50849
70f7483df9cb more uniform Pretty.char_width;
wenzelm
parents: 50658
diff changeset
   234
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   235
    val buffer = text_area.getBuffer
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   236
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   237
    val end = buffer.getLength
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   238
    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
   239
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
   240
    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
   241
      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
   242
        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
   243
        val (q, r) =
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66592
diff changeset
   244
          if (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
   245
            (text_area.offsetToXY(stop - 1), char_width)
55549
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
   246
          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
   247
            (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
   248
          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
   249
        (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
   250
      }
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
   251
      catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   252
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   253
    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
50115
8cde6f1a0106 tuned signature;
wenzelm
parents: 49941
diff changeset
   254
      Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
49409
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   255
    else None
7140a738aa49 tuned signature;
wenzelm
parents: 49408
diff changeset
   256
  }
49941
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   257
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   258
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   259
  /* pixel range */
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   260
f2db0596bd61 more precise pixel_range: avoid popup when pointing into empty space after actual end-of-line;
wenzelm
parents: 49843
diff changeset
   261
  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
   262
  {
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   263
    // coordinates wrt. inner painter component
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   264
    val painter = text_area.getPainter
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   265
    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
   266
      val offset = text_area.xyToOffset(x, y, false)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   267
      if (offset >= 0) {
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   268
        val range = point_range(text_area.getBuffer, offset)
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   269
        gfx_range(text_area, range) match {
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59571
diff changeset
   270
          case Some(g) if g.x <= x && x < g.x + g.length => Some(range)
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   271
          case _ => None
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   272
        }
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   273
      }
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   274
      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
   275
    }
53183
018d71bee930 strict checking of coordinates wrt. inner painter component;
wenzelm
parents: 53019
diff changeset
   276
    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
   277
  }
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
   278
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
   279
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
   280
  /* 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
   281
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   282
  abstract class Pretty_Metric extends Pretty.Metric
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   283
  {
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   284
    def average: Double
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   285
  }
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
   286
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   287
  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   288
    new Pretty_Metric {
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   289
      def string_width(s: String): Double =
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   290
        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   291
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71502
diff changeset
   292
      val unit: Double = string_width(Symbol.space) max 1.0
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71502
diff changeset
   293
      val average: Double = string_width("mix") / (3 * unit)
51507
ebd5366e7a42 tuned signature;
wenzelm
parents: 51492
diff changeset
   294
      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
   295
    }
52873
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   296
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   297
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   298
  /* icons */
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   299
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   300
  def load_icon(name: String): Icon =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   301
  {
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   302
    val name1 =
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   303
      if (name.startsWith("idea-icons/")) {
64770
1ddc262514b8 more robust, notably on Windows;
wenzelm
parents: 64730
diff changeset
   304
        val file = Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar").file.toURI.toASCIIString
52873
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   305
        "jar:" + file + "!/" + name
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   306
      }
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   307
      else name
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   308
    val icon = GUIUtilities.loadIcon(name1)
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   309
    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   310
    else icon
9e934d4fff00 tuned signature;
wenzelm
parents: 52478
diff changeset
   311
  }
52874
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   312
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   313
  def load_image_icon(name: String): ImageIcon =
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   314
    load_icon(name) match {
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   315
      case icon: ImageIcon => icon
91032244e4ca query process animation;
wenzelm
parents: 52873
diff changeset
   316
      case _ => error("Bad image icon: " + name)
91032244e4ca query process animation;
wenzelm
parents: 52873
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
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
   320
  /* 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
   321
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   322
  def request_focus_view(alt_view: View = null): Unit =
66592
cc93f86e005f tuned signature;
wenzelm
parents: 66591
diff changeset
   323
    isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view)
cc93f86e005f tuned signature;
wenzelm
parents: 66591
diff changeset
   324
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   325
  def propagate_key(view: View, evt: KeyEvent): Unit =
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
   326
  {
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
   327
    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
   328
      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
   329
  }
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   330
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   331
  def key_listener(
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   332
    key_typed: KeyEvent => Unit = _ => (),
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   333
    key_pressed: KeyEvent => Unit = _ => (),
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   334
    key_released: KeyEvent => Unit = _ => ()): KeyListener =
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   335
  {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   336
    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit =
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   337
    {
53237
6bfe54791591 enable jEdit KeyEventWorkaround uniformly;
wenzelm
parents: 53231
diff changeset
   338
      val evt = KeyEventWorkaround.processKeyEvent(evt0)
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   339
      if (evt != null) handle(evt)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   340
    }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   341
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   342
    new KeyListener
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   343
    {
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   344
      def keyTyped(evt: KeyEvent): Unit = process_key_event(evt, key_typed)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   345
      def keyPressed(evt: KeyEvent): Unit = process_key_event(evt, key_pressed)
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 72974
diff changeset
   346
      def keyReleased(evt: KeyEvent): Unit = process_key_event(evt, key_released)
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   347
    }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53183
diff changeset
   348
  }
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   349
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   350
  def special_key(evt: KeyEvent): Boolean =
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   351
  {
59571
1081f91c0662 updated to jedit-5.2.0;
wenzelm
parents: 59077
diff changeset
   352
    // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
71500
a3ed1b0a132f tuned -- avoid deprecated operations;
wenzelm
parents: 71499
diff changeset
   353
    val mod = evt.getModifiersEx
a3ed1b0a132f tuned -- avoid deprecated operations;
wenzelm
parents: 71499
diff changeset
   354
    (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 ||
a3ed1b0a132f tuned -- avoid deprecated operations;
wenzelm
parents: 71499
diff changeset
   355
    (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 &&
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   356
      !Debug.ALT_KEY_PRESSED_DISABLED ||
71500
a3ed1b0a132f tuned -- avoid deprecated operations;
wenzelm
parents: 71499
diff changeset
   357
    (mod & InputEvent.META_DOWN_MASK) != 0
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53712
diff changeset
   358
  }
72899
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
   359
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
   360
  def command_modifier(evt: InputEvent): Boolean =
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
   361
    (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
   362
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
   363
  def shift_modifier(evt: InputEvent): Boolean =
8732315dfafa tuned signature;
wenzelm
parents: 71861
diff changeset
   364
    (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0
72927
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
   365
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
   366
  def modifier_string(evt: InputEvent): String =
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
   367
    KeyEventTranslator.getModifierString(evt) match {
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
   368
      case null => ""
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
   369
      case s => s
69f768aff611 clarified caret focus modifier, depending on option "jedit_focus_modifier";
wenzelm
parents: 72899
diff changeset
   370
    }
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents:
diff changeset
   371
}