src/Tools/jEdit/src/document_view.scala
author wenzelm
Wed Jun 08 17:42:07 2011 +0200 (2011-06-08 ago)
changeset 43282 5d294220ca43
parent 42839 src/Tools/jEdit/src/jedit/document_view.scala@19df8385f38d
child 43369 4c86b3405010
permissions -rw-r--r--
moved sources -- eliminated Netbeans artifact of jedit package directory;
     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.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
    16 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
    17   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    18 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
    19 import javax.swing.event.{CaretListener, CaretEvent}
    20 import java.util.ArrayList
    21 
    22 import org.gjt.sp.jedit.{jEdit, OperatingSystem, 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, DisplayTokenHandler, Chunk, Token}
    27 
    28 
    29 object Document_View
    30 {
    31   /* document view of text area */
    32 
    33   private val key = new Object
    34 
    35   def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    36   {
    37     Swing_Thread.require()
    38     val doc_view = new Document_View(model, text_area)
    39     text_area.putClientProperty(key, doc_view)
    40     doc_view.activate()
    41     doc_view
    42   }
    43 
    44   def apply(text_area: JEditTextArea): Option[Document_View] =
    45   {
    46     Swing_Thread.require()
    47     text_area.getClientProperty(key) match {
    48       case doc_view: Document_View => Some(doc_view)
    49       case _ => None
    50     }
    51   }
    52 
    53   def exit(text_area: JEditTextArea)
    54   {
    55     Swing_Thread.require()
    56     apply(text_area) match {
    57       case None =>
    58       case Some(doc_view) =>
    59         doc_view.deactivate()
    60         text_area.putClientProperty(key, null)
    61     }
    62   }
    63 }
    64 
    65 
    66 class Document_View(val model: Document_Model, text_area: JEditTextArea)
    67 {
    68   private val session = model.session
    69 
    70 
    71   /** token handling **/
    72 
    73   /* extended token styles */
    74 
    75   private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
    76 
    77   def extend_styles()
    78   {
    79     Swing_Thread.require()
    80     styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
    81   }
    82   extend_styles()
    83 
    84   def set_styles()
    85   {
    86     Swing_Thread.require()
    87     text_area.getPainter.setStyles(styles)
    88   }
    89 
    90 
    91   /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
    92 
    93   def wrap_margin(): Int =
    94   {
    95     val buffer = text_area.getBuffer
    96     val painter = text_area.getPainter
    97     val font = painter.getFont
    98     val font_context = painter.getFontRenderContext
    99 
   100     val soft_wrap = buffer.getStringProperty("wrap") == "soft"
   101     val max = buffer.getIntegerProperty("maxLineLen", 0)
   102 
   103     if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   104     else if (soft_wrap)
   105       painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
   106     else 0
   107   }
   108 
   109 
   110   /* chunks */
   111 
   112   def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
   113   {
   114     import scala.collection.JavaConversions._
   115 
   116     val buffer = text_area.getBuffer
   117     val painter = text_area.getPainter
   118     val margin = wrap_margin().toFloat
   119 
   120     val out = new ArrayList[Chunk]
   121     val handler = new DisplayTokenHandler
   122 
   123     var result = Map[Text.Offset, Chunk]()
   124     for (line <- physical_lines) {
   125       out.clear
   126       handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
   127       buffer.markTokens(line, handler)
   128 
   129       val line_start = buffer.getLineStartOffset(line)
   130       for (chunk <- handler.getChunkList.iterator)
   131         result += (line_start + chunk.offset -> chunk)
   132     }
   133     result
   134   }
   135 
   136 
   137   /* visible line ranges */
   138 
   139   // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
   140   // NB: jEdit already normalizes \r\n and \r to \n
   141   def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
   142   {
   143     val stop = if (start < end) end - 1 else end min model.buffer.getLength
   144     Text.Range(start, stop)
   145   }
   146 
   147   def screen_lines_range(): Text.Range =
   148   {
   149     val start = text_area.getScreenLineStartOffset(0)
   150     val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
   151     proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
   152   }
   153 
   154   def invalidate_line_range(range: Text.Range)
   155   {
   156     text_area.invalidateLineRange(
   157       model.buffer.getLineOfOffset(range.start),
   158       model.buffer.getLineOfOffset(range.stop))
   159   }
   160 
   161 
   162   /* HTML popups */
   163 
   164   private var html_popup: Option[Popup] = None
   165 
   166   private def exit_popup() { html_popup.map(_.hide) }
   167 
   168   private val html_panel =
   169     new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   170   html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
   171 
   172   private def html_panel_resize()
   173   {
   174     Swing_Thread.now {
   175       html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   176     }
   177   }
   178 
   179   private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
   180   {
   181     exit_popup()
   182 /* FIXME broken
   183     val offset = text_area.xyToOffset(x, y)
   184     val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
   185 
   186     // FIXME snapshot.cumulate
   187     snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
   188       case Text.Info(_, Some(msg)) #:: _ =>
   189         val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
   190         html_panel.render_sync(List(msg))
   191         Thread.sleep(10)  // FIXME !?
   192         popup.show
   193         html_popup = Some(popup)
   194       case _ =>
   195     }
   196 */
   197   }
   198 
   199 
   200   /* subexpression highlighting */
   201 
   202   private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
   203     : Option[(Text.Range, Color)] =
   204   {
   205     val offset = text_area.xyToOffset(x, y)
   206     snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
   207       case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   208       case _ => None
   209     }
   210   }
   211 
   212   private var highlight_range: Option[(Text.Range, Color)] = None
   213 
   214 
   215   /* CONTROL-mouse management */
   216 
   217   private var control: Boolean = false
   218 
   219   private def exit_control()
   220   {
   221     exit_popup()
   222     highlight_range = None
   223   }
   224 
   225   private val focus_listener = new FocusAdapter {
   226     override def focusLost(e: FocusEvent) {
   227       highlight_range = None // FIXME exit_control !?
   228     }
   229   }
   230 
   231   private val window_listener = new WindowAdapter {
   232     override def windowIconified(e: WindowEvent) { exit_control() }
   233     override def windowDeactivated(e: WindowEvent) { exit_control() }
   234   }
   235 
   236   private val mouse_motion_listener = new MouseMotionAdapter {
   237     override def mouseMoved(e: MouseEvent) {
   238       control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   239       val x = e.getX()
   240       val y = e.getY()
   241 
   242       if (!model.buffer.isLoaded) exit_control()
   243       else
   244         Isabelle.swing_buffer_lock(model.buffer) {
   245           val snapshot = model.snapshot
   246 
   247           if (control) init_popup(snapshot, x, y)
   248 
   249           highlight_range map { case (range, _) => invalidate_line_range(range) }
   250           highlight_range = if (control) subexp_range(snapshot, x, y) else None
   251           highlight_range map { case (range, _) => invalidate_line_range(range) }
   252         }
   253     }
   254   }
   255 
   256 
   257   /* TextArea painters */
   258 
   259   private val background_painter = new TextAreaExtension
   260   {
   261     override def paintScreenLineRange(gfx: Graphics2D,
   262       first_line: Int, last_line: Int, physical_lines: Array[Int],
   263       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   264     {
   265       Isabelle.swing_buffer_lock(model.buffer) {
   266         val snapshot = model.snapshot()
   267         val ascent = text_area.getPainter.getFontMetrics.getAscent
   268 
   269         for (i <- 0 until physical_lines.length) {
   270           if (physical_lines(i) != -1) {
   271             val line_range = proper_line_range(start(i), end(i))
   272 
   273             // background color: status
   274             val cmds = snapshot.node.command_range(snapshot.revert(line_range))
   275             for {
   276               (command, command_start) <- cmds if !command.is_ignored
   277               val range = line_range.restrict(snapshot.convert(command.range + command_start))
   278               r <- Isabelle.gfx_range(text_area, range)
   279               color <- Isabelle_Markup.status_color(snapshot, command)
   280             } {
   281               gfx.setColor(color)
   282               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   283             }
   284 
   285             // background color (1): markup
   286             for {
   287               Text.Info(range, Some(color)) <-
   288                 snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   289               r <- Isabelle.gfx_range(text_area, range)
   290             } {
   291               gfx.setColor(color)
   292               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   293             }
   294 
   295             // background color (2): markup
   296             for {
   297               Text.Info(range, Some(color)) <-
   298                 snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   299               r <- Isabelle.gfx_range(text_area, range)
   300             } {
   301               gfx.setColor(color)
   302               gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   303             }
   304 
   305             // sub-expression highlighting -- potentially from other snapshot
   306             highlight_range match {
   307               case Some((range, color)) if line_range.overlaps(range) =>
   308                 Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   309                   case None =>
   310                   case Some(r) =>
   311                     gfx.setColor(color)
   312                     gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   313                 }
   314               case _ =>
   315             }
   316 
   317             // squiggly underline
   318             for {
   319               Text.Info(range, Some(color)) <-
   320                 snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   321               r <- Isabelle.gfx_range(text_area, range)
   322             } {
   323               gfx.setColor(color)
   324               val x0 = (r.x / 2) * 2
   325               val y0 = r.y + ascent + 1
   326               for (x1 <- Range(x0, x0 + r.length, 2)) {
   327                 val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   328                 gfx.drawLine(x1, y1, x1 + 1, y1)
   329               }
   330             }
   331           }
   332         }
   333       }
   334     }
   335 
   336     override def getToolTipText(x: Int, y: Int): String =
   337     {
   338       Isabelle.swing_buffer_lock(model.buffer) {
   339         val snapshot = model.snapshot()
   340         val offset = text_area.xyToOffset(x, y)
   341         if (control) {
   342           snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
   343           {
   344             case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   345             case _ => null
   346           }
   347         }
   348         else {
   349           // FIXME snapshot.cumulate
   350           snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
   351           {
   352             case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   353             case _ => null
   354           }
   355         }
   356       }
   357     }
   358   }
   359 
   360   var use_text_painter = false
   361 
   362   private val text_painter = new TextAreaExtension
   363   {
   364     override def paintScreenLineRange(gfx: Graphics2D,
   365       first_line: Int, last_line: Int, physical_lines: Array[Int],
   366       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   367     {
   368       if (use_text_painter) {
   369         Isabelle.swing_buffer_lock(model.buffer) {
   370           val painter = text_area.getPainter
   371           val fm = painter.getFontMetrics
   372 
   373           val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
   374 
   375           val x0 = text_area.getHorizontalOffset
   376           var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   377           for (i <- 0 until physical_lines.length) {
   378             if (physical_lines(i) != -1) {
   379               all_chunks.get(start(i)) match {
   380                 case Some(chunk) =>
   381                   Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
   382                 case None =>
   383               }
   384             }
   385             y0 += line_height
   386           }
   387         }
   388       }
   389     }
   390   }
   391 
   392   private val gutter_painter = new TextAreaExtension
   393   {
   394     override def paintScreenLineRange(gfx: Graphics2D,
   395       first_line: Int, last_line: Int, physical_lines: Array[Int],
   396       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   397     {
   398       val gutter = text_area.getGutter
   399       val width = GutterOptionPane.getSelectionAreaWidth
   400       val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   401       val FOLD_MARKER_SIZE = 12
   402 
   403       if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   404         Isabelle.swing_buffer_lock(model.buffer) {
   405           val snapshot = model.snapshot()
   406           for (i <- 0 until physical_lines.length) {
   407             if (physical_lines(i) != -1) {
   408               val line_range = proper_line_range(start(i), end(i))
   409 
   410               // gutter icons
   411               val icons =
   412                 (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
   413                   snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
   414                 yield icon).toList.sortWith(_ >= _)
   415               icons match {
   416                 case icon :: _ =>
   417                   val icn = icon.icon
   418                   val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
   419                   val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
   420                   icn.paintIcon(gutter, gfx, x0, y0)
   421                 case Nil =>
   422               }
   423             }
   424           }
   425         }
   426       }
   427     }
   428   }
   429 
   430 
   431   /* caret handling */
   432 
   433   def selected_command(): Option[Command] =
   434   {
   435     Swing_Thread.require()
   436     model.snapshot().node.proper_command_at(text_area.getCaretPosition)
   437   }
   438 
   439   private val caret_listener = new CaretListener {
   440     private val delay = Swing_Thread.delay_last(session.input_delay) {
   441       session.perspective.event(Session.Perspective)
   442     }
   443     override def caretUpdate(e: CaretEvent) { delay() }
   444   }
   445 
   446 
   447   /* overview of command status left of scrollbar */
   448 
   449   private val overview = new JPanel(new BorderLayout)
   450   {
   451     private val WIDTH = 10
   452     private val HEIGHT = 2
   453 
   454     setPreferredSize(new Dimension(WIDTH, 0))
   455 
   456     setRequestFocusEnabled(false)
   457 
   458     addMouseListener(new MouseAdapter {
   459       override def mousePressed(event: MouseEvent) {
   460         val line = y_to_line(event.getY)
   461         if (line >= 0 && line < text_area.getLineCount)
   462           text_area.setCaretPosition(text_area.getLineStartOffset(line))
   463       }
   464     })
   465 
   466     override def addNotify() {
   467       super.addNotify()
   468       ToolTipManager.sharedInstance.registerComponent(this)
   469     }
   470 
   471     override def removeNotify() {
   472       ToolTipManager.sharedInstance.unregisterComponent(this)
   473       super.removeNotify
   474     }
   475 
   476     override def paintComponent(gfx: Graphics)
   477     {
   478       super.paintComponent(gfx)
   479       Swing_Thread.assert()
   480 
   481       val buffer = model.buffer
   482       Isabelle.buffer_lock(buffer) {
   483         val snapshot = model.snapshot()
   484 
   485         def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
   486         {
   487           try {
   488             val line1 = buffer.getLineOfOffset(snapshot.convert(start))
   489             val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
   490             Some((line1, line2))
   491           }
   492           catch { case e: ArrayIndexOutOfBoundsException => None }
   493         }
   494         for {
   495           (command, start) <- snapshot.node.command_starts
   496           if !command.is_ignored
   497           (line1, line2) <- line_range(command, start)
   498           val y = line_to_y(line1)
   499           val height = HEIGHT * (line2 - line1)
   500           color <- Isabelle_Markup.overview_color(snapshot, command)
   501         } {
   502           gfx.setColor(color)
   503           gfx.fillRect(0, y, getWidth - 1, height)
   504         }
   505       }
   506     }
   507 
   508     private def line_to_y(line: Int): Int =
   509       (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   510 
   511     private def y_to_line(y: Int): Int =
   512       (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   513   }
   514 
   515 
   516   /* main actor */
   517 
   518   private val main_actor = actor {
   519     loop {
   520       react {
   521         case Session.Commands_Changed(changed) =>
   522           val buffer = model.buffer
   523           Isabelle.swing_buffer_lock(buffer) {
   524             val snapshot = model.snapshot()
   525 
   526             if (changed.exists(snapshot.node.commands.contains))
   527               overview.repaint()
   528 
   529             val visible_range = screen_lines_range()
   530             val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   531             if (visible_cmds.exists(changed)) {
   532               for {
   533                 line <- 0 until text_area.getVisibleLines
   534                 val start = text_area.getScreenLineStartOffset(line) if start >= 0
   535                 val end = text_area.getScreenLineEndOffset(line) if end >= 0
   536                 val range = proper_line_range(start, end)
   537                 val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   538                 if line_cmds.exists(changed)
   539               } text_area.invalidateScreenLineRange(line, line)
   540 
   541               // FIXME danger of deadlock!?
   542               // FIXME potentially slow!?
   543               model.buffer.propertiesChanged()
   544             }
   545           }
   546 
   547         case Session.Global_Settings => html_panel_resize()
   548 
   549         case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   550       }
   551     }
   552   }
   553 
   554 
   555   /* activation */
   556 
   557   private def activate()
   558   {
   559     val painter = text_area.getPainter
   560     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   561     painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
   562     text_area.getGutter.addExtension(gutter_painter)
   563     text_area.addFocusListener(focus_listener)
   564     text_area.getView.addWindowListener(window_listener)
   565     painter.addMouseMotionListener(mouse_motion_listener)
   566     text_area.addCaretListener(caret_listener)
   567     text_area.addLeftOfScrollBar(overview)
   568     session.commands_changed += main_actor
   569     session.global_settings += main_actor
   570   }
   571 
   572   private def deactivate()
   573   {
   574     val painter = text_area.getPainter
   575     session.commands_changed -= main_actor
   576     session.global_settings -= main_actor
   577     text_area.removeFocusListener(focus_listener)
   578     text_area.getView.removeWindowListener(window_listener)
   579     painter.removeMouseMotionListener(mouse_motion_listener)
   580     text_area.removeCaretListener(caret_listener)
   581     text_area.removeLeftOfScrollBar(overview)
   582     text_area.getGutter.removeExtension(gutter_painter)
   583     painter.removeExtension(text_painter)
   584     painter.removeExtension(background_painter)
   585     exit_popup()
   586   }
   587 }