src/Tools/jEdit/src/document_view.scala
author wenzelm
Sat, 07 Apr 2012 17:49:20 +0200
changeset 47392 6a08fd7a6071
parent 47027 fc3bb6c02a3c
child 47993 135fd6f2dadd
permissions -rw-r--r--
tuned imports;
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}
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
    20
import java.awt.event.{MouseMotionAdapter, MouseEvent,
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
    21
  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
    22
import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    23
import javax.swing.event.{CaretListener, CaretEvent}
34734
wenzelm
parents: 34733
diff changeset
    24
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    25
import org.gjt.sp.util.Log
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    26
42839
19df8385f38d basic support for overpainting of text, imitating jEdit internals;
wenzelm
parents: 42838
diff changeset
    27
import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
34709
2f0c18f9b6c7 minor tuning;
wenzelm
parents: 34679
diff changeset
    28
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
    29
import org.gjt.sp.jedit.options.GutterOptionPane
47392
6a08fd7a6071 tuned imports;
wenzelm
parents: 47027
diff changeset
    30
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
43369
4c86b3405010 separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents: 43282
diff changeset
    31
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
    32
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
object Document_View
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    35
{
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    36
  /* 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
    37
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    38
  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
    39
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
    40
  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
    41
  {
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
    42
    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
    43
    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
    44
      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
    45
      case _ => None
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    46
    }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    47
  }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    48
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
    49
  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
    50
  {
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
    51
    Swing_Thread.require()
34788
3779c54a2d21 direct apply for Document_Model and Document_View;
wenzelm
parents: 34784
diff changeset
    52
    apply(text_area) match {
39636
610dc743932c permissive exit;
wenzelm
parents: 39182
diff changeset
    53
      case None =>
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    54
      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
    55
        doc_view.deactivate()
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    56
        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
    57
    }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    58
  }
43397
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    59
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    60
  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    61
  {
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    62
    exit(text_area)
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    63
    val doc_view = new Document_View(model, text_area)
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    64
    text_area.putClientProperty(key, doc_view)
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    65
    doc_view.activate()
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    66
    doc_view
dba359c0ae3b more robust init;
wenzelm
parents: 43393
diff changeset
    67
  }
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    68
}
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
    69
34733
a3ad6d51db1d misc tuning and unification;
wenzelm
parents: 34711
diff changeset
    70
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43369
diff changeset
    71
class Document_View(val model: Document_Model, val text_area: JEditTextArea)
34654
30f588245884 arbitrary history
immler@in.tum.de
parents: 34653
diff changeset
    72
{
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
    73
  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
    74
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
    75
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
    76
  /* robust extension body */
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    77
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    78
  def robust_body[A](default: A)(body: => A): A =
43417
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    79
  {
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    80
    try {
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    81
      Swing_Thread.require()
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    82
      if (model.buffer == text_area.getBuffer) body
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    83
      else {
43650
f00da558b78e imitate exception ERROR of Isabelle/ML;
wenzelm
parents: 43520
diff changeset
    84
        Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
43417
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    85
        default
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    86
      }
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    87
    }
43417
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    88
    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
83be997a11d6 more precise imitation of original TextAreaPainter: no locking;
wenzelm
parents: 43414
diff changeset
    89
  }
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    90
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
    91
44378
81b4af4cfa5a tuned signature;
wenzelm
parents: 43661
diff changeset
    92
  /* visible text range */
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
    93
46815
6bccb1dc9bc3 tuned comment;
wenzelm
parents: 46814
diff changeset
    94
  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
    95
  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
46812
3d55ef732cd7 clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";
wenzelm
parents: 46740
diff changeset
    96
    Text.Range(start, end min model.buffer.getLength)
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
    97
46583
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
    98
  def visible_range(): Option[Text.Range] =
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
    99
  {
46583
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   100
    val n = text_area.getVisibleLines
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   101
    if (n > 0) {
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   102
      val start = text_area.getScreenLineStartOffset(0)
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   103
      val raw_end = text_area.getScreenLineEndOffset(n - 1)
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   104
      Some(proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength))
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   105
    }
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   106
    else None
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
   107
  }
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
   108
44378
81b4af4cfa5a tuned signature;
wenzelm
parents: 43661
diff changeset
   109
  def invalidate_range(range: Text.Range)
39132
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   110
  {
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   111
    text_area.invalidateLineRange(
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   112
      model.buffer.getLineOfOffset(range.start),
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   113
      model.buffer.getLineOfOffset(range.stop))
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   114
  }
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   115
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
   116
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   117
  /* perspective */
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   118
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   119
  def perspective(): Text.Perspective =
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   120
  {
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   121
    Swing_Thread.require()
44776
47e8c8daccae added "check" button: adhoc change to full buffer perspective;
wenzelm
parents: 44615
diff changeset
   122
    val buffer_range = model.buffer_range()
44473
4f264fdf8d0e slightly more abstract Text.Perspective;
wenzelm
parents: 44437
diff changeset
   123
    Text.Perspective(
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   124
      for {
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   125
        i <- 0 until text_area.getVisibleLines
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   126
        start = text_area.getScreenLineStartOffset(i)
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   127
        stop = text_area.getScreenLineEndOffset(i)
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   128
        if start >= 0 && stop >= 0
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   129
        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
   130
        if !range.is_singularity
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   131
      }
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
   132
      yield range)
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   133
  }
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   134
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
   135
  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
   136
  {
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
   137
    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
   138
      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
   139
      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
   140
    {
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
   141
      model.update_perspective()
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
   142
    }
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
   143
  }
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
   144
44379
1079ab6b342b added official Text.Range.Ordering;
wenzelm
parents: 44378
diff changeset
   145
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   146
  /* HTML popups */
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   147
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   148
  private var html_popup: Option[Popup] = None
34834
df9af932e418 slightly more uniform/robust handling of visible document;
wenzelm
parents: 34832
diff changeset
   149
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   150
  private def exit_popup() { html_popup.map(_.hide) }
38881
c8123e77acc5 tuned commands_changed_actor: more precise/efficient handling of visible screen lines;
wenzelm
parents: 38880
diff changeset
   151
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   152
  private val html_panel =
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43650
diff changeset
   153
    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   154
  html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
38884
9ec5f6010d6e Document_View: repaint overview for any command change of this node (again);
wenzelm
parents: 38883
diff changeset
   155
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   156
  private def html_panel_resize()
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   157
  {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   158
    Swing_Thread.now {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   159
      html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   160
    }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   161
  }
38884
9ec5f6010d6e Document_View: repaint overview for any command change of this node (again);
wenzelm
parents: 38883
diff changeset
   162
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   163
  private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   164
  {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   165
    exit_popup()
40154
e11da4ec9d74 disable broken popups for now;
wenzelm
parents: 39742
diff changeset
   166
/* FIXME broken
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   167
    val offset = text_area.xyToOffset(x, y)
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   168
    val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   169
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   170
    // FIXME snapshot.cumulate
45665
129db1416717 renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents: 45467
diff changeset
   171
    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.popup) match {
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   172
      case Text.Info(_, Some(msg)) #:: _ =>
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   173
        val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   174
        html_panel.render_sync(List(msg))
39742
b59e064e32c3 CONTROL-mouse management: handle windowDeactivated as well;
wenzelm
parents: 39741
diff changeset
   175
        Thread.sleep(10)  // FIXME !?
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   176
        popup.show
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   177
        html_popup = Some(popup)
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   178
      case _ =>
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
   179
    }
40154
e11da4ec9d74 disable broken popups for now;
wenzelm
parents: 39742
diff changeset
   180
*/
34678
acaac03ced00 tuned whitespace
immler@in.tum.de
parents: 34654
diff changeset
   181
  }
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
   182
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
   183
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   184
  /* subexpression highlighting */
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   185
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   186
  @volatile private var _highlight_range: Option[Text.Info[Color]] = None
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   187
  def highlight_range(): Option[Text.Info[Color]] = _highlight_range
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   188
40338
e2f03de2b3c7 clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents: 40154
diff changeset
   189
  private var control: Boolean = false
e2f03de2b3c7 clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents: 40154
diff changeset
   190
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   191
  private def exit_control()
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   192
  {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   193
    exit_popup()
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   194
    _highlight_range = None
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   195
  }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   196
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   197
  private val focus_listener = new FocusAdapter {
39742
b59e064e32c3 CONTROL-mouse management: handle windowDeactivated as well;
wenzelm
parents: 39741
diff changeset
   198
    override def focusLost(e: FocusEvent) {
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   199
      _highlight_range = None // FIXME exit_control !?
39742
b59e064e32c3 CONTROL-mouse management: handle windowDeactivated as well;
wenzelm
parents: 39741
diff changeset
   200
    }
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   201
  }
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   202
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   203
  private val window_listener = new WindowAdapter {
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   204
    override def windowIconified(e: WindowEvent) { exit_control() }
39742
b59e064e32c3 CONTROL-mouse management: handle windowDeactivated as well;
wenzelm
parents: 39741
diff changeset
   205
    override def windowDeactivated(e: WindowEvent) { exit_control() }
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   206
  }
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   207
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   208
  private val mouse_motion_listener = new MouseMotionAdapter {
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   209
    override def mouseMoved(e: MouseEvent) {
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   210
      Swing_Thread.assert()
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   211
40338
e2f03de2b3c7 clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents: 40154
diff changeset
   212
      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   213
      val x = e.getX()
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   214
      val y = e.getY()
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   215
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   216
      if (!model.buffer.isLoaded) exit_control()
39132
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   217
      else
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   218
        Isabelle.buffer_lock(model.buffer) {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   219
          val snapshot = model.snapshot()
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   220
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   221
          if (control) init_popup(snapshot, x, y)
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   222
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   223
          for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   224
          _highlight_range =
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   225
            if (control) {
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   226
              val offset = text_area.xyToOffset(x, y)
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   227
              Isabelle_Rendering.subexp(snapshot, Text.Range(offset, offset + 1))
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   228
            }
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   229
            else None
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46178
diff changeset
   230
          for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
39132
ba17ca3acdd3 refined treatment of multi-line subexpressions;
wenzelm
parents: 39131
diff changeset
   231
        }
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   232
    }
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   233
  }
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   234
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   235
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   236
  /* text area painting */
39044
5c13736e81c7 Document_View: squiggly underline for messages;
wenzelm
parents: 38886
diff changeset
   237
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   238
  private val text_area_painter = new Text_Area_Painter(this)
39700
fa55cf2c1ae4 more precise treatment of backgrounds vs. rectangles;
wenzelm
parents: 39690
diff changeset
   239
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   240
  private val tooltip_painter = new TextAreaExtension
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   241
  {
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   242
    override def getToolTipText(x: Int, y: Int): String =
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   243
    {
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   244
      robust_body(null: String) {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   245
        val snapshot = model.snapshot()
38845
a9e37daf5bd0 added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents: 38843
diff changeset
   246
        val offset = text_area.xyToOffset(x, y)
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 44805
diff changeset
   247
        val range = Text.Range(offset, offset + 1)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   248
        val tip =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   249
          if (control) Isabelle_Rendering.tooltip(snapshot, range)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   250
          else Isabelle_Rendering.tooltip_message(snapshot, range)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   251
        tip.map(Isabelle.tooltip(_)) getOrElse null
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   252
      }
34734
wenzelm
parents: 34733
diff changeset
   253
    }
34678
acaac03ced00 tuned whitespace
immler@in.tum.de
parents: 34654
diff changeset
   254
  }
34513
411017e76e98 respect current offsets
immler@in.tum.de
parents: 34503
diff changeset
   255
42825
wenzelm
parents: 40338
diff changeset
   256
  private val gutter_painter = new TextAreaExtension
39175
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   257
  {
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   258
    override def paintScreenLineRange(gfx: Graphics2D,
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   259
      first_line: Int, last_line: Int, physical_lines: Array[Int],
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   260
      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   261
    {
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   262
      robust_body(()) {
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   263
        Swing_Thread.assert()
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   264
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   265
        val gutter = text_area.getGutter
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   266
        val width = GutterOptionPane.getSelectionAreaWidth
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   267
        val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   268
        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
   269
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   270
        if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
46920
5f44c8bea84e more explicit indication of swing thread context;
wenzelm
parents: 46918
diff changeset
   271
          Isabelle.buffer_lock(model.buffer) {
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   272
            val snapshot = model.snapshot()
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   273
            for (i <- 0 until physical_lines.length) {
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   274
              if (physical_lines(i) != -1) {
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   275
                val line_range = proper_line_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
   276
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   277
                // gutter icons
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   278
                Isabelle_Rendering.gutter_message(snapshot, line_range) match {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   279
                  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
   280
                    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
   281
                    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
   282
                    icon.paintIcon(gutter, gfx, x0, y0)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 45744
diff changeset
   283
                  case None =>
43404
c8369f3d88a1 uniform use of Document_View.robust_body;
wenzelm
parents: 43397
diff changeset
   284
                }
39175
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   285
              }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   286
            }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   287
          }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   288
        }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   289
      }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   290
    }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   291
  }
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   292
a08d68e993ea basic support for warning/error gutter icons;
wenzelm
parents: 39174
diff changeset
   293
43448
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43419
diff changeset
   294
  /* caret range */
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43419
diff changeset
   295
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43419
diff changeset
   296
  def caret_range(): Text.Range =
46229
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   297
    Isabelle.buffer_lock(model.buffer) {
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   298
      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   299
      val caret = text_area.getCaretPosition
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   300
      try {
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   301
        val c = text(caret)
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   302
        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   303
          Text.Range(caret, caret + 2)
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   304
        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   305
          Text.Range(caret - 1, caret + 1)
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   306
        else Text.Range(caret, caret + 1)
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   307
      }
d8286601e7df back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;
wenzelm
parents: 46227
diff changeset
   308
      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
43448
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43419
diff changeset
   309
    }
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43419
diff changeset
   310
90aec5043461 more robust caret painting wrt. surrogate characters;
wenzelm
parents: 43419
diff changeset
   311
37129
4c83696b340e Command.toString: include id for debugging;
wenzelm
parents: 36990
diff changeset
   312
  /* caret handling */
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   313
37849
4f9de312cc23 Session: predefined real time parameters;
wenzelm
parents: 37685
diff changeset
   314
  def selected_command(): Option[Command] =
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
   315
  {
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
   316
    Swing_Thread.require()
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   317
    model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
38223
2a368e8e0a80 more explicit treatment of Swing thread context;
wenzelm
parents: 38158
diff changeset
   318
  }
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   319
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   320
  private val delay_caret_update =
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   321
    Swing_Thread.delay_last(session.input_delay) {
44805
48a5c104d434 clarified terminology;
wenzelm
parents: 44776
diff changeset
   322
      session.caret_focus.event(Session.Caret_Focus)
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   323
    }
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   324
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   325
  private val caret_listener = new CaretListener {
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   326
    override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   327
  }
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   328
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   329
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
   330
  /* 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
   331
46572
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
   332
  private val overview = new Text_Overview(this)
3074685ab7ed separate module for text status overview;
wenzelm
parents: 46571
diff changeset
   333
  {
46571
edcccd7a9eee overview.delay_repaint: avoid wasting GUI cycles via update_delay;
wenzelm
parents: 46550
diff changeset
   334
    val delay_repaint =
edcccd7a9eee overview.delay_repaint: avoid wasting GUI cycles via update_delay;
wenzelm
parents: 46550
diff changeset
   335
      Swing_Thread.delay_first(Isabelle.session.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
   336
  }
34403
6c812a3cb170 information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff changeset
   337
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   338
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   339
  /* main actor */
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   340
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   341
  private val main_actor = actor {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   342
    loop {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   343
      react {
44608
76c2e3ddc183 tuned Commands_Changed: cover nodes as well;
wenzelm
parents: 44583
diff changeset
   344
        case changed: Session.Commands_Changed =>
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   345
          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
   346
          Swing_Thread.later {
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   347
            Isabelle.buffer_lock(buffer) {
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   348
              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
   349
                val snapshot = model.snapshot()
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   350
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   351
                if (changed.assignment ||
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   352
                    (changed.nodes.contains(model.name) &&
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   353
                     changed.commands.exists(snapshot.node.commands.contains)))
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   354
                  overview.delay_repaint(true)
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   355
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   356
                visible_range() match {
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   357
                  case Some(visible) =>
47027
fc3bb6c02a3c explicit propagation of assignment event, even if changed command set is empty;
wenzelm
parents: 47013
diff changeset
   358
                    if (changed.assignment) invalidate_range(visible)
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   359
                    else {
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   360
                      val visible_cmds =
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   361
                        snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   362
                      if (visible_cmds.exists(changed.commands)) {
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   363
                        for {
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   364
                          line <- 0 until text_area.getVisibleLines
46997
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   365
                          start = text_area.getScreenLineStartOffset(line) if start >= 0
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   366
                          end = text_area.getScreenLineEndOffset(line) if end >= 0
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   367
                          range = proper_line_range(start, end)
395b7277ed76 misc tuning to accomodate scala-2.10.0-M2;
wenzelm
parents: 46920
diff changeset
   368
                          line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   369
                          if line_cmds.exists(changed.commands)
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   370
                        } text_area.invalidateScreenLineRange(line, line)
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   371
                      }
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   372
                    }
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   373
                  case None =>
46583
926957a621dd more robust visible_range: allow empty view;
wenzelm
parents: 46572
diff changeset
   374
                }
46918
1752164d916b prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents: 46815
diff changeset
   375
              }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   376
            }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   377
          }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   378
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   379
        case Session.Global_Settings => html_panel_resize()
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   380
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   381
        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
   382
      }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   383
    }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   384
  }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   385
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   386
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   387
  /* activation */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   388
