src/Tools/jEdit/src/document_view.scala
author wenzelm
Thu, 29 Aug 2013 12:38:33 +0200
changeset 53274 1760c01f1c78
parent 53272 0dfd78ff7696
child 53780 ef62204a126b
permissions -rw-r--r--
maintain Completion_Popup.Text_Area as client property like Document_View; global Completion_Popup.Text_Area init/exit like SideKickPlugin; eliminated old SideKick completion -- cover all Isabelle modes uniformly; dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 42839
diff changeset
     1
/*  Title:      Tools/jEdit/src/document_view.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Fabian Immler, TU Munich
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     4
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     5
Document view connected to jEdit text area.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     6
*/
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     7
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
     8
package isabelle.jedit
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
     9
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    10
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    11
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34871
diff changeset
    12
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    13
import scala.collection.mutable
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 44805
diff changeset
    14
import scala.collection.immutable.SortedMap
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    15
import scala.actors.Actor._
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    16
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43510
diff changeset
    17
import java.lang.System
45744
0ad063afa3d6 caret_range based on BreakIterator, which handles combined unicode characters as well;
wenzelm
parents: 45665
diff changeset
    18
import java.text.BreakIterator
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
    19
import java.awt.{Color, Graphics2D, Point}
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53179
diff changeset
    20
import java.awt.event.KeyEvent
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    21
import javax.swing.event.{CaretListener, CaretEvent}
34734
wenzelm
parents: 34733
diff changeset
    22
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49408
diff changeset
    23
import org.gjt.sp.jedit.{jEdit, Debug}
34709
2f0c18f9b6c7 minor tuning;
wenzelm
parents: 34679
diff changeset
    24
import org.gjt.sp.jedit.gui.RolloverButton
39176
b8fdd3ae8815 Document_View: more precise painting of gutter icons, only if line selection area is sufficiently large;
wenzelm
parents: 39175
diff changeset
    25
import org.gjt.sp.jedit.options.GutterOptionPane
47392
6a08fd7a6071 tuned imports;
wenzelm
parents: 47027
diff changeset
    26
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
52479
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
    27
import org.gjt.sp.jedit.syntax.SyntaxStyle
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    28
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    29
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    30
object Document_View
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    31
{
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    32
  /* document view of text area */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    33
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    34
  private val key = new Object
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    35
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
    36
  def apply(text_area: JEditTextArea): Option[Document_View] =
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    37
  {
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
    38
    Swing_Thread.require()
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    39
    text_area.getClientProperty(key) match {
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    40
      case doc_view: Document_View => Some(doc_view)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    41
      case _ => None
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    42
    }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    43
  }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    44
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
    45
  def exit(text_area: JEditTextArea)
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    46
  {
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
    47
    Swing_Thread.require()
34788
3779c54a2d21 direct apply for Document_Model and Document_View;
wenzelm
parents: 34784
diff changeset
    48
    apply(text_area) match {
39636
610dc743932c permissive exit;
wenzelm
parents: 39182
diff changeset
    49
      case None =>
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    50
      case Some(doc_view) =>
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    51
        doc_view.deactivate()
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    52
        text_area.putClientProperty(key, null)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    53
    }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    54
  }
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    55
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    56
  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    57
  {
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    58
    exit(text_area)
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    59
    val doc_view = new Document_View(model, text_area)
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    60
    text_area.putClientProperty(key, doc_view)
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    61
    doc_view.activate()
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    62
    doc_view
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    63
  }
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    64
}
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
    65
34733
a3ad6d51db1d misc tuning and unification;
wenzelm
parents: 34711
diff changeset
    66
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43369
diff changeset
    67
class Document_View(val model: Document_Model, val text_area: JEditTextArea)
34654
30f588245884 arbitrary history
immler@in.tum.de
parents: 34653
diff changeset
    68
{
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    69
  private val session = model.session
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    70
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50199
diff changeset
    71
  def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
    72
50306
b655d2d0406d updated to jedit-5.0.0;
wenzelm
parents: 50207
diff changeset
    73
  val rich_text_area =
50915
12de8ea66f54 close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);
wenzelm
parents: 50770
diff changeset
    74
    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
53179
336cd976698c tuned signature;
wenzelm
parents: 52973
diff changeset
    75
      caret_visible = true, enable_hovering = false)
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
    76
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
    77
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    78
  /* perspective */
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    79
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    80
  def perspective(): Text.Perspective =
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    81
  {
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    82
    Swing_Thread.require()
50363
2f8dc9e65401 tuned signature in accordance to document operations;
wenzelm
parents: 50306
diff changeset
    83
    val buffer_range = JEdit_Lib.buffer_range(model.buffer)
44473
4f264fdf8d0e slightly more abstract Text.Perspective;
wenzelm
parents: 44437
diff changeset
    84
    Text.Perspective(
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    85
      for {
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    86
        i <- 0 until text_area.getVisibleLines
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
    87
        start = text_area.getScreenLineStartOffset(i)
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
    88
        stop = text_area.getScreenLineEndOffset(i)
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    89
        if start >= 0 && stop >= 0
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
    90
        range <- buffer_range.try_restrict(Text.Range(start, stop))
44583
022509c908fb restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);
wenzelm
parents: 44473
diff changeset
    91
        if !range.is_singularity
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    92
      }
44583
022509c908fb restrict perspective to actual buffer_range, to avoid spurious edits due to faulty last_exec_offset (NB: jEdit screenlines may be silently extended by trailing newline);
wenzelm
parents: 44473
diff changeset
    93
      yield range)
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    94
  }
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
    95
