src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Sat Jan 07 14:34:53 2017 +0100 (2017-01-07)
changeset 64817 0bb6b582bb4f
parent 64813 7283f41d05ab
child 64829 07f209e957bc
permissions -rw-r--r--
separate Buffer_Model vs. File_Model;
misc tuning and clarification;
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@64817
    25
  override def flush(hidden: Boolean = false): Unit =
wenzelm@64817
    26
    GUI_Thread.require {
wenzelm@64817
    27
      val (doc_blobs, edits) = Document_Model.flush_edits(hidden)
wenzelm@64817
    28
      session.update(doc_blobs, edits)
wenzelm@64817
    29
    }
wenzelm@52974
    30
wenzelm@64524
    31
  private val delay1_flush =
wenzelm@57612
    32
    GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
wenzelm@54461
    33
wenzelm@64524
    34
  private val delay2_flush =
wenzelm@64524
    35
    GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
wenzelm@64521
    36
wenzelm@64524
    37
  def invoke(): Unit = delay1_flush.invoke()
wenzelm@64524
    38
  def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
wenzelm@54461
    39
wenzelm@60933
    40
  def stable_tip_version(): Option[Document.Version] =
wenzelm@60933
    41
    GUI_Thread.require {
wenzelm@64817
    42
      if (Document_Model.is_stable())
wenzelm@60933
    43
        session.current_state().stable_tip_version
wenzelm@60933
    44
      else None
wenzelm@60933
    45
    }
wenzelm@60933
    46
wenzelm@64799
    47
  def visible_node(name: Document.Node.Name): Boolean =
wenzelm@64799
    48
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@64799
    49
      case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty
wenzelm@64799
    50
      case None => false
wenzelm@64799
    51
    }
wenzelm@64799
    52
wenzelm@52977
    53
wenzelm@52977
    54
  /* current situation */
wenzelm@52977
    55
wenzelm@52980
    56
  override def current_context: View =
wenzelm@57612
    57
    GUI_Thread.require { jEdit.getActiveView() }
wenzelm@52971
    58
wenzelm@52980
    59
  override def current_node(view: View): Option[Document.Node.Name] =
wenzelm@64813
    60
    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
wenzelm@52971
    61
wenzelm@52980
    62
  override def current_node_snapshot(view: View): Option[Document.Snapshot] =
wenzelm@64813
    63
    GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
wenzelm@52971
    64
wenzelm@52980
    65
  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
wenzelm@52974
    66
  {
wenzelm@57612
    67
    GUI_Thread.require {}
wenzelm@64817
    68
    Document_Model.get(name) match {
wenzelm@64817
    69
      case Some(model) => model.snapshot
wenzelm@52974
    70
      case None => session.snapshot(name)
wenzelm@52974
    71
    }
wenzelm@52974
    72
  }
wenzelm@52974
    73
wenzelm@53844
    74
  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
wenzelm@52971
    75
  {
wenzelm@57612
    76
    GUI_Thread.require {}
wenzelm@52971
    77
wenzelm@54325
    78
    val text_area = view.getTextArea
wenzelm@54528
    79
    val buffer = view.getBuffer
wenzelm@54528
    80
wenzelm@54325
    81
    PIDE.document_view(text_area) match {
wenzelm@55432
    82
      case Some(doc_view) if doc_view.model.is_theory =>
wenzelm@54325
    83
        val node = snapshot.version.nodes(doc_view.model.node_name)
wenzelm@54325
    84
        val caret = snapshot.revert(text_area.getCaretPosition)
wenzelm@54528
    85
        if (caret < buffer.getLength) {
wenzelm@56373
    86
          val caret_command_iterator = node.command_iterator(caret)
wenzelm@56373
    87
          if (caret_command_iterator.hasNext) {
wenzelm@56373
    88
            val (cmd0, _) = caret_command_iterator.next
wenzelm@54325
    89
            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
wenzelm@53844
    90
          }
wenzelm@54325
    91
          else None
wenzelm@54325
    92
        }
wenzelm@54325
    93
        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
wenzelm@55432
    94
      case _ =>
wenzelm@64813
    95
        Document_Model.get(buffer) match {
wenzelm@54531
    96
          case Some(model) if !model.is_theory =>
wenzelm@64799
    97
            snapshot.version.nodes.commands_loading(model.node_name) match {
wenzelm@54528
    98
              case cmd :: _ => Some(cmd)
wenzelm@54528
    99
              case Nil => None
wenzelm@54528
   100
            }
wenzelm@54528
   101
          case _ => None
wenzelm@54528
   102
        }
wenzelm@52971
   103
    }
wenzelm@52971
   104
  }
wenzelm@52977
   105
wenzelm@52977
   106
wenzelm@52977
   107
  /* overlays */
wenzelm@52977
   108
wenzelm@57873
   109
  private val overlays = Synchronized(Document.Overlays.empty)
wenzelm@52977
   110
wenzelm@52980
   111
  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
wenzelm@57873
   112
    overlays.value(name)
wenzelm@52977
   113
wenzelm@52980
   114
  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@57873
   115
    overlays.change(_.insert(command, fn, args))
