src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Tue Feb 11 21:58:31 2014 +0100 (2014-02-11)
changeset 55432 9c53198dbb1c
parent 54706 d3c656f0b7ab
child 55781 b3a4207fb9a6
permissions -rw-r--r--
maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;
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@54706
    13
import java.io.{File => JFile}
wenzelm@54706
    14
wenzelm@52971
    15
import org.gjt.sp.jedit.{jEdit, View}
wenzelm@54706
    16
import org.gjt.sp.jedit.browser.VFSBrowser
wenzelm@52971
    17
wenzelm@52971
    18
wenzelm@52971
    19
class JEdit_Editor extends Editor[View]
wenzelm@52971
    20
{
wenzelm@52977
    21
  /* session */
wenzelm@52977
    22
wenzelm@52980
    23
  override def session: Session = PIDE.session
wenzelm@52971
    24
wenzelm@52980
    25
  override def flush()
wenzelm@52974
    26
  {
wenzelm@52974
    27
    Swing_Thread.require()
wenzelm@52974
    28
wenzelm@54522
    29
    val edits = PIDE.document_models().flatMap(_.flushed_edits())
wenzelm@54522
    30
    if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
wenzelm@52974
    31
  }
wenzelm@52974
    32
wenzelm@54461
    33
  private val delay_flush =
wenzelm@54461
    34
    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
wenzelm@54461
    35
wenzelm@54461
    36
  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
wenzelm@54461
    37
wenzelm@52977
    38
wenzelm@52977
    39
  /* current situation */
wenzelm@52977
    40
wenzelm@52980
    41
  override def current_context: View =
wenzelm@52971
    42
    Swing_Thread.require { jEdit.getActiveView() }
wenzelm@52971
    43
wenzelm@52980
    44
  override def current_node(view: View): Option[Document.Node.Name] =
wenzelm@52973
    45
    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
wenzelm@52971
    46
wenzelm@52980
    47
  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
wenzelm@52971
    48
    Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
wenzelm@52971
    49
wenzelm@52980
    50
  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
wenzelm@52974
    51
  {
wenzelm@52974
    52
    Swing_Thread.require()
wenzelm@52974
    53
wenzelm@52974
    54
    JEdit_Lib.jedit_buffer(name.node) match {
wenzelm@52974
    55
      case Some(buffer) =>
wenzelm@52974
    56
        PIDE.document_model(buffer) match {
wenzelm@52974
    57
          case Some(model) => model.snapshot
wenzelm@52974
    58
          case None => session.snapshot(name)
wenzelm@52974
    59
        }
wenzelm@52974
    60
      case None => session.snapshot(name)
wenzelm@52974
    61
    }
wenzelm@52974
    62
  }
wenzelm@52974
    63
wenzelm@53844
    64
  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
wenzelm@52971
    65
  {
wenzelm@52971
    66
    Swing_Thread.require()
wenzelm@52971
    67
wenzelm@54325
    68
    val text_area = view.getTextArea
wenzelm@54528
    69
    val buffer = view.getBuffer
wenzelm@54528
    70
wenzelm@54325
    71
    PIDE.document_view(text_area) match {
wenzelm@55432
    72
      case Some(doc_view) if doc_view.model.is_theory =>
wenzelm@54325
    73
        val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@54325
    74
        val caret = snapshot.revert(text_area.getCaretPosition)
wenzelm@54528
    75
        if (caret < buffer.getLength) {
wenzelm@54325
    76
          val caret_commands = node.command_range(caret)
wenzelm@54325
    77
          if (caret_commands.hasNext) {
wenzelm@54325
    78
            val (cmd0, _) = caret_commands.next
wenzelm@54325
    79
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
wenzelm@53844
    80
          }
wenzelm@54325
    81
          else None
wenzelm@54325
    82
        }
wenzelm@54325
    83
        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
wenzelm@55432
    84
      case _ =>
wenzelm@54528
    85
        PIDE.document_model(buffer) match {
wenzelm@54531
    86
          case Some(model) if !model.is_theory =>
wenzelm@54528
    87
            snapshot.version.nodes.thy_load_commands(model.node_name) match {
wenzelm@54528
    88
              case cmd :: _ => Some(cmd)
wenzelm@54528
    89
              case Nil => None
wenzelm@54528
    90
            }
wenzelm@54528
    91
          case _ => None
wenzelm@54528
    92
        }
wenzelm@52971
    93
    }
wenzelm@52971
    94
  }
wenzelm@52977
    95
wenzelm@52977
    96
wenzelm@52977
    97
  /* overlays */
wenzelm@52977
    98
wenzelm@52977
    99
  private var overlays = Document.Overlays.empty
wenzelm@52977
   100
wenzelm@52980
   101
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@52977
   102
    synchronized { overlays(name) }
wenzelm@52977
   103
wenzelm@52980
   104
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@52977
   105
    synchronized { overlays = overlays.insert(command, fn, args) }
wenzelm@52977
   106
wenzelm@52980
   107
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@52977
   108
    synchronized { overlays = overlays.remove(command, fn, args) }
wenzelm@52980
   109
wenzelm@52980
   110
wenzelm@52980
   111
  /* hyperlinks */
wenzelm@52980
   112
wenzelm@54706
   113
  def goto(view: View, name: String, line: Int = 0, column: Int = 0)
wenzelm@52980
   114
  {
wenzelm@52980
   115
    Swing_Thread.require()
wenzelm@52980
   116
wenzelm@54706
   117
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52980
   118
      case Some(buffer) =>
wenzelm@52980
   119
        view.goToBuffer(buffer)
wenzelm@52980
   120
        val text_area = view.getTextArea
wenzelm@52980
   121
wenzelm@52980
   122
        try {
wenzelm@52980
   123
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
wenzelm@52980
   124
          text_area.moveCaretPosition(line_start)
wenzelm@52980
   125
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
wenzelm@52980
   126
        }
wenzelm@52980
   127
        catch {
wenzelm@52980
   128
          case _: ArrayIndexOutOfBoundsException =>
wenzelm@52980
   129
          case _: IllegalArgumentException =>
wenzelm@52980
   130
        }
wenzelm@52980
   131
wenzelm@54706
   132
      case None if (new JFile(name)).isDirectory =>
wenzelm@54706
   133
        VFSBrowser.browseDirectory(view, name)
wenzelm@54706
   134
wenzelm@52980
   135
      case None =>
wenzelm@52980
   136
        val args =
wenzelm@54706
   137
          if (line <= 0) Array(name)
wenzelm@54706
   138
          else if (column <= 0) Array(name, "+line:" + line.toInt)
wenzelm@54706
   139
          else Array(name, "+line:" + line.toInt + "," + column.toInt)
wenzelm@52980
   140
        jEdit.openFiles(view, null, args)
wenzelm@52980
   141
    }
wenzelm@52980
   142
  }