44437
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
    96
  private def update_perspective = new TextAreaExtension
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
    97
  {
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
    98
    override def paintScreenLineRange(gfx: Graphics2D,
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
    99
      first_line: Int, last_line: Int, physical_lines: Array[Int],
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   100
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   101
    {
49424
491363c6feb4 more robust GUI component handlers;
wenzelm
parents: 49411
diff changeset
   102
      // no robust_body
52767
9c28559e5fff back to model.update_perspective with delay (cf. a20631db9c8a);
wenzelm
parents: 52759
diff changeset
   103
      model.update_perspective()
44437
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   104
    }
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   105
  }
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   106
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   107
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
   108
  /* gutter */
34513
411017e76e98 respect current offsets
immler@in.tum.de
parents: 34503
diff changeset
   109
42825
wenzelm
parents: 40338
diff changeset
   110
  private val gutter_painter = new TextAreaExtension
39175
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   111
  {
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   112
    override def paintScreenLineRange(gfx: Graphics2D,
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   113
      first_line: Int, last_line: Int, physical_lines: Array[Int],
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   114
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   115
    {
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
   116
      rich_text_area.robust_body(()) {
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   117
        Swing_Thread.assert()
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   118
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   119
        val gutter = text_area.getGutter
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   120
        val width = GutterOptionPane.getSelectionAreaWidth
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   121
        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   122
        val FOLD_MARKER_SIZE = 12
43419
6ed49c52d463 flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
wenzelm
parents: 43417
diff changeset
   123
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   124
        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
49408
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   125
          val buffer = model.buffer
3cfc114acd05 tuned signature;
wenzelm
parents: 49407
diff changeset
   126
          JEdit_Lib.buffer_lock(buffer) {
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49408
diff changeset
   127
            val rendering = get_rendering()
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49288
diff changeset
   128
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   129
            for (i <- 0 until physical_lines.length) {
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   130
              if (physical_lines(i) != -1) {
49843
afddf4e26fac further refinement of jEdit line range, avoiding lack of final \n;
wenzelm
parents: 49492
diff changeset
   131
                val line_range = Text.Range(start(i), end(i))
43419
6ed49c52d463 flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
wenzelm
parents: 43417
diff changeset
   132
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   133
                // gutter icons
49356
6e0c0ffb6ec7 more static handling of rendering options;
wenzelm
parents: 49288
diff changeset
   134
                rendering.gutter_message(line_range) match {
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   135
                  case Some(icon) =>
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46205
diff changeset
   136
                    val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46205
diff changeset
   137
                    val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46205
diff changeset
   138
                    icon.paintIcon(gutter, gfx, x0, y0)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   139
                  case None =>
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   140
                }
39175
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   141
              }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   142
            }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   143
          }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   144
        }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   145
      }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   146
    }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   147
  }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   148
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   149
52479
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   150
  /* key listener */
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   151
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53179
diff changeset
   152
  private val key_listener =
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53179
diff changeset
   153
    JEdit_Lib.key_listener(
53227
68cc55ceb7f6 more standard key handling according to jEdit (with workaround);
wenzelm
parents: 53226
diff changeset
   154
      key_pressed = (evt: KeyEvent) =>
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53179
diff changeset
   155
        {
53244
ec6011bf2362 dismiss popups more uniformly;
wenzelm
parents: 53242
diff changeset
   156
          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53179
diff changeset
   157
            evt.consume
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
   158
        }
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53179
diff changeset
   159
    )
52479
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   160
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   161
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   162
  /* caret handling */
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   163
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   164
  private val delay_caret_update =
50207
54be125d8cdc tuned signature;
wenzelm
parents: 50205
diff changeset
   165
    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
44805
48a5c104d434 clarified terminology;
wenzelm
parents: 44776
diff changeset
   166
      session.caret_focus.event(Session.Caret_Focus)
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   167
    }
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   168
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   169
  private val caret_listener = new CaretListener {
49195
9d10bd85c1be more explicit Delay operations;
wenzelm
parents: 48921
diff changeset
   170
    override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   171
  }
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   172
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   173
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
   174
  /* text status overview left of scrollbar */
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   175
47993
135fd6f2dadd less warning in scala-2.10.0-M3;
wenzelm
parents: 47392
diff changeset
   176
  private object overview extends Text_Overview(this)
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
   177
  {
46571
edcccd7a9eee overview.delay_repaint: avoid wasting GUI cycles via update_delay;
wenzelm
parents: 46550
diff changeset
   178
    val delay_repaint =
50207
54be125d8cdc tuned signature;
wenzelm
parents: 50205
diff changeset
   179
      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   180
  }
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
   181
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   182
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   183
  /* main actor */
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   184
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   185
  private val main_actor = actor {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   186
    loop {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   187
      react {
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   188
        case _: Session.Raw_Edits =>
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   189
          Swing_Thread.later {
50207
54be125d8cdc tuned signature;
wenzelm
parents: 50205
diff changeset
   190
            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   191
          }
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   192
44608
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44583
diff changeset
   193
        case changed: Session.Commands_Changed =>
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   194
          val buffer = model.buffer
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   195
          Swing_Thread.later {
49406
38db4832b210 somewhat more general JEdit_Lib;
wenzelm
parents: 49360
diff changeset
   196
            JEdit_Lib.buffer_lock(buffer) {
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   197
              if (model.buffer == text_area.getBuffer) {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   198
                val snapshot = model.snapshot()
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   199
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   200
                if (changed.assignment ||
52973
d5f7fa1498b7 tuned signature;
wenzelm
parents: 52767
diff changeset
   201
                    (changed.nodes.contains(model.node_name) &&
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   202
                     changed.commands.exists(snapshot.node.commands.contains)))
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   203
                  Swing_Thread.later { overview.delay_repaint.invoke() }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   204
50770
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   205
                val visible_lines = text_area.getVisibleLines
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   206
                if (visible_lines > 0) {
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   207
                  if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   208
                  else {
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   209
                    val visible_range = JEdit_Lib.visible_range(text_area).get
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   210
                    val visible_cmds =
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   211
                      snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   212
                    if (visible_cmds.exists(changed.commands)) {
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   213
                      for {
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   214
                        line <- 0 until visible_lines
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   215
                        start = text_area.getScreenLineStartOffset(line) if start >= 0
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   216
                        end = text_area.getScreenLineEndOffset(line) if end >= 0
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   217
                        range = Text.Range(start, end)
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   218
                        line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   219
                        if line_cmds.exists(changed.commands)
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   220
                      } text_area.invalidateScreenLineRange(line, line)
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   221
                    }
50770
82d48783fd7a more direct invalidateScreenLineRange after changed assignment;
wenzelm
parents: 50363
diff changeset
   222
                  }
46583
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   223
                }
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   224
              }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   225
            }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   226
          }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   227
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   228
        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   229
      }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   230
    }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   231
  }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   232
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   233
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   234
  /* activation */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   235