wenzelm@52977
   116
wenzelm@52980
   117
  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
wenzelm@57873
   118
    overlays.change(_.remove(command, fn, args))
wenzelm@52980
   119
wenzelm@52980
   120
wenzelm@55877
   121
  /* navigation */
wenzelm@52980
   122
wenzelm@56413
   123
  def push_position(view: View)
wenzelm@56413
   124
  {
wenzelm@56413
   125
    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
wenzelm@56413
   126
    if (navigator != null) {
wenzelm@59080
   127
      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
wenzelm@56413
   128
      catch { case _: NoSuchMethodException => }
wenzelm@56413
   129
    }
wenzelm@56413
   130
  }
wenzelm@56413
   131
wenzelm@60893
   132
  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
wenzelm@58545
   133
  {
wenzelm@58545
   134
    GUI_Thread.require {}
wenzelm@58545
   135
wenzelm@58545
   136
    push_position(view)
wenzelm@58545
   137
wenzelm@60893
   138
    if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
wenzelm@58545
   139
    try { view.getTextArea.moveCaretPosition(offset) }
wenzelm@58545
   140
    catch {
wenzelm@58545
   141
      case _: ArrayIndexOutOfBoundsException =>
wenzelm@58545
   142
      case _: IllegalArgumentException =>
wenzelm@58545
   143
    }
wenzelm@58545
   144
  }
wenzelm@58545
   145
wenzelm@64653
   146
  def goto_file(focus: Boolean, view: View, name: String): Unit =
wenzelm@64653
   147
    goto_file(focus, view, Line.Node_Position(name))
wenzelm@64653
   148
wenzelm@64653
   149
  def goto_file(focus: Boolean, view: View, pos: Line.Node_Position)
