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