src/Tools/jEdit/src/document_view.scala
author wenzelm
Wed Aug 24 13:03:39 2011 +0200 (2011-08-24 ago)
changeset 44436 546adfa8a6fc
parent 44379 1079ab6b342b
child 44437 bebe15799192
permissions -rw-r--r--
update_perspective without actual edits, bypassing the full state assignment protocol;
edit_nodes/Perspective: do not touch_descendants here;
propagate editor scroll events via update_perspective;
misc tuning;
     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.actors.Actor._
    15 
    16 import java.lang.System
    17 import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
    18 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
    19   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    20 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
    21 import javax.swing.event.{CaretListener, CaretEvent}
    22 
    23 import org.gjt.sp.util.Log
    24 
    25 import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
    26 import org.gjt.sp.jedit.gui.RolloverButton
    27 import org.gjt.sp.jedit.options.GutterOptionPane
    28 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
    29   ScrollListener}
    30 import org.gjt.sp.jedit.syntax.{SyntaxStyle}
    31 
    32 
    33 object Document_View
    34 {
    35   /* document view of text area */
    36 
    37   private val key = new Object
    38 
    39   def apply(text_area: JEditTextArea): Option[Document_View] =
    40   {
    41     Swing_Thread.require()
    42     text_area.getClientProperty(key) match {
    43       case doc_view: Document_View => Some(doc_view)
    44       case _ => None
    45     }
    46   }
    47 
    48   def exit(text_area: JEditTextArea)
    49   {
    50     Swing_Thread.require()
    51     apply(text_area) match {
    52       case None =>
    53       case Some(doc_view) =>
    54         doc_view.deactivate()
    55         text_area.putClientProperty(key, null)
    56     }
    57   }
    58 
    59   def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    60   {
    61     exit(text_area)
    62     val doc_view = new Document_View(model, text_area)
    63     text_area.putClientProperty(key, doc_view)
    64     doc_view.activate()
    65     doc_view
    66   }
    67 }
    68 
    69 
    70 class Document_View(val model: Document_Model, val text_area: JEditTextArea)
    71 {
    72   private val session = model.session
    73 
    74 
    75   /* robust extension body */
    76 
    77   def robust_body[A](default: A)(body: => A): A =
    78   {
    79     try {
    80       Swing_Thread.require()
    81       if (model.buffer == text_area.getBuffer) body
    82       else {
    83         Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
    84         default
    85       }
    86     }
    87     catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
    88   }
    89 
    90 
    91   /* visible text range */
    92 
    93   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    94   // NB: jEdit already normalizes \r\n and \r to \n
    95   def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
    96   {
    97     val stop = if (start < end) end - 1 else end min model.buffer.getLength
    98     Text.Range(start, stop)
    99   }
   100 
   101   def visible_range(): Text.Range =
   102   {
   103     val start = text_area.getScreenLineStartOffset(0)
   104     val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
   105     proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
   106   }
   107 
   108   def invalidate_range(range: Text.Range)
   109   {
   110     text_area.invalidateLineRange(
   111       model.buffer.getLineOfOffset(range.start),
   112       model.buffer.getLineOfOffset(range.stop))
   113   }
   114 
   115 
   116   /* perspective */
   117 
   118   def perspective(): Text.Perspective =
   119   {
   120     Swing_Thread.require()
   121     Text.perspective(
   122       for {
   123         i <- 0 until text_area.getVisibleLines
   124         val start = text_area.getScreenLineStartOffset(i)
   125         val stop = text_area.getScreenLineEndOffset(i)
   126         if start >= 0 && stop >= 0
   127       }
   128       yield Text.Range(start, stop))
   129   }
   130 
   131 
   132   /* snapshot */
   133 
   134   // owned by Swing thread
   135   @volatile private var was_outdated = false
   136   @volatile private var was_updated = false
   137 
   138   def update_snapshot(): Document.Snapshot =
   139   {
   140     Swing_Thread.require()
   141     val snapshot = model.snapshot()
   142     was_updated = was_outdated && !snapshot.is_outdated
   143     was_outdated = was_outdated || snapshot.is_outdated
   144     snapshot
   145   }
   146 
   147   def flush_snapshot(): (Boolean, Document.Snapshot) =
   148   {
   149     Swing_Thread.require()
   150     val snapshot = update_snapshot()
   151     val updated = was_updated
   152     if (updated) { was_outdated = false; was_updated = false }
   153     (updated, snapshot)
   154   }
   155 
   156 
   157   /* HTML popups */
   158 
   159   private var html_popup: Option[Popup] = None
   160 
   161   private def exit_popup() { html_popup.map(_.hide) }
   162 
   163   private val html_panel =
   164     new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   165   html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
   166 
   167   private def html_panel_resize()
   168   {
   169     Swing_Thread.now {
   170       html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   171     }
   172   }
   173 
   174   private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
   175   {
   176     exit_popup()
   177 /* FIXME broken
   178     val offset = text_area.xyToOffset(x, y)
   179     val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
   180 
   181     // FIXME snapshot.cumulate
   182     snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
   183       case Text.Info(_, Some(msg)) #:: _ =>
   184         val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
   185         html_panel.render_sync(List(msg))
   186         Thread.sleep(10)  // FIXME !?
   187         popup.show
   188         html_popup = Some(popup)
   189       case _ =>
   190     }
   191 */
   192   }
   193 
   194 
   195   /* subexpression highlighting */
   196 
   197   private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
   198     : Option[(Text.Range, Color)] =
   199   {
   200     val offset = text_area.xyToOffset(x, y)
   201     snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
   202       case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   203       case _ => None
   204     }
   205   }
   206 
   207   @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
   208   def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
   209 
   210 
   211   /* CONTROL-mouse management */
   212 
   213   private var control: Boolean = false
   214 
   215   private def exit_control()
   216   {
   217     exit_popup()
   218     _highlight_range = None
   219   }
   220 
   221   private val focus_listener = new FocusAdapter {
   222     override def focusLost(e: FocusEvent) {
   223       _highlight_range = None // FIXME exit_control !?
   224     }
   225   }
   226 
   227   private val window_listener = new WindowAdapter {
   228     override def windowIconified(e: WindowEvent) { exit_control() }
   229     override def windowDeactivated(e: WindowEvent) { exit_control() }
   230   }
   231 
   232   private val mouse_motion_listener = new MouseMotionAdapter {
   233     override def mouseMoved(e: MouseEvent) {
   234       control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   235       val x = e.getX()
   236       val y = e.getY()
   237 
   238       if (!model.buffer.isLoaded) exit_control()
   239       else
   240         Isabelle.swing_buffer_lock(model.buffer) {
   241           val snapshot = update_snapshot()
   242 
   243           if (control) init_popup(snapshot, x, y)
   244 
   245           _highlight_range map { case (range, _) => invalidate_range(range) }
   246           _highlight_range = if (control) subexp_range(snapshot, x, y) else None
   247           _highlight_range map { case (range, _) => invalidate_range(range) }
   248         }
   249     }
   250   }
   251 
   252 
   253   /* text area painting */
   254 
   255   private val text_area_painter = new Text_Area_Painter(this)
   256 
   257   private val tooltip_painter = new TextAreaExtension
   258   {
   259     override def getToolTipText(x: Int, y: Int): String =
   260     {
   261       robust_body(null: String) {
   262         val snapshot = update_snapshot()
   263         val offset = text_area.xyToOffset(x, y)
   264         if (control) {
   265           snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
   266           {
   267             case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   268             case _ => null
   269           }
   270         }
   271         else {
   272           // FIXME snapshot.cumulate
   273           snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
   274           {
   275             case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   276             case _ => null
   277           }
   278         }
   279       }
   280     }
   281   }
   282 
   283   private val gutter_painter = new TextAreaExtension
   284   {
   285     override def paintScreenLineRange(gfx: Graphics2D,
   286       first_line: Int, last_line: Int, physical_lines: Array[Int],
   287       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   288     {
   289       robust_body(()) {
   290         val gutter = text_area.getGutter
   291         val width = GutterOptionPane.getSelectionAreaWidth
   292         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   293         val FOLD_MARKER_SIZE = 12
   294 
   295         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   296           Isabelle.swing_buffer_lock(model.buffer) {
   297             val snapshot = update_snapshot()
   298             for (i <- 0 until physical_lines.length) {
   299               if (physical_lines(i) != -1) {
   300                 val line_range = proper_line_range(start(i), end(i))
   301 
   302                 // gutter icons
   303                 val icons =
   304                   (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
   305                     snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
   306                   yield icon).toList.sortWith(_ >= _)
   307                 icons match {
   308                   case icon :: _ =>
   309                     val icn = icon.icon
   310                     val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
   311                     val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
   312                     icn.paintIcon(gutter, gfx, x0, y0)
   313                   case Nil =>
   314                 }
   315               }
   316             }
   317           }
   318         }
   319       }
   320     }
   321   }
   322 
   323 
   324   /* caret range */
   325 
   326   def caret_range(): Text.Range =
   327     Isabelle.buffer_lock(model.buffer) {
   328       def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
   329       val caret = text_area.getCaretPosition
   330       try {
   331         val c = text(caret)
   332         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
   333           Text.Range(caret, caret + 2)
   334         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
   335           Text.Range(caret - 1, caret + 1)
   336         else Text.Range(caret, caret + 1)
   337       }
   338       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
   339     }
   340 
   341 
   342   /* caret handling */
   343 
   344   def selected_command(): Option[Command] =
   345   {
   346     Swing_Thread.require()
   347     update_snapshot().node.proper_command_at(text_area.getCaretPosition)
   348   }
   349 
   350   private val caret_listener = new CaretListener {
   351     private val delay = Swing_Thread.delay_last(session.input_delay) {
   352       session.perspective.event(Session.Perspective)
   353     }
   354     override def caretUpdate(e: CaretEvent) { delay() }
   355   }
   356 
   357 
   358   /* scrolling */
   359 
   360   private val scroll_listener = new ScrollListener
   361   {
   362     def scrolledVertically(arg: TextArea) { model.update_perspective() }
   363     def scrolledHorizontally(arg: TextArea) { }
   364   }
   365 
   366 
   367   /* overview of command status left of scrollbar */
   368 
   369   private val overview = new JPanel(new BorderLayout)
   370   {
   371     private val WIDTH = 10
   372     private val HEIGHT = 2
   373 
   374     setPreferredSize(new Dimension(WIDTH, 0))
   375 
   376     setRequestFocusEnabled(false)
   377 
   378     addMouseListener(new MouseAdapter {
   379       override def mousePressed(event: MouseEvent) {
   380         val line = y_to_line(event.getY)
   381         if (line >= 0 && line < text_area.getLineCount)
   382           text_area.setCaretPosition(text_area.getLineStartOffset(line))
   383       }
   384     })
   385 
   386     override def addNotify() {
   387       super.addNotify()
   388       ToolTipManager.sharedInstance.registerComponent(this)
   389     }
   390 
   391     override def removeNotify() {
   392       ToolTipManager.sharedInstance.unregisterComponent(this)
   393       super.removeNotify
   394     }
   395 
   396     override def paintComponent(gfx: Graphics)
   397     {
   398       super.paintComponent(gfx)
   399       Swing_Thread.assert()
   400 
   401       val buffer = model.buffer
   402       Isabelle.buffer_lock(buffer) {
   403         val snapshot = update_snapshot()
   404 
   405         def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
   406         {
   407           try {
   408             val line1 = buffer.getLineOfOffset(snapshot.convert(start))
   409             val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
   410             Some((line1, line2))
   411           }
   412           catch { case e: ArrayIndexOutOfBoundsException => None }
   413         }
   414         for {
   415           (command, start) <- snapshot.node.command_starts
   416           if !command.is_ignored
   417           (line1, line2) <- line_range(command, start)
   418           val y = line_to_y(line1)
   419           val height = HEIGHT * (line2 - line1)
   420           color <- Isabelle_Markup.overview_color(snapshot, command)
   421         } {
   422           gfx.setColor(color)
   423           gfx.fillRect(0, y, getWidth - 1, height)
   424         }
   425       }
   426     }
   427 
   428     private def line_to_y(line: Int): Int =
   429       (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   430 
   431     private def y_to_line(y: Int): Int =
   432       (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   433   }
   434 
   435 
   436   /* main actor */
   437 
   438   private val main_actor = actor {
   439     loop {
   440       react {
   441         case Session.Commands_Changed(changed) =>
   442           val buffer = model.buffer
   443           Isabelle.swing_buffer_lock(buffer) {
   444             val (updated, snapshot) = flush_snapshot()
   445             val visible = visible_range()
   446 
   447             if (updated || changed.exists(snapshot.node.commands.contains))
   448               overview.repaint()
   449 
   450             if (updated) invalidate_range(visible)
   451             else {
   452               val visible_cmds =
   453                 snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
   454               if (visible_cmds.exists(changed)) {
   455                 for {
   456                   line <- 0 until text_area.getVisibleLines
   457                   val start = text_area.getScreenLineStartOffset(line) if start >= 0
   458                   val end = text_area.getScreenLineEndOffset(line) if end >= 0
   459                   val range = proper_line_range(start, end)
   460                   val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   461                   if line_cmds.exists(changed)
   462                 } text_area.invalidateScreenLineRange(line, line)
   463               }
   464             }
   465           }
   466 
   467         case Session.Global_Settings => html_panel_resize()
   468 
   469         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   470       }
   471     }
   472   }
   473 
   474 
   475   /* activation */
   476 
   477   private def activate()
   478   {
   479     val painter = text_area.getPainter
   480     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
   481     text_area_painter.activate()
   482     text_area.getGutter.addExtension(gutter_painter)
   483     text_area.addFocusListener(focus_listener)
   484     text_area.getView.addWindowListener(window_listener)
   485     painter.addMouseMotionListener(mouse_motion_listener)
   486     text_area.addCaretListener(caret_listener)
   487     text_area.addScrollListener(scroll_listener)
   488     text_area.addLeftOfScrollBar(overview)
   489     session.commands_changed += main_actor
   490     session.global_settings += main_actor
   491   }
   492 
   493   private def deactivate()
   494   {
   495     val painter = text_area.getPainter
   496     session.commands_changed -= main_actor
   497     session.global_settings -= main_actor
   498     text_area.removeFocusListener(focus_listener)
   499     text_area.getView.removeWindowListener(window_listener)
   500     painter.removeMouseMotionListener(mouse_motion_listener)
   501     text_area.removeCaretListener(caret_listener)
   502     text_area.removeScrollListener(scroll_listener)
   503     text_area.removeLeftOfScrollBar(overview)
   504     text_area.getGutter.removeExtension(gutter_painter)
   505     text_area_painter.deactivate()
   506     painter.removeExtension(tooltip_painter)
   507     exit_popup()
   508   }
   509 }