wenzelm@52980
   143
wenzelm@54702
   144
  override def hyperlink_url(name: String): Hyperlink =
wenzelm@54702
   145
    new Hyperlink {
wenzelm@54702
   146
      def follow(view: View) =
wenzelm@54702
   147
        default_thread_pool.submit(() =>
wenzelm@54702
   148
          try { Isabelle_System.open(name) }
wenzelm@54702
   149
          catch {
wenzelm@54702
   150
            case exn: Throwable =>
wenzelm@54702
   151
              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@54702
   152
          })
wenzelm@54702
   153
    }
wenzelm@54702
   154
wenzelm@54706
   155
  override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
wenzelm@54706
   156
    new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
wenzelm@52980
   157
wenzelm@52980
   158
  override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
wenzelm@52980
   159
    : Option[Hyperlink] =
wenzelm@52980
   160
  {
wenzelm@52980
   161
    if (snapshot.is_outdated) None
wenzelm@52980
   162
    else {
wenzelm@52980
   163
      snapshot.state.find_command(snapshot.version, command.id) match {
wenzelm@52980
   164
        case None => None
wenzelm@52980
   165
        case Some((node, _)) =>
wenzelm@52980
   166
          val file_name = command.node_name.node
wenzelm@52980
   167
          val sources =
wenzelm@52980
   168
            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm@52980
   169
              (if (offset == 0) Iterator.empty
wenzelm@52980
   170
               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
wenzelm@52980
   171
          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
wenzelm@52980
   172
          Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
wenzelm@52980
   173
      }
wenzelm@52980
   174
    }
wenzelm@52980
   175
  }
wenzelm@52971
   176
}