src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Tue Apr 22 23:49:15 2014 +0200 (2014-04-22)
changeset 56662 f373fb77e0a4
parent 56494 1b74abf064e1
child 56729 1da2272a06a4
permissions -rw-r--r--
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
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@56662
    27
    Swing_Thread.require {}
wenzelm@52974
    28
wenzelm@55783
    29
    val doc_blobs = PIDE.document_blobs()
wenzelm@55783
    30
    val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
wenzelm@55783
    31
    if (!edits.isEmpty) session.update(doc_blobs, edits)
wenzelm@52974
    32
  }
wenzelm@52974
    33
wenzelm@54461
    34
  private val delay_flush =
wenzelm@54461
    35
    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
wenzelm@54461
    36
wenzelm@54461
    37
  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
wenzelm@54461
    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@56662
    53
    Swing_Thread.require {}
wenzelm@52974
    54
wenzelm@56457
    55
    JEdit_Lib.jedit_buffer(name) 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@56662
    67
    Swing_Thread.require {}
wenzelm@52971
    68
wenzelm@54325
    69
    val text_area = view.getTextArea
wenzelm@54528
    70
    val buffer = view.getBuffer
wenzelm@54528
    71
wenzelm@54325
    72
    PIDE.document_view(text_area) match {
wenzelm@55432
    73
      case Some(doc_view) if doc_view.model.is_theory =>
wenzelm@54325
    74
        val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@54325
    75
        val caret = snapshot.revert(text_area.getCaretPosition)
wenzelm@54528
    76
        if (caret < buffer.getLength) {
wenzelm@56373
    77
          val caret_command_iterator = node.command_iterator(caret)
wenzelm@56373
    78
          if (caret_command_iterator.hasNext) {
wenzelm@56373
    79
            val (cmd0, _) = caret_command_iterator.next
wenzelm@54325
    80
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
wenzelm@53844
    81
          }
wenzelm@54325
    82
          else None
wenzelm@54325
    83
        }
wenzelm@54325
    84
        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
wenzelm@55432
    85
      case _ =>
wenzelm@54528
    86
        PIDE.document_model(buffer) match {
wenzelm@54531
    87
          case Some(model) if !model.is_theory =>
wenzelm@56314
    88
            snapshot.version.nodes.load_commands(model.node_name) match {
wenzelm@54528
    89
              case cmd :: _ => Some(cmd)
wenzelm@54528
    90
              case Nil => None
wenzelm@54528
    91
            }
wenzelm@54528
    92
          case _ => None
wenzelm@54528
    93
        }
wenzelm@52971
    94
    }
wenzelm@52971
    95
  }
wenzelm@52977
    96
wenzelm@52977
    97
wenzelm@52977
    98
  /* overlays */
wenzelm@52977
    99
wenzelm@52977
   100
  private var overlays = Document.Overlays.empty
wenzelm@52977
   101
wenzelm@52980
   102
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@52977
   103
    synchronized { overlays(name) }
wenzelm@52977
   104
wenzelm@52980
   105
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@52977
   106
    synchronized { overlays = overlays.insert(command, fn, args) }
wenzelm@52977
   107
wenzelm@52980
   108
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@52977
   109
    synchronized { overlays = overlays.remove(command, fn, args) }
wenzelm@52980
   110
wenzelm@52980
   111
wenzelm@55877
   112
  /* navigation */
wenzelm@52980
   113
wenzelm@56413
   114
  def push_position(view: View)
wenzelm@56413
   115
  {
wenzelm@56413
   116
    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
wenzelm@56413
   117
    if (navigator != null) {
wenzelm@56413
   118
      try {
wenzelm@56413
   119
        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
wenzelm@56413
   120
        m.invoke(null, view)
wenzelm@56413
   121
      }
wenzelm@56413
   122
      catch { case _: NoSuchMethodException => }
wenzelm@56413
   123
    }
wenzelm@56413
   124
  }
wenzelm@56413
   125
wenzelm@55877
   126
  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
wenzelm@52980
   127
  {
wenzelm@56662
   128
    Swing_Thread.require {}
wenzelm@52980
   129
wenzelm@56413
   130
    push_position(view)
wenzelm@56413
   131
wenzelm@54706
   132
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52980
   133
      case Some(buffer) =>
wenzelm@52980
   134
        view.goToBuffer(buffer)
wenzelm@52980
   135
        val text_area = view.getTextArea
wenzelm@52980
   136
wenzelm@52980
   137
        try {
wenzelm@52980
   138
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
wenzelm@52980
   139
          text_area.moveCaretPosition(line_start)
wenzelm@52980
   140
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
wenzelm@52980
   141
        }
wenzelm@52980
   142
        catch {
wenzelm@52980
   143
          case _: ArrayIndexOutOfBoundsException =>
wenzelm@52980
   144
          case _: IllegalArgumentException =>
wenzelm@52980
   145
        }
wenzelm@52980
   146
wenzelm@54706
   147
      case None if (new JFile(name)).isDirectory =>
wenzelm@54706
   148
        VFSBrowser.browseDirectory(view, name)
wenzelm@54706
   149
wenzelm@52980
   150
      case None =>
wenzelm@52980
   151
        val args =
wenzelm@54706
   152
          if (line <= 0) Array(name)
wenzelm@54706
   153
          else if (column <= 0) Array(name, "+line:" + line.toInt)
wenzelm@54706
   154
          else Array(name, "+line:" + line.toInt + "," + column.toInt)
wenzelm@52980
   155
        jEdit.openFiles(view, null, args)
wenzelm@52980
   156
    }
