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