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;
     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 current_context: View =
    21     Swing_Thread.require { jEdit.getActiveView() }
    22 
    23   def current_node(view: View): Option[Document.Node.Name] =
    24     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    25 
    26   def current_snapshot(view: View): Option[Document.Snapshot] =
    27     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    28 
    29   def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
    30   {
    31     Swing_Thread.require()
    32 
    33     if (snapshot.is_outdated) None
    34     else {
    35       val text_area = view.getTextArea
    36       PIDE.document_view(text_area) match {
    37         case Some(doc_view) =>
    38           val node = snapshot.version.nodes(doc_view.model.node_name)
    39           node.command_at(text_area.getCaretPosition)
    40         case None => None
    41       }
    42     }
    43   }
    44 }