34808
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34806
diff changeset
   389
  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
   390
  {
42825
wenzelm
parents: 40338
diff changeset
   391
    val painter = text_area.getPainter
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
   392
    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
43387
a59ae768249e recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);
wenzelm
parents: 43381
diff changeset
   393
    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   394
    text_area_painter.activate()
42825
wenzelm
parents: 40338
diff changeset
   395
    text_area.getGutter.addExtension(gutter_painter)
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   396
    text_area.addFocusListener(focus_listener)
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   397
    text_area.getView.addWindowListener(window_listener)
42825
wenzelm
parents: 40338
diff changeset
   398
    painter.addMouseMotionListener(mouse_motion_listener)
34810
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   399
    text_area.addCaretListener(caret_listener)
9ad3431a34a5 tuned caret_listener/selected_command;
wenzelm
parents: 34808
diff changeset
   400
    text_area.addLeftOfScrollBar(overview)
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   401
    session.commands_changed += main_actor
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   402
    session.global_settings += main_actor
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   403
  }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   404
34808
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34806
diff changeset
   405
  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
   406
  {
42825
wenzelm
parents: 40338
diff changeset
   407
    val painter = text_area.getPainter
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   408
    session.commands_changed -= main_actor
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   409
    session.global_settings -= main_actor
39131
947c62440026 basic support for subexpression highlighting (see also gatchan.jedit.hyperlinks.HyperlinkManager/HyperlinkTextAreaPainter);
wenzelm
parents: 39044
diff changeset
   410
    text_area.removeFocusListener(focus_listener)
39741
62b91eb2d39a CONTROL-mouse management: handle windowIconified;
wenzelm
parents: 39740
diff changeset
   411
    text_area.getView.removeWindowListener(window_listener)
42825
wenzelm
parents: 40338
diff changeset
   412
    painter.removeMouseMotionListener(mouse_motion_listener)
46740
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   413
    text_area.removeCaretListener(caret_listener); delay_caret_update(false)
852baa599351 explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents: 46583
diff changeset
   414
    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
42825
wenzelm
parents: 40338
diff changeset
   415
    text_area.getGutter.removeExtension(gutter_painter)
43381
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   416
    text_area_painter.deactivate()
806878ae2219 separate module for text area painting;
wenzelm
parents: 43376
diff changeset
   417
    painter.removeExtension(tooltip_painter)
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
   418
    painter.removeExtension(update_perspective)
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39737
diff changeset
   419
    exit_popup()
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34777
diff changeset
   420
  }
42825
wenzelm
parents: 40338
diff changeset
   421
}