src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Sun Oct 05 17:58:36 2014 +0200 (2014-10-05 ago)
changeset 58545 30b75b7958d6
parent 57878 51a2f9140175
child 59080 611914621edb
permissions -rw-r--r--
citation tooltip/hyperlink based on open buffers with .bib 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@58545
    15
import org.gjt.sp.jedit.{jEdit, View, Buffer}
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@57612
    25
  // owned by GUI thread
wenzelm@57611
    26
  private var removed_nodes = Set.empty[Document.Node.Name]
wenzelm@57611
    27
wenzelm@57611
    28
  def remove_node(name: Document.Node.Name): Unit =
wenzelm@57612
    29
    GUI_Thread.require { removed_nodes += name }
wenzelm@57611
    30
wenzelm@52980
    31
  override def flush()
wenzelm@52974
    32
  {
wenzelm@57612
    33
    GUI_Thread.require {}
wenzelm@52974
    34
wenzelm@55783
    35
    val doc_blobs = PIDE.document_blobs()
wenzelm@57611
    36
    val models = PIDE.document_models()
wenzelm@57611
    37
wenzelm@57611
    38
    val removed = removed_nodes; removed_nodes = Set.empty
wenzelm@57611
    39
    val removed_perspective =
wenzelm@57611
    40
      (removed -- models.iterator.map(_.node_name)).toList.map(
wenzelm@57615
    41
        name => (name, Document.Node.no_perspective_text))
wenzelm@57611
    42
wenzelm@57611
    43
    val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
wenzelm@55783
    44
    if (!edits.isEmpty) session.update(doc_blobs, edits)
wenzelm@52974
    45
  }
wenzelm@52974
    46
wenzelm@54461
    47
  private val delay_flush =
wenzelm@57612
    48
    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
wenzelm@54461
    49
wenzelm@56770
    50
  def invoke(): Unit = delay_flush.invoke()
wenzelm@54461
    51
wenzelm@52977
    52
wenzelm@52977
    53
  /* current situation */
wenzelm@52977
    54
wenzelm@52980
    55
  override def current_context: View =
wenzelm@57612
    56
    GUI_Thread.require { jEdit.getActiveView() }
wenzelm@52971
    57
wenzelm@52980
    58
  override def current_node(view: View): Option[Document.Node.Name] =
wenzelm@57612
    59
    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
wenzelm@52971
    60
wenzelm@52980
    61
  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
wenzelm@57612
    62
    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
wenzelm@52971
    63
wenzelm@52980
    64
  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
wenzelm@52974
    65
  {
wenzelm@57612
    66
    GUI_Thread.require {}
wenzelm@52974
    67
wenzelm@56457
    68
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52974
    69
      case Some(buffer) =>
wenzelm@52974
    70
        PIDE.document_model(buffer) match {
wenzelm@52974
    71
          case Some(model) => model.snapshot
wenzelm@52974
    72
          case None => session.snapshot(name)
wenzelm@52974
    73
        }
wenzelm@52974
    74
      case None => session.snapshot(name)
wenzelm@52974
    75
    }
wenzelm@52974
    76
  }
wenzelm@52974
    77
wenzelm@53844
    78
  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
wenzelm@52971
    79
  {
wenzelm@57612
    80
    GUI_Thread.require {}
wenzelm@52971
    81
wenzelm@54325
    82
    val text_area = view.getTextArea
wenzelm@54528
    83
    val buffer = view.getBuffer
wenzelm@54528
    84
wenzelm@54325
    85
    PIDE.document_view(text_area) match {
wenzelm@55432
    86
      case Some(doc_view) if doc_view.model.is_theory =>
wenzelm@54325
    87
        val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@54325
    88
        val caret = snapshot.revert(text_area.getCaretPosition)
wenzelm@54528
    89
        if (caret < buffer.getLength) {
wenzelm@56373
    90
          val caret_command_iterator = node.command_iterator(caret)
wenzelm@56373
    91
          if (caret_command_iterator.hasNext) {
wenzelm@56373
    92
            val (cmd0, _) = caret_command_iterator.next
wenzelm@54325
    93
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
wenzelm@53844
    94
          }
wenzelm@54325
    95
          else None
wenzelm@54325
    96
        }
wenzelm@54325
    97
        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
wenzelm@55432
    98
      case _ =>
wenzelm@54528
    99
        PIDE.document_model(buffer) match {
wenzelm@54531
   100
          case Some(model) if !model.is_theory =>
wenzelm@56314
   101
            snapshot.version.nodes.load_commands(model.node_name) match {
wenzelm@54528
   102
              case cmd :: _ => Some(cmd)
wenzelm@54528
   103
              case Nil => None
wenzelm@54528
   104
            }
wenzelm@54528
   105
          case _ => None
wenzelm@54528
   106
        }
wenzelm@52971
   107
    }
wenzelm@52971
   108
  }