wenzelm@52980
   150
  {
wenzelm@57612
   151
    GUI_Thread.require {}
wenzelm@52980
   152
wenzelm@56413
   153
    push_position(view)
wenzelm@56413
   154
wenzelm@64653
   155
    val name = pos.name
wenzelm@64653
   156
    val line = pos.line
wenzelm@64653
   157
    val column = pos.column
wenzelm@64653
   158
wenzelm@54706
   159
    JEdit_Lib.jedit_buffer(name) match {
wenzelm@52980
   160
      case Some(buffer) =>
wenzelm@60893
   161
        if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
wenzelm@52980
   162
        val text_area = view.getTextArea
wenzelm@52980
   163
wenzelm@52980
   164
        try {
wenzelm@64653
   165
          val line_start = text_area.getBuffer.getLineStartOffset(line)
wenzelm@52980
   166
          text_area.moveCaretPosition(line_start)
wenzelm@64653
   167
          if (column > 0) text_area.moveCaretPosition(line_start + column)
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@64653
   180
          else if (column <= 0) Array(name, "+line:" + (line + 1))
wenzelm@64653
   181
          else Array(name, "+line:" + (line + 1) + "," + (column + 1))
wenzelm@52980
   182
        jEdit.openFiles(view, null, args)
wenzelm@52980
   183
    }
wenzelm@52980
   184
  }
wenzelm@52980
   185
wenzelm@61660
   186
  def goto_doc(view: View, path: Path)
wenzelm@61660
   187
  {
wenzelm@61660
   188
    if (path.is_file)
wenzelm@61660
   189
      goto_file(true, view, File.platform_path(path))
wenzelm@61660
   190
    else {
wenzelm@61660
   191
      Standard_Thread.fork("documentation") {
wenzelm@61660
   192
        try { Doc.view(path) }
wenzelm@61660
   193
        catch {
wenzelm@61660
   194
          case exn: Throwable =>
wenzelm@62062
   195
            GUI_Thread.later {
wenzelm@62062
   196
              GUI.error_dialog(view,
wenzelm@62062
   197
                "Documentation error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@62062
   198
            }
wenzelm@61660
   199
        }
wenzelm@61660
   200
      }
wenzelm@61660
   201
    }
wenzelm@61660
   202
  }
wenzelm@61660
   203
wenzelm@55877
   204
wenzelm@55877
   205
  /* hyperlinks */
wenzelm@55877
   206
wenzelm@61660
   207
  def hyperlink_doc(name: String): Option[Hyperlink] =
wenzelm@61660
   208
    Doc.contents().collectFirst({
wenzelm@61660
   209
      case doc: Doc.Text_File if doc.name == name => doc.path
wenzelm@61660
   210
      case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
wenzelm@61660
   211
        new Hyperlink {
wenzelm@64663
   212
          override val external = !path.is_file
wenzelm@61660
   213
          def follow(view: View): Unit = goto_doc(view, path)
wenzelm@61660
   214
          override def toString: String = "doc " + quote(name)
wenzelm@61660
   215
        })
wenzelm@61660
   216
wenzelm@56461
   217
  def hyperlink_url(name: String): Hyperlink =
wenzelm@56461
   218
    new Hyperlink {
wenzelm@64663
   219
      override val external = true
wenzelm@56729
   220
      def follow(view: View): Unit =
wenzelm@61557
   221
        Standard_Thread.fork("hyperlink_url") {
wenzelm@62248
   222
          try { Isabelle_System.open(Url.escape(name)) }
wenzelm@56461
   223
          catch {
wenzelm@56461
   224
            case exn: Throwable =>
wenzelm@62062
   225
              GUI_Thread.later {
wenzelm@62062
   226
                GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
wenzelm@62062
   227
              }
wenzelm@56729
   228
          }
wenzelm@56729
   229
        }
wenzelm@56461
   230
      override def toString: String = "URL " + quote(name)
wenzelm@52980
   231
    }
wenzelm@55876
   232
wenzelm@60893
   233
  def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
wenzelm@58545
   234
    new Hyperlink {
wenzelm@60893
   235
      def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
wenzelm@58545
   236
      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
wenzelm@58545
   237
    }
wenzelm@58545
   238
wenzelm@64653
   239
  def hyperlink_file(focus: Boolean, name: String): Hyperlink =
wenzelm@64653
   240
    hyperlink_file(focus, Line.Node_Position(name))
wenzelm@64653
   241
wenzelm@64653
   242
  def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
wenzelm@56461
   243
    new Hyperlink {
wenzelm@64653
   244
      def follow(view: View): Unit = goto_file(focus, view, pos)
wenzelm@64653
   245
      override def toString: String = "file " + quote(pos.name)
wenzelm@56461
   246
    }
wenzelm@55876
   247
wenzelm@64653
   248
  def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
wenzelm@55878
   249
    : Option[Hyperlink] =
wenzelm@55878
   250
  {
wenzelm@64657
   251
    for (name <- PIDE.resources.source_file(source_name)) yield {
wenzelm@64657
   252
      JEdit_Lib.jedit_buffer(name) match {
wenzelm@64657
   253
        case Some(buffer) if offset > 0 =>
wenzelm@64657
   254
          val pos =
wenzelm@64657
   255
            JEdit_Lib.buffer_lock(buffer) {
wenzelm@64657
   256
              (Line.Position.zero /:
wenzelm@64657
   257
                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
wenzelm@64682
   258
                  zipWithIndex.takeWhile(p => p._2 < offset - 1).
wenzelm@64682
   259
                  map(_._1)))(_.advance(_, Text.Length))
wenzelm@64657
   260
            }
wenzelm@64657
   261
          hyperlink_file(focus, Line.Node_Position(name, pos))
wenzelm@64657
   262
        case _ =>
wenzelm@64657
   263
          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
wenzelm@55878
   264
      }
wenzelm@55878
   265
    }
wenzelm@55878
   266
  }
wenzelm@55876
   267
wenzelm@56461
   268
  override def hyperlink_command(
wenzelm@64664
   269
    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
wenzelm@60893
   270
      : Option[Hyperlink] =
wenzelm@56461
   271
  {
wenzelm@56461
   272
    if (snapshot.is_outdated) None
wenzelm@64665
   273
    else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
wenzelm@56461
   274
  }
wenzelm@56461
   275
wenzelm@61011
   276
  def is_hyperlink_position(snapshot: Document.Snapshot,
wenzelm@61011
   277
    text_offset: Text.Offset, pos: Position.T): Boolean =
wenzelm@61011
   278
  {
wenzelm@61011
   279
    pos match {
wenzelm@64667
   280
      case Position.Item_Id(id, range) if range.start > 0 =>
wenzelm@64665
   281
        snapshot.find_command(id) match {
wenzelm@61011
   282
          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
wenzelm@61011
   283
            node.command_start(command) match {
wenzelm@64667
   284
              case Some(start) => text_offset == start + command.chunk.decode(range.start)
wenzelm@61011
   285
              case None => false
wenzelm@61011
   286
            }
wenzelm@61011
   287
          case _ => false
wenzelm@61011
   288
        }
wenzelm@61011
   289
      case _ => false
wenzelm@61011
   290
    }
wenzelm@61011
   291
  }
wenzelm@61011
   292
wenzelm@60893
   293
  def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
wenzelm@60893
   294
      : Option[Hyperlink] =
wenzelm@60874
   295
    pos match {
wenzelm@64667
   296
      case Position.Item_File(name, line, range) =>
wenzelm@64667
   297
        hyperlink_source_file(focus, name, line, range.start)
wenzelm@64667
   298
      case Position.Item_Id(id, range) =>
wenzelm@64667
   299
        hyperlink_command(focus, snapshot, id, range.start)
wenzelm@60874
   300
      case _ => None
wenzelm@60874
   301
    }
wenzelm@60874
   302
wenzelm@60893
   303
  def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
wenzelm@60893
   304
      : Option[Hyperlink] =
wenzelm@60874
   305
    pos match {
wenzelm@64667
   306
      case Position.Item_Def_File(name, line, range) =>
wenzelm@64667
   307
        hyperlink_source_file(focus, name, line, range.start)
wenzelm@64667
   308
      case Position.Item_Def_Id(id, range) =>
wenzelm@64667
   309
        hyperlink_command(focus, snapshot, id, range.start)
wenzelm@60874
   310
      case _ => None
wenzelm@60874
   311
    }
wenzelm@52971
   312
}