src/Tools/jEdit/src/document_view.scala
author wenzelm
Fri Oct 11 20:45:21 2013 +0200 (2013-10-11)
changeset 54325 2c4155003352
parent 53780 ef62204a126b
child 54441 3d37b2957a3e
permissions -rw-r--r--
clarified Editor.current_command: allow outdated snapshot;
more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);
     1 /*  Title:      Tools/jEdit/src/document_view.scala
     2     Author:     Fabian Immler, TU Munich
     3     Author:     Makarius
     4 
     5 Document view connected to jEdit text area.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import scala.collection.mutable
    14 import scala.collection.immutable.SortedMap
    15 import scala.actors.Actor._
    16 
    17 import java.lang.System
    18 import java.text.BreakIterator
    19 import java.awt.{Color, Graphics2D, Point}
    20 import java.awt.event.KeyEvent
    21 import javax.swing.event.{CaretListener, CaretEvent}
    22 
    23 import org.gjt.sp.jedit.{jEdit, Debug}
    24 import org.gjt.sp.jedit.gui.RolloverButton
    25 import org.gjt.sp.jedit.options.GutterOptionPane
    26 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    27 import org.gjt.sp.jedit.syntax.SyntaxStyle
    28 
    29 
    30 object Document_View
    31 {
    32   /* document view of text area */
    33 
    34   private val key = new Object
    35 
    36   def apply(text_area: JEditTextArea): Option[Document_View] =
    37   {
    38     Swing_Thread.require()
    39     text_area.getClientProperty(key) match {
    40       case doc_view: Document_View => Some(doc_view)
    41       case _ => None
    42     }
    43   }
    44 
    45   def exit(text_area: JEditTextArea)
    46   {
    47     Swing_Thread.require()
    48     apply(text_area) match {
    49       case None =>
    50       case Some(doc_view) =>
    51         doc_view.deactivate()
    52         text_area.putClientProperty(key, null)
    53     }
    54   }
    55 
    56   def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    57   {
    58     exit(text_area)
    59     val doc_view = new Document_View(model, text_area)
    60     text_area.putClientProperty(key, doc_view)
    61     doc_view.activate()
    62     doc_view
    63   }
    64 }
    65 
    66 
    67 class Document_View(val model: Document_Model, val text_area: JEditTextArea)
    68 {
    69   private val session = model.session
    70 
    71   def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
    72 
    73   val rich_text_area =
    74     new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
    75       caret_visible = true, enable_hovering = false)
    76 
    77 
    78   /* perspective */
    79 
    80   def perspective(snapshot: Document.Snapshot): Text.Perspective =
    81   {
    82     Swing_Thread.require()
    83 
    84     val active_command =
    85     {
    86       val view = text_area.getView
    87       if (view != null && view.getTextArea == text_area) {
    88         PIDE.editor.current_command(view, snapshot) match {
    89           case Some(command) =>
    90             snapshot.node.command_start(command) match {
    91               case Some(start) => List(command.proper_range + start)
    92               case None => Nil
    93             }
    94           case None => Nil
    95         }
    96       }
    97       else Nil
    98     }
    99 
   100     val buffer_range = JEdit_Lib.buffer_range(model.buffer)
   101     val visible_lines =
   102       (for {
   103         i <- 0 until text_area.getVisibleLines
   104         start = text_area.getScreenLineStartOffset(i)
   105         stop = text_area.getScreenLineEndOffset(i)
   106         if start >= 0 && stop >= 0
   107         range <- buffer_range.try_restrict(Text.Range(start, stop))
   108         if !range.is_singularity
   109       }
   110       yield range).toList
   111 
   112     Text.Perspective(active_command ::: visible_lines)
   113   }
   114 
   115   private def update_perspective = new TextAreaExtension
   116   {
   117     override def paintScreenLineRange(gfx: Graphics2D,
   118       first_line: Int, last_line: Int, physical_lines: Array[Int],
   119       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   120     {
   121       // no robust_body
   122       model.update_perspective()
   123     }
   124   }
   125 
   126 
   127   /* gutter */
   128 
   129   private val gutter_painter = new TextAreaExtension
   130   {
   131     override def paintScreenLineRange(gfx: Graphics2D,
   132       first_line: Int, last_line: Int, physical_lines: Array[Int],
   133       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   134     {
   135       rich_text_area.robust_body(()) {
   136         Swing_Thread.assert()
   137 
   138         val gutter = text_area.getGutter
   139         val width = GutterOptionPane.getSelectionAreaWidth
   140         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   141         val FOLD_MARKER_SIZE = 12
   142 
   143         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   144           val buffer = model.buffer
   145           JEdit_Lib.buffer_lock(buffer) {
   146             val rendering = get_rendering()
   147 
   148             for (i <- 0 until physical_lines.length) {
   149               if (physical_lines(i) != -1) {
   150                 val line_range = Text.Range(start(i), end(i))
   151 
   152                 // gutter icons
   153                 rendering.gutter_message(line_range) match {
   154                   case Some(icon) =>
   155                     val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
   156                     val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
   157                     icon.paintIcon(gutter, gfx, x0, y0)
   158                   case None =>
   159                 }
   160               }
   161             }
   162           }
   163         }
   164       }
   165     }
   166   }
   167 
   168 
   169   /* key listener */
   170 
   171   private val key_listener =
   172     JEdit_Lib.key_listener(
   173       key_pressed = (evt: KeyEvent) =>
   174         {
   175           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
   176             evt.consume
   177         }
   178     )
   179 
   180 
   181   /* caret handling */
   182 
   183   private val delay_caret_update =
   184     Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   185       session.caret_focus.event(Session.Caret_Focus)
   186     }
   187 
   188   private val caret_listener = new CaretListener {
   189     override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
   190   }
   191 
   192 
   193   /* text status overview left of scrollbar */
   194 
   195   private object overview extends Text_Overview(this)
   196   {
   197     val delay_repaint =
   198       Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
   199   }
   200 
   201 
   202   /* main actor */
   203 
   204   private val main_actor = actor {
   205     loop {
   206       react {
   207         case _: Session.Raw_Edits =>
   208           Swing_Thread.later {
   209             overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
   210           }
   211 
   212         case changed: Session.Commands_Changed =>
   213           val buffer = model.buffer
   214           Swing_Thread.later {
   215             JEdit_Lib.buffer_lock(buffer) {
   216               if (model.buffer == text_area.getBuffer) {
   217                 val snapshot = model.snapshot()
   218 
   219                 if (changed.assignment ||
   220                     (changed.nodes.contains(model.node_name) &&
   221                      changed.commands.exists(snapshot.node.commands.contains)))
   222                   Swing_Thread.later { overview.delay_repaint.invoke() }
   223 
   224                 val visible_lines = text_area.getVisibleLines
   225                 if (visible_lines > 0) {
   226                   if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines)
   227                   else {
   228                     val visible_range = JEdit_Lib.visible_range(text_area).get
   229                     val visible_cmds =
   230                       snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   231                     if (visible_cmds.exists(changed.commands)) {
   232                       for {
   233                         line <- 0 until visible_lines
   234                         start = text_area.getScreenLineStartOffset(line) if start >= 0
   235                         end = text_area.getScreenLineEndOffset(line) if end >= 0
   236                         range = Text.Range(start, end)
   237                         line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   238                         if line_cmds.exists(changed.commands)
   239                       } text_area.invalidateScreenLineRange(line, line)
   240                     }
   241                   }
   242                 }
   243               }
   244             }
   245           }
   246 
   247         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   248       }
   249     }
   250   }
   251 
   252 
   253   /* activation */
   254 
   255   private def activate()
   256   {
   257     val painter = text_area.getPainter
   258 
   259     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
   260     rich_text_area.activate()
   261     text_area.getGutter.addExtension(gutter_painter)
   262     text_area.addKeyListener(key_listener)
   263     text_area.addCaretListener(caret_listener)
   264     text_area.addLeftOfScrollBar(overview)
   265     session.raw_edits += main_actor
   266     session.commands_changed += main_actor
   267   }
   268 
   269   private def deactivate()
   270   {
   271     val painter = text_area.getPainter
   272 
   273     session.raw_edits -= main_actor
   274     session.commands_changed -= main_actor
   275     text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
   276     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   277     text_area.removeKeyListener(key_listener)
   278     text_area.getGutter.removeExtension(gutter_painter)
   279     rich_text_area.deactivate()
   280     painter.removeExtension(update_perspective)
   281   }
   282 }