src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Wed Nov 23 16:15:17 2016 +0100 (2016-11-23)
changeset 64521 1aef5a0e18d7
parent 62248 dca0bac351b2
child 64524 e6a3c55b929b
permissions -rw-r--r--
delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
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@61728
    31
  override def flush(hidden: Boolean = false)
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@61728
    43
    val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective
wenzelm@61544
    44
    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@64521
    50
  private val delay_update_flush =
wenzelm@64521
    51
    GUI_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay") * 3.0)) { flush() }
wenzelm@64521
    52
wenzelm@56770
    53
  def invoke(): Unit = delay_flush.invoke()
wenzelm@64521
    54
  def invoke_update(): Unit = { delay_flush.invoke(); delay_update_flush.invoke() }
wenzelm@54461
    55
wenzelm@60933
    56
  def stable_tip_version(): Option[Document.Version] =
wenzelm@60933
    57
    GUI_Thread.require {
wenzelm@60933
    58
      if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable))
wenzelm@60933
    59
        session.current_state().stable_tip_version
wenzelm@60933
    60
      else None
wenzelm@60933
    61
    }
wenzelm@60933
    62
wenzelm@52977
    63
wenzelm@52977
    64
  /* current situation */
wenzelm@52977
    65
wenzelm@52980
    66
  override def current_context: View =
wenzelm@57612
    67
    GUI_Thread.require { jEdit.getActiveView() }
wenzelm@52971
    68
wenzelm@52980
    69
  override def current_node(view: View): Option[Document.Node.Name] =
wenzelm@57612
    70
    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
wenzelm@52971
    71
wenzelm@52980
    72
  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
wenzelm@57612
    73
    GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
wenzelm@52971
    74
wenzelm@52980
    75
  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
wenzelm@52974
    76
  {
wenzelm@57612
    77
    GUI_Thread.require {}
wenzelm@52974
    78
wenzelm@56457
    79
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52974
    80
      case Some(buffer) =>
wenzelm@52974
    81
        PIDE.document_model(buffer) match {
wenzelm@52974
    82
          case Some(model) => model.snapshot
wenzelm@52974
    83
          case None => session.snapshot(name)
wenzelm@52974
    84
        }
wenzelm@52974
    85
      case None => session.snapshot(name)
wenzelm@52974
    86
    }
wenzelm@52974
    87
  }
wenzelm@52974
    88
wenzelm@53844
    89
  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
wenzelm@52971
    90
  {
wenzelm@57612
    91
    GUI_Thread.require {}
wenzelm@52971
    92
wenzelm@54325
    93
    val text_area = view.getTextArea
wenzelm@54528
    94
    val buffer = view.getBuffer
wenzelm@54528
    95
wenzelm@54325
    96
    PIDE.document_view(text_area) match {
wenzelm@55432
    97
      case Some(doc_view) if doc_view.model.is_theory =>
wenzelm@54325
    98
        val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@54325
    99
        val caret = snapshot.revert(text_area.getCaretPosition)
wenzelm@54528
   100
        if (caret < buffer.getLength) {
wenzelm@56373
   101
          val caret_command_iterator = node.command_iterator(caret)
wenzelm@56373
   102
          if (caret_command_iterator.hasNext) {
wenzelm@56373
   103
            val (cmd0, _) = caret_command_iterator.next
wenzelm@54325
   104
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
wenzelm@53844
   105
          }
wenzelm@54325
   106
          else None
wenzelm@54325
   107
        }
wenzelm@54325
   108
        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
wenzelm@55432
   109
      case _ =>
wenzelm@54528
   110
        PIDE.document_model(buffer) match {
wenzelm@54531
   111
          case Some(model) if !model.is_theory =>
wenzelm@56314
   112
            snapshot.version.nodes.load_commands(model.node_name) match {
wenzelm@54528
   113
              case cmd :: _ => Some(cmd)
wenzelm@54528
   114
              case Nil => None
wenzelm@54528
   115
            }
wenzelm@54528
   116
          case _ => None
wenzelm@54528
   117
        }
wenzelm@52971
   118
    }
wenzelm@52971
   119
  }
wenzelm@52977
   120
