src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Tue Sep 24 16:35:01 2013 +0200 (2013-09-24)
changeset 53844 71f103629327
parent 52980 28f59ca8ce78
child 53845 08721d7b2262
permissions -rw-r--r--
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
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@52977
    18
  /* session */
wenzelm@52977
    19
wenzelm@52980
    20
  override def session: Session = PIDE.session
wenzelm@52971
    21
wenzelm@52980
    22
  override def flush()
wenzelm@52974
    23
  {
wenzelm@52974
    24
    Swing_Thread.require()
wenzelm@52974
    25
wenzelm@52974
    26
    session.update(
wenzelm@52974
    27
      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
wenzelm@52974
    28
        case (edits, buffer) =>
wenzelm@52974
    29
          JEdit_Lib.buffer_lock(buffer) {
wenzelm@52974
    30
            PIDE.document_model(buffer) match {
wenzelm@52974
    31
              case Some(model) => model.flushed_edits() ::: edits
wenzelm@52974
    32
              case None => edits
wenzelm@52974
    33
            }
wenzelm@52974
    34
          }
wenzelm@52974
    35
      }
wenzelm@52974
    36
    )
wenzelm@52974
    37
  }
wenzelm@52974
    38
wenzelm@52977
    39
wenzelm@52977
    40
  /* current situation */
wenzelm@52977
    41
wenzelm@52980
    42
  override def current_context: View =
wenzelm@52971
    43
    Swing_Thread.require { jEdit.getActiveView() }
wenzelm@52971
    44
wenzelm@52980
    45
  override def current_node(view: View): Option[Document.Node.Name] =
wenzelm@52973
    46
    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
wenzelm@52971
    47
wenzelm@52980
    48
  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
wenzelm@52971
    49
    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
wenzelm@52971
    50
wenzelm@52980
    51
  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
wenzelm@52974
    52
  {
wenzelm@52974
    53
    Swing_Thread.require()
wenzelm@52974
    54
wenzelm@52974
    55
    JEdit_Lib.jedit_buffer(name.node) match {
wenzelm@52974
    56
      case Some(buffer) =>
wenzelm@52974
    57
        PIDE.document_model(buffer) match {
wenzelm@52974
    58
          case Some(model) => model.snapshot
wenzelm@52974
    59
          case None => session.snapshot(name)
wenzelm@52974
    60
        }
wenzelm@52974
    61
      case None => session.snapshot(name)
wenzelm@52974
    62
    }
wenzelm@52974
    63
  }
wenzelm@52974
    64
wenzelm@53844
    65
  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
wenzelm@52971
    66
  {
wenzelm@52971
    67
    Swing_Thread.require()
wenzelm@52971
    68
wenzelm@52971
    69
    if (snapshot.is_outdated) None
wenzelm@52971
    70
    else {
wenzelm@52971
    71
      val text_area = view.getTextArea
wenzelm@52971
    72
      PIDE.document_view(text_area) match {
wenzelm@52971
    73
        case Some(doc_view) =>
wenzelm@52973
    74
          val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@52978
    75
          val caret_commands = node.command_range(text_area.getCaretPosition)
wenzelm@53844
    76
          if (caret_commands.hasNext) {
wenzelm@53844
    77
            val (cmd0, _) = caret_commands.next
wenzelm@53844
    78
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
wenzelm@53844
    79
          }
wenzelm@53844
    80
          else None
wenzelm@52971
    81
        case None => None
wenzelm@52971
    82
      }
wenzelm@52971
    83
    }
wenzelm@52971
    84
  }
wenzelm@52977
    85
wenzelm@52977
    86
wenzelm@52977
    87
  /* overlays */
wenzelm@52977
    88
wenzelm@52977
    89
  private var overlays = Document.Overlays.empty
wenzelm@52977
    90
wenzelm@52980
    91
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@52977
    92
    synchronized { overlays(name) }
wenzelm@52977
    93
wenzelm@52980
    94
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@52977
    95
    synchronized { overlays = overlays.insert(command, fn, args) }
wenzelm@52977
    96
wenzelm@52980
    97
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@52977
    98
    synchronized { overlays = overlays.remove(command, fn, args) }
wenzelm@52980
    99
wenzelm@52980
   100
wenzelm@52980
   101
  /* hyperlinks */
wenzelm@52980
   102
wenzelm@52980
   103
  def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
wenzelm@52980
   104
  {
wenzelm@52980
   105
    Swing_Thread.require()
wenzelm@52980
   106
wenzelm@52980
   107
    JEdit_Lib.jedit_buffer(file_name) match {
wenzelm@52980
   108
      case Some(buffer) =>
wenzelm@52980
   109
        view.goToBuffer(buffer)
wenzelm@52980
   110
        val text_area = view.getTextArea
wenzelm@52980
   111
wenzelm@52980
   112
        try {
wenzelm@52980
   113
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
wenzelm@52980
   114
          text_area.moveCaretPosition(line_start)
wenzelm@52980
   115
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
wenzelm@52980
   116
        }
wenzelm@52980
   117
        catch {
wenzelm@52980
   118
          case _: ArrayIndexOutOfBoundsException =>
wenzelm@52980
   119
          case _: IllegalArgumentException =>
wenzelm@52980
   120
        }
wenzelm@52980
   121
wenzelm@52980
   122
      case None =>
wenzelm@52980
   123
        val args =
wenzelm@52980
   124
          if (line <= 0) Array(file_name)
wenzelm@52980
   125
          else if (column <= 0) Array(file_name, "+line:" + line.toInt)
wenzelm@52980
   126
          else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
wenzelm@52980
   127
        jEdit.openFiles(view, null, args)
wenzelm@52980
   128
    }
wenzelm@52980
   129
  }
wenzelm@52980
   130
wenzelm@52980
   131
  override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
wenzelm@52980
   132
    new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
wenzelm@52980
   133
wenzelm@52980
   134
  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
wenzelm@52980
   135
    : Option[Hyperlink] =
wenzelm@52980
   136
  {
wenzelm@52980
   137
    if (snapshot.is_outdated) None
wenzelm@52980
   138
    else {
wenzelm@52980
   139
      snapshot.state.find_command(snapshot.version, command.id) match {
wenzelm@52980
   140
        case None => None
wenzelm@52980
   141
        case Some((node, _)) =>
wenzelm@52980
   142
          val file_name = command.node_name.node
wenzelm@52980
   143
          val sources =
wenzelm@52980
   144
            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm@52980
   145
              (if (offset == 0) Iterator.empty
wenzelm@52980
   146
               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
wenzelm@52980
   147
          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@52980
   148
          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
wenzelm@52980
   149
      }
wenzelm@52980
   150
    }
wenzelm@52980
   151
  }
wenzelm@52971
   152
}