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