src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Mon Aug 12 11:56:12 2013 +0200 (2013-08-12)
changeset 52973 d5f7fa1498b7
parent 52971 31926d2c04ee
child 52974 908e8a36e975
permissions -rw-r--r--
tuned signature;
wenzelm@52971
     1
/*  Title:      Tools/jEdit/src/jedit_editor.scala
wenzelm@52971
     2
    Author:     Makarius
wenzelm@52971
     3
wenzelm@52971
     4
PIDE editor operations for jEdit.
wenzelm@52971
     5
*/
wenzelm@52971
     6
wenzelm@52971
     7
package isabelle.jedit
wenzelm@52971
     8
wenzelm@52971
     9
wenzelm@52971
    10
import isabelle._
wenzelm@52971
    11
wenzelm@52971
    12
wenzelm@52971
    13
import org.gjt.sp.jedit.{jEdit, View}
wenzelm@52971
    14
wenzelm@52971
    15
wenzelm@52971
    16
class JEdit_Editor extends Editor[View]
wenzelm@52971
    17
{
wenzelm@52971
    18
  def session: Session = PIDE.session
wenzelm@52971
    19
wenzelm@52971
    20
  def current_context: View =
wenzelm@52971
    21
    Swing_Thread.require { jEdit.getActiveView() }
wenzelm@52971
    22
wenzelm@52971
    23
  def current_node(view: View): Option[Document.Node.Name] =
wenzelm@52973
    24
    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
wenzelm@52971
    25
wenzelm@52971
    26
  def current_snapshot(view: View): Option[Document.Snapshot] =
wenzelm@52971
    27
    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
wenzelm@52971
    28
wenzelm@52971
    29
  def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
wenzelm@52971
    30
  {
wenzelm@52971
    31
    Swing_Thread.require()
wenzelm@52971
    32
wenzelm@52971
    33
    if (snapshot.is_outdated) None
wenzelm@52971
    34
    else {
wenzelm@52971
    35
      val text_area = view.getTextArea
wenzelm@52971
    36
      PIDE.document_view(text_area) match {
wenzelm@52971
    37
        case Some(doc_view) =>
wenzelm@52973
    38
          val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@52971
    39
          node.command_at(text_area.getCaretPosition)
wenzelm@52971
    40
        case None => None
wenzelm@52971
    41
      }
wenzelm@52971
    42
    }
wenzelm@52971
    43
  }
wenzelm@52971
    44
}