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