src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Mon Aug 12 12:06:48 2013 +0200 (2013-08-12)
changeset 52974 908e8a36e975
parent 52973 d5f7fa1498b7
child 52977 15254e32d299
permissions -rw-r--r--
tuned signature;
     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   def session: Session = PIDE.session
    19 
    20   def flush()
    21   {
    22     Swing_Thread.require()
    23 
    24     session.update(
    25       (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    26         case (edits, buffer) =>
    27           JEdit_Lib.buffer_lock(buffer) {
    28             PIDE.document_model(buffer) match {
    29               case Some(model) => model.flushed_edits() ::: edits
    30               case None => edits
    31             }
    32           }
    33       }
    34     )
    35   }
    36 
    37   def current_context: View =
    38     Swing_Thread.require { jEdit.getActiveView() }
    39 
    40   def current_node(view: View): Option[Document.Node.Name] =
    41     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    42 
    43   def current_snapshot(view: View): Option[Document.Snapshot] =
    44     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    45 
    46   def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    47   {
    48     Swing_Thread.require()
    49 
    50     JEdit_Lib.jedit_buffer(name.node) match {
    51       case Some(buffer) =>
    52         PIDE.document_model(buffer) match {
    53           case Some(model) => model.snapshot
    54           case None => session.snapshot(name)
    55         }
    56       case None => session.snapshot(name)
    57     }
    58   }
    59 
    60   def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
    61   {
    62     Swing_Thread.require()
    63 
    64     if (snapshot.is_outdated) None
    65     else {
    66       val text_area = view.getTextArea
    67       PIDE.document_view(text_area) match {
    68         case Some(doc_view) =>
    69           val node = snapshot.version.nodes(doc_view.model.node_name)
    70           node.command_at(text_area.getCaretPosition)
    71         case None => None
    72       }
    73     }
    74   }
    75 }