src/Tools/jEdit/src/document_view.scala
author wenzelm
Fri Sep 21 15:39:51 2012 +0200 (2012-09-21)
changeset 49492 2e3e7ea5ce8e
parent 49424 491363c6feb4
child 49843 afddf4e26fac
permissions -rw-r--r--
some support for hovering and sendback area;
     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 javax.swing.event.{CaretListener, CaretEvent}
    21 
    22 import org.gjt.sp.jedit.{jEdit, Debug}
    23 import org.gjt.sp.jedit.gui.RolloverButton
    24 import org.gjt.sp.jedit.options.GutterOptionPane
    25 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    26 import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    27 
    28 
    29 object Document_View
    30 {
    31   /* document view of text area */
    32 
    33   private val key = new Object
    34 
    35   def apply(text_area: JEditTextArea): Option[Document_View] =
    36   {
    37     Swing_Thread.require()
    38     text_area.getClientProperty(key) match {
    39       case doc_view: Document_View => Some(doc_view)
    40       case _ => None
    41     }
    42   }
    43 
    44   def exit(text_area: JEditTextArea)
    45   {
    46     Swing_Thread.require()
    47     apply(text_area) match {
    48       case None =>
    49       case Some(doc_view) =>
    50         doc_view.deactivate()
    51         text_area.putClientProperty(key, null)
    52     }
    53   }
    54 
    55   def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    56   {
    57     exit(text_area)
    58     val doc_view = new Document_View(model, text_area)
    59     text_area.putClientProperty(key, doc_view)
    60     doc_view.activate()
    61     doc_view
    62   }
    63 }
    64 
    65 
    66 class Document_View(val model: Document_Model, val text_area: JEditTextArea)
    67 {
    68   private val session = model.session
    69 
    70   def get_rendering(): Isabelle_Rendering =
    71     Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    72 
    73   val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
    74 
    75 
    76   /* perspective */
    77 
    78   def perspective(): Text.Perspective =
    79   {
    80     Swing_Thread.require()
    81     val buffer_range = model.buffer_range()
    82     Text.Perspective(
    83       for {
    84         i <- 0 until text_area.getVisibleLines
    85         start = text_area.getScreenLineStartOffset(i)
    86         stop = text_area.getScreenLineEndOffset(i)
    87         if start >= 0 && stop >= 0
    88         range <- buffer_range.try_restrict(Text.Range(start, stop))
    89         if !range.is_singularity
    90       }
    91       yield range)
    92   }
    93 
    94   private def update_perspective = new TextAreaExtension
    95   {
    96     override def paintScreenLineRange(gfx: Graphics2D,
    97       first_line: Int, last_line: Int, physical_lines: Array[Int],
    98       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    99     {
   100       // no robust_body
   101       model.update_perspective()
   102     }
   103   }
   104 
   105 
   106   /* gutter */
   107 
   108   private val gutter_painter = new TextAreaExtension
   109   {
   110     override def paintScreenLineRange(gfx: Graphics2D,
   111       first_line: Int, last_line: Int, physical_lines: Array[Int],
   112       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   113     {
   114       rich_text_area.robust_body(()) {
   115         Swing_Thread.assert()
   116 
   117         val gutter = text_area.getGutter
   118         val width = GutterOptionPane.getSelectionAreaWidth
   119         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   120         val FOLD_MARKER_SIZE = 12
   121 
   122         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   123           val buffer = model.buffer
   124           JEdit_Lib.buffer_lock(buffer) {
   125             val rendering = get_rendering()
   126 
   127             for (i <- 0 until physical_lines.length) {
   128               if (physical_lines(i) != -1) {
   129                 val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
   130 
   131                 // gutter icons
   132                 rendering.gutter_message(line_range) match {
   133                   case Some(icon) =>
   134                     val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
   135                     val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
   136                     icon.paintIcon(gutter, gfx, x0, y0)
   137                   case None =>
   138                 }
   139               }
   140             }
   141           }
   142         }
   143       }
   144     }
   145   }
   146 
   147 
   148   /* caret handling */
   149 
   150   private val delay_caret_update =
   151     Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
   152       session.caret_focus.event(Session.Caret_Focus)
   153     }
   154 
   155   private val caret_listener = new CaretListener {
   156     override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
   157   }
   158 
   159 
   160   /* text status overview left of scrollbar */
   161 
   162   private object overview extends Text_Overview(this)
   163   {
   164     val delay_repaint =
   165       Swing_Thread.delay_first(
   166         Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
   167   }
   168 
   169 
   170   /* main actor */
   171 
   172   private val main_actor = actor {
   173     loop {
   174       react {
   175         case _: Session.Raw_Edits =>
   176           Swing_Thread.later {
   177             overview.delay_repaint.postpone(
   178               Time.seconds(Isabelle.options.real("editor_input_delay")))
   179           }
   180 
   181         case changed: Session.Commands_Changed =>
   182           val buffer = model.buffer
   183           Swing_Thread.later {
   184             JEdit_Lib.buffer_lock(buffer) {
   185               if (model.buffer == text_area.getBuffer) {
   186                 val snapshot = model.snapshot()
   187 
   188                 if (changed.assignment ||
   189                     (changed.nodes.contains(model.name) &&
   190                      changed.commands.exists(snapshot.node.commands.contains)))
   191                   Swing_Thread.later { overview.delay_repaint.invoke() }
   192 
   193                 JEdit_Lib.visible_range(text_area) match {
   194                   case Some(visible) =>
   195                     if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
   196                     else {
   197                       val visible_cmds =
   198                         snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
   199                       if (visible_cmds.exists(changed.commands)) {
   200                         for {
   201                           line <- 0 until text_area.getVisibleLines
   202                           start = text_area.getScreenLineStartOffset(line) if start >= 0
   203                           end = text_area.getScreenLineEndOffset(line) if end >= 0
   204                           range = JEdit_Lib.proper_line_range(buffer, start, end)
   205                           line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   206                           if line_cmds.exists(changed.commands)
   207                         } text_area.invalidateScreenLineRange(line, line)
   208                       }
   209                     }
   210                   case None =>
   211                 }
   212               }
   213             }
   214           }
   215 
   216         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   217       }
   218     }
   219   }
   220 
   221 
   222   /* activation */
   223 
   224   private def activate()
   225   {
   226     val painter = text_area.getPainter
   227 
   228     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
   229     rich_text_area.activate()
   230     text_area.getGutter.addExtension(gutter_painter)
   231     text_area.addCaretListener(caret_listener)
   232     text_area.addLeftOfScrollBar(overview)
   233     session.raw_edits += main_actor
   234     session.commands_changed += main_actor
   235   }
   236 
   237   private def deactivate()
   238   {
   239     val painter = text_area.getPainter
   240 
   241     session.raw_edits -= main_actor
   242     session.commands_changed -= main_actor
   243     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   244     text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
   245     text_area.getGutter.removeExtension(gutter_painter)
   246     rich_text_area.deactivate()
   247     painter.removeExtension(update_perspective)
   248   }
   249 }