wenzelm@52977
   109
wenzelm@52977
   110
wenzelm@52977
   111
  /* overlays */
wenzelm@52977
   112
wenzelm@57873
   113
  private val overlays = Synchronized(Document.Overlays.empty)
wenzelm@52977
   114
wenzelm@52980
   115
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@57873
   116
    overlays.value(name)
wenzelm@52977
   117
wenzelm@52980
   118
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@57873
   119
    overlays.change(_.insert(command, fn, args))
wenzelm@52977
   120
wenzelm@52980
   121
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@57873
   122
    overlays.change(_.remove(command, fn, args))
wenzelm@52980
   123
wenzelm@52980
   124
wenzelm@55877
   125
  /* navigation */
wenzelm@52980
   126
wenzelm@56413
   127
  def push_position(view: View)
wenzelm@56413
   128
  {
wenzelm@56413
   129
    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
wenzelm@56413
   130
    if (navigator != null) {
wenzelm@56413
   131
      try {
wenzelm@56413
   132
        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
wenzelm@56413
   133
        m.invoke(null, view)
wenzelm@56413
   134
      }
wenzelm@56413
   135
      catch { case _: NoSuchMethodException => }
wenzelm@56413
   136
    }
wenzelm@56413
   137
  }
wenzelm@56413
   138
wenzelm@58545
   139
  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
wenzelm@58545
   140
  {
wenzelm@58545
   141
    GUI_Thread.require {}
wenzelm@58545
   142
wenzelm@58545
   143
    push_position(view)
wenzelm@58545
   144
wenzelm@58545
   145
    view.goToBuffer(buffer)
wenzelm@58545
   146
    try { view.getTextArea.moveCaretPosition(offset) }
wenzelm@58545
   147
    catch {
wenzelm@58545
   148
      case _: ArrayIndexOutOfBoundsException =>
wenzelm@58545
   149
      case _: IllegalArgumentException =>
wenzelm@58545
   150
    }
wenzelm@58545
   151
  }
wenzelm@58545
   152
wenzelm@55877
   153
  def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
wenzelm@52980
   154
  {
wenzelm@57612
   155
    GUI_Thread.require {}
wenzelm@52980
   156
wenzelm@56413
   157
    push_position(view)
wenzelm@56413
   158
wenzelm@54706
   159
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52980
   160
      case Some(buffer) =>
wenzelm@52980
   161
        view.goToBuffer(buffer)
wenzelm@52980
   162
        val text_area = view.getTextArea
wenzelm@52980
   163
wenzelm@52980
   164
        try {
wenzelm@52980
   165
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
wenzelm@52980
   166
          text_area.moveCaretPosition(line_start)
wenzelm@52980
   167
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
wenzelm@52980
   168
        }
wenzelm@52980
   169
        catch {
wenzelm@52980
   170
          case _: ArrayIndexOutOfBoundsException =>
wenzelm@52980
   171
          case _: IllegalArgumentException =>
wenzelm@52980
   172
        }
wenzelm@52980
   173
wenzelm@54706
   174
      case None if (new JFile(name)).isDirectory =>
wenzelm@54706
   175
        VFSBrowser.browseDirectory(view, name)
wenzelm@54706
   176
wenzelm@52980
   177
      case None =>
wenzelm@52980
   178
        val args =
wenzelm@54706
   179
          if (line <= 0) Array(name)
wenzelm@54706
   180
          else if (column <= 0) Array(name, "+line:" + line.toInt)
wenzelm@54706
   181
          else Array(name, "+line:" + line.toInt + "," + column.toInt)
wenzelm@52980
   182
        jEdit.openFiles(view, null, args)
wenzelm@52980
   183
    }
wenzelm@52980
   184
  }
wenzelm@52980
   185
wenzelm@55877
   186
wenzelm@55877
   187
  /* hyperlinks */
wenzelm@55877
   188
wenzelm@56461
   189
  def hyperlink_url(name: String): Hyperlink =