wenzelm@52977
   121
wenzelm@52977
   122
  /* overlays */
wenzelm@52977
   123
wenzelm@57873
   124
  private val overlays = Synchronized(Document.Overlays.empty)
wenzelm@52977
   125
wenzelm@52980
   126
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@57873
   127
    overlays.value(name)
wenzelm@52977
   128
wenzelm@52980
   129
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@57873
   130
    overlays.change(_.insert(command, fn, args))
wenzelm@52977
   131
wenzelm@52980
   132
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@57873
   133
    overlays.change(_.remove(command, fn, args))
wenzelm@52980
   134
wenzelm@52980
   135
wenzelm@55877
   136
  /* navigation */
wenzelm@52980
   137
wenzelm@56413
   138
  def push_position(view: View)
wenzelm@56413
   139
  {
wenzelm@56413
   140
    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
wenzelm@56413
   141
    if (navigator != null) {
wenzelm@59080
   142
      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
wenzelm@56413
   143
      catch { case _: NoSuchMethodException => }
wenzelm@56413
   144
    }
wenzelm@56413
   145
  }
wenzelm@56413
   146
wenzelm@60893
   147
  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
wenzelm@58545
   148
  {
wenzelm@58545
   149
    GUI_Thread.require {}
wenzelm@58545
   150
wenzelm@58545
   151
    push_position(view)
wenzelm@58545
   152
wenzelm@60893
   153
    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
wenzelm@58545
   154
    try { view.getTextArea.moveCaretPosition(offset) }
wenzelm@58545
   155
    catch {
wenzelm@58545
   156
      case _: ArrayIndexOutOfBoundsException =>
wenzelm@58545
   157
      case _: IllegalArgumentException =>
wenzelm@58545
   158
    }
wenzelm@58545
   159
  }
wenzelm@58545
   160
wenzelm@60893
   161
  def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
wenzelm@52980
   162
  {
wenzelm@57612
   163
    GUI_Thread.require {}
wenzelm@52980
   164
wenzelm@56413
   165
    push_position(view)
wenzelm@56413
   166
wenzelm@54706
   167
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52980
   168
      case Some(buffer) =>
wenzelm@60893
   169
        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
wenzelm@52980
   170
        val text_area = view.getTextArea
wenzelm@52980
   171
wenzelm@52980
   172
        try {
wenzelm@52980
   173
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
wenzelm@52980
   174
          text_area.moveCaretPosition(line_start)
wenzelm@52980
   175
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
wenzelm@52980
   176
        }
wenzelm@52980
   177
        catch {
wenzelm@52980
   178
          case _: ArrayIndexOutOfBoundsException =>
wenzelm@52980
   179
          case _: IllegalArgumentException =>
wenzelm@52980
   180
        }
wenzelm@52980
   181
wenzelm@54706
   182
      case None if (new JFile(name)).isDirectory =>
wenzelm@54706
   183
        VFSBrowser.browseDirectory(view, name)
wenzelm@54706
   184
wenzelm@52980
   185
      case None =>
wenzelm@52980
   186
        val args =
wenzelm@54706
   187
          if (line <= 0) Array(name)
wenzelm@54706
   188
          else if (column <= 0) Array(name, "+line:" + line.toInt)
wenzelm@54706
   189
          else Array(name, "+line:" + line.toInt + "," + column.toInt)
wenzelm@52980
   190
        jEdit.openFiles(view, null, args)
wenzelm@52980
   191
    }
wenzelm@52980
   192
  }
wenzelm@52980
   193
wenzelm@61660
   194
  def goto_doc(view: View, path: Path)