wenzelm@52980
   157
  }
wenzelm@52980
   158
wenzelm@55877
   159
wenzelm@55877
   160
  /* hyperlinks */
wenzelm@55877
   161
wenzelm@56461
   162
  def hyperlink_url(name: String): Hyperlink =
wenzelm@56461
   163
    new Hyperlink {
wenzelm@56494
   164
      val external = true
wenzelm@56461
   165
      def follow(view: View) =
wenzelm@56461
   166
        default_thread_pool.submit(() =>
wenzelm@56461
   167
          try { Isabelle_System.open(name) }
wenzelm@56461
   168
          catch {
wenzelm@56461
   169
            case exn: Throwable =>
wenzelm@56461
   170
              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@56461
   171
          })
wenzelm@56461
   172
      override def toString: String = "URL " + quote(name)
wenzelm@52980
   173
    }
wenzelm@55876
   174
wenzelm@55876
   175
  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
wenzelm@56461
   176
    new Hyperlink {
wenzelm@56494
   177
      val external = false
wenzelm@56461
   178
      def follow(view: View) = goto_file(view, name, line, column)
wenzelm@56461
   179
      override def toString: String = "file " + quote(name)
wenzelm@56461
   180
    }
wenzelm@55876
   181
wenzelm@55884
   182
  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
wenzelm@55878
   183
    : Option[Hyperlink] =
wenzelm@55878
   184
  {
wenzelm@56458
   185
    val opt_name =
wenzelm@56458
   186
      if (Path.is_wellformed(source_name)) {
wenzelm@56458
   187
        if (Path.is_valid(source_name)) {
wenzelm@56458
   188
          val path = Path.explode(source_name)
wenzelm@56458
   189
          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
wenzelm@56458
   190
        }
wenzelm@56458
   191
        else None
wenzelm@55878
   192
      }
wenzelm@56458
   193
      else Some(source_name)
wenzelm@56458
   194
wenzelm@56458
   195
    opt_name match {
wenzelm@56458
   196
      case Some(name) =>
wenzelm@56458
   197
        JEdit_Lib.jedit_buffer(name) match {
wenzelm@56458
   198
          case Some(buffer) if offset > 0 =>
wenzelm@56458
   199
            val (line, column) =
wenzelm@56458
   200
              JEdit_Lib.buffer_lock(buffer) {
wenzelm@56458
   201
                ((1, 1) /:
wenzelm@56458
   202
                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
wenzelm@56458
   203
                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
wenzelm@56458
   204
                      Symbol.advance_line_column)
wenzelm@56458
   205
              }
wenzelm@56458
   206
            Some(hyperlink_file(name, line, column))
wenzelm@56458
   207
          case _ => Some(hyperlink_file(name, line))
wenzelm@56458
   208
        }
wenzelm@56458
   209
      case None => None
wenzelm@55878
   210
    }
wenzelm@55878
   211
  }
wenzelm@55876
   212
wenzelm@56461
   213
  override def hyperlink_command(
wenzelm@56461
   214
    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
wenzelm@56461
   215
  {
wenzelm@56461
   216
    if (snapshot.is_outdated) None
wenzelm@56461
   217
    else {
wenzelm@56461
   218
      snapshot.state.find_command(snapshot.version, command.id) match {
wenzelm@56461
   219
        case None => None
wenzelm@56461
   220
        case Some((node, _)) =>
wenzelm@56461
   221
          val file_name = command.node_name.node
wenzelm@56461
   222
          val sources_iterator =
wenzelm@56461
   223
            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm@56461
   224
              (if (offset == 0) Iterator.empty
wenzelm@56462
   225
               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
wenzelm@56461
   226
          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
wenzelm@56461
   227
          Some(hyperlink_file(file_name, line, column))
wenzelm@56461
   228
      }
wenzelm@55876
   229
    }
wenzelm@56461
   230
  }
wenzelm@56461
   231
wenzelm@56461
   232
  def hyperlink_command_id(
wenzelm@56461
   233
    snapshot: Document.Snapshot,
wenzelm@56461
   234
    id: Document_ID.Generic,
wenzelm@56461
   235
    offset: Symbol.Offset): Option[Hyperlink] =
wenzelm@56461
   236
  {
wenzelm@56461
   237
    snapshot.state.find_command(snapshot.version, id) match {
wenzelm@56461
   238
      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
wenzelm@56461
   239
      case None => None
wenzelm@56461
   240
    }
wenzelm@56461
   241
  }
wenzelm@52971
   242
}