wenzelm@56461
   190
    new Hyperlink {
wenzelm@56494
   191
      val external = true
wenzelm@56729
   192
      def follow(view: View): Unit =
wenzelm@56729
   193
        Future.fork {
wenzelm@56461
   194
          try { Isabelle_System.open(name) }
wenzelm@56461
   195
          catch {
wenzelm@56461
   196
            case exn: Throwable =>
wenzelm@56461
   197
              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@56729
   198
          }
wenzelm@56729
   199
        }
wenzelm@56461
   200
      override def toString: String = "URL " + quote(name)
wenzelm@52980
   201
    }
wenzelm@55876
   202
wenzelm@58545
   203
  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
wenzelm@58545
   204
    new Hyperlink {
wenzelm@58545
   205
      val external = false
wenzelm@58545
   206
      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
wenzelm@58545
   207
      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
wenzelm@58545
   208
    }
wenzelm@58545
   209
wenzelm@55876
   210
  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
wenzelm@56461
   211
    new Hyperlink {
wenzelm@56494
   212
      val external = false
wenzelm@56729
   213
      def follow(view: View): Unit = goto_file(view, name, line, column)
wenzelm@56461
   214
      override def toString: String = "file " + quote(name)
wenzelm@56461
   215
    }
wenzelm@55876
   216
wenzelm@55884
   217
  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
wenzelm@55878
   218
    : Option[Hyperlink] =
wenzelm@55878
   219
  {
wenzelm@56458
   220
    val opt_name =
wenzelm@56458
   221
      if (Path.is_wellformed(source_name)) {
wenzelm@56458
   222
        if (Path.is_valid(source_name)) {
wenzelm@56458
   223
          val path = Path.explode(source_name)
wenzelm@56458
   224
          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
wenzelm@56458
   225
        }
wenzelm@56458
   226
        else None
wenzelm@55878
   227
      }
wenzelm@56458
   228
      else Some(source_name)
wenzelm@56458
   229
wenzelm@56458
   230
    opt_name match {
wenzelm@56458
   231
      case Some(name) =>
wenzelm@56458
   232
        JEdit_Lib.jedit_buffer(name) match {
wenzelm@56458
   233
          case Some(buffer) if offset > 0 =>
wenzelm@56458
   234
            val (line, column) =
wenzelm@56458
   235
              JEdit_Lib.buffer_lock(buffer) {
wenzelm@56458
   236
                ((1, 1) /:
wenzelm@56458
   237
                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
wenzelm@56458
   238
                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
wenzelm@56458
   239
                      Symbol.advance_line_column)
wenzelm@56458
   240
              }
wenzelm@56458
   241
            Some(hyperlink_file(name, line, column))
wenzelm@56458
   242
          case _ => Some(hyperlink_file(name, line))
wenzelm@56458
   243
        }
wenzelm@56458
   244
      case None => None
wenzelm@55878
   245
    }
wenzelm@55878
   246
  }
wenzelm@55876
   247
wenzelm@56461
   248
  override def hyperlink_command(
wenzelm@56461
   249
    snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
wenzelm@56461
   250
  {
wenzelm@56461
   251
    if (snapshot.is_outdated) None
wenzelm@56461
   252
    else {
wenzelm@56461
   253
      snapshot.state.find_command(snapshot.version, command.id) match {
wenzelm@56461
   254
        case None => None
wenzelm@56461
   255
        case Some((node, _)) =>
wenzelm@56461
   256
          val file_name = command.node_name.node
wenzelm@56461
   257
          val sources_iterator =
wenzelm@56461
   258
            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm@56461
   259
              (if (offset == 0) Iterator.empty
wenzelm@56462
   260
               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
wenzelm@56461
   261
          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
wenzelm@56461
   262
          Some(hyperlink_file(file_name, line, column))
wenzelm@56461
   263
      }
wenzelm@55876
   264
    }
wenzelm@56461
   265
  }
wenzelm@56461
   266
wenzelm@56461
   267
  def hyperlink_command_id(
wenzelm@56461
   268
    snapshot: Document.Snapshot,
wenzelm@56461
   269
    id: Document_ID.Generic,
wenzelm@57878
   270
    offset: Symbol.Offset = 0): Option[Hyperlink] =
wenzelm@56461
   271
  {
wenzelm@56461
   272
    snapshot.state.find_command(snapshot.version, id) match {
wenzelm@56461
   273
      case Some((node, command)) => hyperlink_command(snapshot, command, offset)
wenzelm@56461
   274
      case None => None
wenzelm@56461
   275
    }
wenzelm@56461
   276
  }
wenzelm@52971
   277
}