wenzelm@61660
   195
  {
wenzelm@61660
   196
    if (path.is_file)
wenzelm@61660
   197
      goto_file(true, view, File.platform_path(path))
wenzelm@61660
   198
    else {
wenzelm@61660
   199
      Standard_Thread.fork("documentation") {
wenzelm@61660
   200
        try { Doc.view(path) }
wenzelm@61660
   201
        catch {
wenzelm@61660
   202
          case exn: Throwable =>
wenzelm@62062
   203
            GUI_Thread.later {
wenzelm@62062
   204
              GUI.error_dialog(view,
wenzelm@62062
   205
                "Documentation error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@62062
   206
            }
wenzelm@61660
   207
        }
wenzelm@61660
   208
      }
wenzelm@61660
   209
    }
wenzelm@61660
   210
  }
wenzelm@61660
   211
wenzelm@55877
   212
wenzelm@55877
   213
  /* hyperlinks */
wenzelm@55877
   214
wenzelm@61660
   215
  def hyperlink_doc(name: String): Option[Hyperlink] =
wenzelm@61660
   216
    Doc.contents().collectFirst({
wenzelm@61660
   217
      case doc: Doc.Text_File if doc.name == name => doc.path
wenzelm@61660
   218
      case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
wenzelm@61660
   219
        new Hyperlink {
wenzelm@61660
   220
          val external = !path.is_file
wenzelm@61660
   221
          def follow(view: View): Unit = goto_doc(view, path)
wenzelm@61660
   222
          override def toString: String = "doc " + quote(name)
wenzelm@61660
   223
        })
wenzelm@61660
   224
wenzelm@56461
   225
  def hyperlink_url(name: String): Hyperlink =
wenzelm@56461
   226
    new Hyperlink {
wenzelm@56494
   227
      val external = true
wenzelm@56729
   228
      def follow(view: View): Unit =
wenzelm@61557
   229
        Standard_Thread.fork("hyperlink_url") {
wenzelm@62248
   230
          try { Isabelle_System.open(Url.escape(name)) }
wenzelm@56461
   231
          catch {
wenzelm@56461
   232
            case exn: Throwable =>
wenzelm@62062
   233
              GUI_Thread.later {
wenzelm@62062
   234
                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@62062
   235
              }
wenzelm@56729
   236
          }
wenzelm@56729
   237
        }
wenzelm@56461
   238
      override def toString: String = "URL " + quote(name)
wenzelm@52980
   239
    }
wenzelm@55876
   240
wenzelm@60893
   241
  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
wenzelm@58545
   242
    new Hyperlink {
wenzelm@58545
   243
      val external = false
wenzelm@60893
   244
      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
wenzelm@58545
   245
      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
wenzelm@58545
   246
    }
wenzelm@58545
   247
wenzelm@60893
   248
  def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
wenzelm@56461
   249
    new Hyperlink {
wenzelm@56494
   250
      val external = false
wenzelm@60893
   251
      def follow(view: View): Unit = goto_file(focus, view, name, line, column)
wenzelm@56461
   252
      override def toString: String = "file " + quote(name)
wenzelm@56461
   253
    }
wenzelm@55876
   254
wenzelm@60893
   255
  def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
wenzelm@55878
   256
    : Option[Hyperlink] =
wenzelm@55878
   257
  {
wenzelm@56458
   258
    val opt_name =
wenzelm@56458
   259
      if (Path.is_wellformed(source_name)) {
wenzelm@56458
   260
        if (Path.is_valid(source_name)) {
wenzelm@56458
   261
          val path = Path.explode(source_name)
wenzelm@60988
   262
          Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
wenzelm@56458
   263
        }
wenzelm@56458
   264
        else None
wenzelm@55878
   265
      }
wenzelm@56458
   266
      else Some(source_name)
wenzelm@56458
   267
wenzelm@56458
   268
    opt_name match {
wenzelm@56458
   269
      case Some(name) =>
wenzelm@56458
   270
        JEdit_Lib.jedit_buffer(name) match {
wenzelm@56458
   271
          case Some(buffer) if offset > 0 =>
wenzelm@56458
   272
            val (line, column) =
wenzelm@56458
   273
              JEdit_Lib.buffer_lock(buffer) {
wenzelm@56458
   274
                ((1, 1) /:
wenzelm@56458
   275
                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
wenzelm@56458
   276
                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
wenzelm@56458
   277
                      Symbol.advance_line_column)
wenzelm@56458
   278
              }
wenzelm@60893
   279
            Some(hyperlink_file(focus, name, line, column))
wenzelm@60893
   280
          case _ => Some(hyperlink_file(focus, name, line))
wenzelm@56458
   281
        }
wenzelm@56458
   282
      case None => None
wenzelm@55878
   283
    }
wenzelm@55878
   284
  }
wenzelm@55876
   285
wenzelm@56461
   286
  override def hyperlink_command(
wenzelm@60893
   287
    focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
wenzelm@60893
   288
      : Option[Hyperlink] =
wenzelm@56461
   289
  {
wenzelm@56461
   290
    if (snapshot.is_outdated) None
wenzelm@56461
   291
    else {
wenzelm@56461
   292
      snapshot.state.find_command(snapshot.version, command.id) match {
wenzelm@56461
   293
        case None => None
wenzelm@56461
   294
        case Some((node, _)) =>
wenzelm@56461
   295
          val file_name = command.node_name.node
wenzelm@56461
   296
          val sources_iterator =
wenzelm@56461
   297
            node.commands.iterator.takeWhile(_ != command).map(_.source) ++
wenzelm@56461
   298
              (if (offset == 0) Iterator.empty
wenzelm@56462
   299
               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
wenzelm@56461
   300
          val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
wenzelm@60893
   301
          Some(hyperlink_file(focus, file_name, line, column))
wenzelm@56461
   302
      }
wenzelm@55876
   303
    }
wenzelm@56461
   304
  }
wenzelm@56461
   305
wenzelm@56461
   306
  def hyperlink_command_id(
wenzelm@60893
   307
    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
wenzelm@60893
   308
      : Option[Hyperlink] =
wenzelm@56461
   309
  {
wenzelm@56461
   310
    snapshot.state.find_command(snapshot.version, id) match {
wenzelm@60893
   311
      case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
wenzelm@56461
   312
      case None => None
wenzelm@56461
   313
    }
wenzelm@56461
   314
  }
wenzelm@60874
   315
wenzelm@61011
   316
  def is_hyperlink_position(snapshot: Document.Snapshot,
wenzelm@61011
   317
    text_offset: Text.Offset, pos: Position.T): Boolean =
wenzelm@61011
   318
  {
wenzelm@61011
   319
    pos match {
wenzelm@61011
   320
      case Position.Id_Offset0(id, offset) if offset > 0 =>
wenzelm@61011
   321
        snapshot.state.find_command(snapshot.version, id) match {
wenzelm@61011
   322
          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
wenzelm@61011
   323
            node.command_start(command) match {
wenzelm@61011
   324
              case Some(start) => text_offset == start + command.chunk.decode(offset)
wenzelm@61011
   325
              case None => false
wenzelm@61011
   326
            }
wenzelm@61011
   327
          case _ => false
wenzelm@61011
   328
        }
wenzelm@61011
   329
      case _ => false
wenzelm@61011
   330
    }
wenzelm@61011
   331
  }
wenzelm@61011
   332
wenzelm@60893
   333
  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
wenzelm@60893
   334
      : Option[Hyperlink] =
wenzelm@60874
   335
    pos match {
wenzelm@60874
   336
      case Position.Line_File(line, name) =>
wenzelm@60874
   337
        val offset = Position.Offset.unapply(pos) getOrElse 0
wenzelm@60893
   338
        hyperlink_source_file(focus, name, line, offset)
wenzelm@60874
   339
      case Position.Id_Offset0(id, offset) =>
wenzelm@60893
   340
        hyperlink_command_id(focus, snapshot, id, offset)
wenzelm@60874
   341
      case _ => None
wenzelm@60874
   342
    }
wenzelm@60874
   343
wenzelm@60893
   344
  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
wenzelm@60893
   345
      : Option[Hyperlink] =
wenzelm@60874
   346
    pos match {
wenzelm@60874
   347
      case Position.Def_Line_File(line, name) =>
wenzelm@60874
   348
        val offset = Position.Def_Offset.unapply(pos) getOrElse 0
wenzelm@60893
   349
        hyperlink_source_file(focus, name, line, offset)
wenzelm@60874
   350
      case Position.Def_Id_Offset0(id, offset) =>
wenzelm@60893
   351
        hyperlink_command_id(focus, snapshot, id, offset)
wenzelm@60874
   352
      case _ => None
wenzelm@60874
   353
    }
wenzelm@52971
   354
}