34808
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34806
diff changeset
   236
  private def activate()
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   237
  {
42825
wenzelm
parents: 40338
diff changeset
   238
    val painter = text_area.getPainter
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49408
diff changeset
   239
44437
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   240
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
   241
    rich_text_area.activate()
42825
wenzelm
parents: 40338
diff changeset
   242
    text_area.getGutter.addExtension(gutter_painter)
52479
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   243
    text_area.addKeyListener(key_listener)
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   244
    text_area.addCaretListener(caret_listener)
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   245
    text_area.addLeftOfScrollBar(overview)
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   246
    session.raw_edits += main_actor
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   247
    session.commands_changed += main_actor
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   248
  }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   249
34808
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34806
diff changeset
   250
  private def deactivate()
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   251
  {
42825
wenzelm
parents: 40338
diff changeset
   252
    val painter = text_area.getPainter
49410
34acbcc33adf tuned signature -- more general Text_Area_Painter operations;
wenzelm
parents: 49408
diff changeset
   253
49196
1d63ceb0d177 postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
wenzelm
parents: 49195
diff changeset
   254
    session.raw_edits -= main_actor
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   255
    session.commands_changed -= main_actor
52479
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   256
    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
49195
9d10bd85c1be more explicit Delay operations;
wenzelm
parents: 48921
diff changeset
   257
    text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
52479
bb516d01d259 more aggresive ESCAPE handling, while retaining its regular meaning for jEdit;
wenzelm
parents: 50915
diff changeset
   258
    text_area.removeKeyListener(key_listener)
42825
wenzelm
parents: 40338
diff changeset
   259
    text_area.getGutter.removeExtension(gutter_painter)
49411
1da54e9bda68 renamed Text_Area_Painter to Rich_Text_Area;
wenzelm
parents: 49410
diff changeset
   260
    rich_text_area.deactivate()
44437
bebe15799192 more reliable update_perspective handler based on actual text visibility (e.g. on startup or when resizing without scrolling);
wenzelm
parents: 44436
diff changeset
   261
    painter.removeExtension(update_perspective)
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   262
  }
42825
wenzelm
parents: 40338
diff changeset
   263
}