src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Mon Aug 12 14:27:58 2013 +0200 (2013-08-12)
changeset 52977 15254e32d299
parent 52974 908e8a36e975
child 52978 37fbb3fde380
permissions -rw-r--r--
central management of Document.Overlays, independent of Document_Model;
     1 /*  Title:      Tools/jEdit/src/jedit_editor.scala
     2     Author:     Makarius
     3 
     4 PIDE editor operations for jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 import org.gjt.sp.jedit.{jEdit, View}
    14 
    15 
    16 class JEdit_Editor extends Editor[View]
    17 {
    18   /* session */
    19 
    20   def session: Session = PIDE.session
    21 
    22   def flush()
    23   {
    24     Swing_Thread.require()
    25 
    26     session.update(
    27       (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    28         case (edits, buffer) =>
    29           JEdit_Lib.buffer_lock(buffer) {
    30             PIDE.document_model(buffer) match {
    31               case Some(model) => model.flushed_edits() ::: edits
    32               case None => edits
    33             }
    34           }
    35       }
    36     )
    37   }
    38 
    39 
    40   /* current situation */
    41 
    42   def current_context: View =
    43     Swing_Thread.require { jEdit.getActiveView() }
    44 
    45   def current_node(view: View): Option[Document.Node.Name] =
    46     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    47 
    48   def current_snapshot(view: View): Option[Document.Snapshot] =
    49     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    50 
    51   def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    52   {
    53     Swing_Thread.require()
    54 
    55     JEdit_Lib.jedit_buffer(name.node) match {
    56       case Some(buffer) =>
    57         PIDE.document_model(buffer) match {
    58           case Some(model) => model.snapshot
    59           case None => session.snapshot(name)
    60         }
    61       case None => session.snapshot(name)
    62     }
    63   }
    64 
    65   def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
    66   {
    67     Swing_Thread.require()
    68 
    69     if (snapshot.is_outdated) None
    70     else {
    71       val text_area = view.getTextArea
    72       PIDE.document_view(text_area) match {
    73         case Some(doc_view) =>
    74           val node = snapshot.version.nodes(doc_view.model.node_name)
    75           node.command_at(text_area.getCaretPosition)
    76         case None => None
    77       }
    78     }
    79   }
    80 
    81 
    82   /* overlays */
    83 
    84   private var overlays = Document.Overlays.empty
    85 
    86   def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    87     synchronized { overlays(name) }
    88 
    89   def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    90     synchronized { overlays = overlays.insert(command, fn, args) }
    91 
    92   def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    93     synchronized { overlays = overlays.remove(command, fn, args) }
    94 }