wenzelm@43282: /*  Title:      Tools/jEdit/src/document_view.scala
wenzelm@36760:     Author:     Fabian Immler, TU Munich
wenzelm@36760:     Author:     Makarius
wenzelm@36760: 
wenzelm@36760: Document view connected to jEdit text area.
wenzelm@36760: */
wenzelm@34408: 
immler@34403: package isabelle.jedit
immler@34403: 
wenzelm@34760: 
wenzelm@36015: import isabelle._
wenzelm@36015: 
wenzelm@54441: import java.awt.Graphics2D
wenzelm@53226: import java.awt.event.KeyEvent
wenzelm@34784: import javax.swing.event.{CaretListener, CaretEvent}
wenzelm@34734: 
wenzelm@54441: import org.gjt.sp.jedit.jEdit
wenzelm@39176: import org.gjt.sp.jedit.options.GutterOptionPane
wenzelm@55712: import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
wenzelm@34784: 
wenzelm@34784: 
wenzelm@34784: object Document_View
wenzelm@34784: {
wenzelm@34784:   /* document view of text area */
wenzelm@34784: 
wenzelm@34784:   private val key = new Object
wenzelm@34784: 
wenzelm@55712:   def apply(text_area: TextArea): Option[Document_View] =
wenzelm@34784:   {
wenzelm@57612:     GUI_Thread.require {}
wenzelm@34784:     text_area.getClientProperty(key) match {
wenzelm@34784:       case doc_view: Document_View => Some(doc_view)
wenzelm@34784:       case _ => None
wenzelm@34784:     }
wenzelm@34784:   }
wenzelm@34784: 
wenzelm@39741:   def exit(text_area: JEditTextArea)
wenzelm@34784:   {
wenzelm@57612:     GUI_Thread.require {}
wenzelm@34788:     apply(text_area) match {
wenzelm@39636:       case None =>
wenzelm@34784:       case Some(doc_view) =>
wenzelm@34784:         doc_view.deactivate()
wenzelm@34784:         text_area.putClientProperty(key, null)
wenzelm@34784:     }
wenzelm@34784:   }
wenzelm@43397: 
wenzelm@43397:   def init(model: Document_Model, text_area: JEditTextArea): Document_View =
wenzelm@43397:   {
wenzelm@43397:     exit(text_area)
wenzelm@43397:     val doc_view = new Document_View(model, text_area)
wenzelm@43397:     text_area.putClientProperty(key, doc_view)
wenzelm@43397:     doc_view.activate()
wenzelm@43397:     doc_view
wenzelm@43397:   }
wenzelm@34784: }
immler@34403: 
wenzelm@34733: 
wenzelm@43376: class Document_View(val model: Document_Model, val text_area: JEditTextArea)
immler@34654: {
wenzelm@34784:   private val session = model.session
wenzelm@34784: 
wenzelm@50205:   def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
wenzelm@49411: 
wenzelm@50306:   val rich_text_area =
wenzelm@63028:     new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (), () => None,
wenzelm@63028:       () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
wenzelm@49411: 
immler@34403: 
wenzelm@44379:   /* perspective */
wenzelm@44379: 
wenzelm@54325:   def perspective(snapshot: Document.Snapshot): Text.Perspective =
wenzelm@44379:   {
wenzelm@57612:     GUI_Thread.require {}
wenzelm@53780: 
wenzelm@54325:     val active_command =
wenzelm@54325:     {
wenzelm@54325:       val view = text_area.getView
wenzelm@54325:       if (view != null && view.getTextArea == text_area) {
wenzelm@54325:         PIDE.editor.current_command(view, snapshot) match {
wenzelm@54325:           case Some(command) =>
wenzelm@54325:             snapshot.node.command_start(command) match {
wenzelm@54530:               case Some(start) => List(snapshot.convert(command.proper_range + start))
wenzelm@54325:               case None => Nil
wenzelm@54325:             }
wenzelm@54325:           case None => Nil
wenzelm@54325:         }
wenzelm@54325:       }
wenzelm@53780:       else Nil
wenzelm@54325:     }
wenzelm@53780: 
wenzelm@50363:     val buffer_range = JEdit_Lib.buffer_range(model.buffer)
wenzelm@53780:     val visible_lines =
wenzelm@53780:       (for {
wenzelm@56356:         i <- (0 until text_area.getVisibleLines).iterator
wenzelm@46997:         start = text_area.getScreenLineStartOffset(i)
wenzelm@46997:         stop = text_area.getScreenLineEndOffset(i)
wenzelm@44379:         if start >= 0 && stop >= 0
wenzelm@46997:         range <- buffer_range.try_restrict(Text.Range(start, stop))
wenzelm@44583:         if !range.is_singularity
wenzelm@44379:       }
wenzelm@53780:       yield range).toList
wenzelm@53780: 
wenzelm@54325:     Text.Perspective(active_command ::: visible_lines)
wenzelm@44379:   }
wenzelm@44379: 
wenzelm@54461:   private def update_view = new TextAreaExtension
wenzelm@44437:   {
wenzelm@44437:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@44437:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@44437:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@44437:     {
wenzelm@49424:       // no robust_body
wenzelm@54461:       PIDE.editor.invoke()
wenzelm@44437:     }
wenzelm@44437:   }
wenzelm@44437: 
wenzelm@44379: 
wenzelm@49411:   /* gutter */
immler@34513: 
wenzelm@42825:   private val gutter_painter = new TextAreaExtension
wenzelm@39175:   {
wenzelm@39175:     override def paintScreenLineRange(gfx: Graphics2D,
wenzelm@39175:       first_line: Int, last_line: Int, physical_lines: Array[Int],
wenzelm@39175:       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
wenzelm@39175:     {
wenzelm@49411:       rich_text_area.robust_body(()) {
wenzelm@57612:         GUI_Thread.assert {}
wenzelm@46920: 
wenzelm@43404:         val gutter = text_area.getGutter
wenzelm@59129:         val sel_width = GutterOptionPane.getSelectionAreaWidth
wenzelm@43404:         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
wenzelm@43404:         val FOLD_MARKER_SIZE = 12
wenzelm@43419: 
wenzelm@59129:         val buffer = model.buffer
wenzelm@59129:         JEdit_Lib.buffer_lock(buffer) {
wenzelm@59129:           val rendering = get_rendering()
wenzelm@49356: 
wenzelm@59129:           for (i <- 0 until physical_lines.length) {
wenzelm@59129:             if (physical_lines(i) != -1) {
wenzelm@59129:               val line_range = Text.Range(start(i), end(i))
wenzelm@43419: 
wenzelm@59129:               rendering.gutter_content(line_range) match {
wenzelm@59129:                 case Some((icon, color)) =>
wenzelm@59129:                   // icons within selection area
wenzelm@59129:                   if (!gutter.isExpanded &&
wenzelm@59129:                       gutter.isSelectionAreaEnabled && sel_width >= 12 && line_height >= 12)
wenzelm@59129:                   {
wenzelm@59129:                     val x0 =
wenzelm@59129:                       (FOLD_MARKER_SIZE + sel_width - border_width - icon.getIconWidth) max 10
wenzelm@59129:                     val y0 =
wenzelm@59129:                       y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
wenzelm@46227:                     icon.paintIcon(gutter, gfx, x0, y0)
wenzelm@59129:                   }
wenzelm@59129:                   // background
wenzelm@59129:                   else {
wenzelm@59129:                     val y0 = y + i * line_height
wenzelm@59129:                     gfx.setColor(color)
wenzelm@59129:                     gfx.fillRect(0, y0, gutter.getWidth, line_height)
wenzelm@59129:                   }
wenzelm@59129:                 case None =>
wenzelm@39175:               }
wenzelm@39175:             }
wenzelm@39175:           }
wenzelm@39175:         }
wenzelm@39175:       }
wenzelm@39175:     }
wenzelm@39175:   }
wenzelm@39175: 
wenzelm@39175: 
wenzelm@52479:   /* key listener */
wenzelm@52479: 
wenzelm@53226:   private val key_listener =
wenzelm@53226:     JEdit_Lib.key_listener(
wenzelm@53227:       key_pressed = (evt: KeyEvent) =>
wenzelm@53226:         {
wenzelm@53244:           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
wenzelm@53226:             evt.consume
wenzelm@53274:         }
wenzelm@53226:     )
wenzelm@52479: 
wenzelm@52479: 
wenzelm@37129:   /* caret handling */
wenzelm@34810: 
wenzelm@46740:   private val delay_caret_update =
wenzelm@57612:     GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
wenzelm@56715:       session.caret_focus.post(Session.Caret_Focus)
wenzelm@62986:       JEdit_Lib.invalidate(text_area)
wenzelm@34810:     }
wenzelm@46740: 
wenzelm@46740:   private val caret_listener = new CaretListener {
wenzelm@49195:     override def caretUpdate(e: CaretEvent) { delay_caret_update.invoke() }
wenzelm@34810:   }
wenzelm@34810: 
wenzelm@34810: 
wenzelm@46572:   /* text status overview left of scrollbar */
wenzelm@34784: 
wenzelm@62985:   private val text_overview = new Text_Overview(this)
immler@34403: 
wenzelm@34784: 
wenzelm@56715:   /* main */
wenzelm@39740: 
wenzelm@56715:   private val main =
wenzelm@56715:     Session.Consumer[Any](getClass.getName) {
wenzelm@61723:       case _: Session.Raw_Edits =>
wenzelm@62985:         text_overview.invoke()
wenzelm@49196: 
wenzelm@56715:       case changed: Session.Commands_Changed =>
wenzelm@56715:         val buffer = model.buffer
wenzelm@57612:         GUI_Thread.later {
wenzelm@56715:           JEdit_Lib.buffer_lock(buffer) {
wenzelm@56715:             if (model.buffer == text_area.getBuffer) {
wenzelm@56715:               val snapshot = model.snapshot()
wenzelm@39740: 
wenzelm@56715:               val load_changed =
wenzelm@56715:                 snapshot.load_commands.exists(changed.commands.contains)
wenzelm@55432: 
wenzelm@56715:               if (changed.assignment || load_changed ||
wenzelm@56715:                   (changed.nodes.contains(model.node_name) &&
wenzelm@56715:                    changed.commands.exists(snapshot.node.commands.contains)))
wenzelm@62985:                 text_overview.invoke()
wenzelm@39740: 
wenzelm@62986:               JEdit_Lib.invalidate(text_area)
wenzelm@39740:             }
wenzelm@39740:           }
wenzelm@56715:         }
wenzelm@39740:     }
wenzelm@39740: 
wenzelm@39740: 
wenzelm@34784:   /* activation */
wenzelm@34784: 
wenzelm@34808:   private def activate()
wenzelm@34784:   {
wenzelm@42825:     val painter = text_area.getPainter
wenzelm@49410: 
wenzelm@54461:     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view)
wenzelm@49411:     rich_text_area.activate()
wenzelm@42825:     text_area.getGutter.addExtension(gutter_painter)
wenzelm@52479:     text_area.addKeyListener(key_listener)
wenzelm@34810:     text_area.addCaretListener(caret_listener)
wenzelm@62985:     text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint()
wenzelm@58748:     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
wenzelm@58748:       foreach(text_area.addStructureMatcher(_))
wenzelm@56715:     session.raw_edits += main
wenzelm@56715:     session.commands_changed += main
wenzelm@34784:   }
wenzelm@34784: 
wenzelm@34808:   private def deactivate()
wenzelm@34784:   {
wenzelm@42825:     val painter = text_area.getPainter
wenzelm@49410: 
wenzelm@56715:     session.raw_edits -= main
wenzelm@56715:     session.commands_changed -= main
wenzelm@58748:     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
wenzelm@58748:       foreach(text_area.removeStructureMatcher(_))
wenzelm@62985:     text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
wenzelm@49195:     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
wenzelm@52479:     text_area.removeKeyListener(key_listener)
wenzelm@42825:     text_area.getGutter.removeExtension(gutter_painter)
wenzelm@49411:     rich_text_area.deactivate()
wenzelm@54461:     painter.removeExtension(update_view)
wenzelm@34784:   }
wenzelm@42825: }