src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Fri Oct 11 20:45:21 2013 +0200 (2013-10-11)
changeset 54325 2c4155003352
parent 53845 08721d7b2262
child 54461 6c360a6ade0e
permissions -rw-r--r--
clarified Editor.current_command: allow outdated snapshot;
more accurate Document_View.perspective based on current_command for proper state output (see also 88c6e630c15f and ef62204a126b);
     1 /*  Title:      Tools/jEdit/src/jedit_editor.scala
     2     Author:     Makarius
     3 
     4 PIDE editor operations for jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 
    13 import org.gjt.sp.jedit.{jEdit, View}
    14 
    15 
    16 class JEdit_Editor extends Editor[View]
    17 {
    18   /* session */
    19 
    20   override def session: Session = PIDE.session
    21 
    22   override def flush()
    23   {
    24     Swing_Thread.require()
    25 
    26     session.update(
    27       (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    28         case (edits, buffer) =>
    29           JEdit_Lib.buffer_lock(buffer) {
    30             PIDE.document_model(buffer) match {
    31               case Some(model) => model.flushed_edits() ::: edits
    32               case None => edits
    33             }
    34           }
    35       }
    36     )
    37   }
    38 
    39 
    40   /* current situation */
    41 
    42   override def current_context: View =
    43     Swing_Thread.require { jEdit.getActiveView() }
    44 
    45   override def current_node(view: View): Option[Document.Node.Name] =
    46     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    47 
    48   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    49     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    50 
    51   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    52   {
    53     Swing_Thread.require()
    54 
    55     JEdit_Lib.jedit_buffer(name.node) match {
    56       case Some(buffer) =>
    57         PIDE.document_model(buffer) match {
    58           case Some(model) => model.snapshot
    59           case None => session.snapshot(name)
    60         }
    61       case None => session.snapshot(name)
    62     }
    63   }
    64 
    65   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    66   {
    67     Swing_Thread.require()
    68 
    69     val text_area = view.getTextArea
    70     PIDE.document_view(text_area) match {
    71       case Some(doc_view) =>
    72         val node = snapshot.version.nodes(doc_view.model.node_name)
    73         val caret = snapshot.revert(text_area.getCaretPosition)
    74         if (caret < text_area.getBuffer.getLength) {
    75           val caret_commands = node.command_range(caret)
    76           if (caret_commands.hasNext) {
    77             val (cmd0, _) = caret_commands.next
    78             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    79           }
    80           else None
    81         }
    82         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    83       case None => None
    84     }
    85   }
    86 
    87 
    88   /* overlays */
    89 
    90   private var overlays = Document.Overlays.empty
    91 
    92   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    93     synchronized { overlays(name) }
    94 
    95   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    96     synchronized { overlays = overlays.insert(command, fn, args) }
    97 
    98   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    99     synchronized { overlays = overlays.remove(command, fn, args) }
   100 
   101 
   102   /* hyperlinks */
   103 
   104   def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
   105   {
   106     Swing_Thread.require()
   107 
   108     JEdit_Lib.jedit_buffer(file_name) match {
   109       case Some(buffer) =>
   110         view.goToBuffer(buffer)
   111         val text_area = view.getTextArea
   112 
   113         try {
   114           val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
   115           text_area.moveCaretPosition(line_start)
   116           if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
   117         }
   118         catch {
   119           case _: ArrayIndexOutOfBoundsException =>
   120           case _: IllegalArgumentException =>
   121         }
   122 
   123       case None =>
   124         val args =
   125           if (line <= 0) Array(file_name)
   126           else if (column <= 0) Array(file_name, "+line:" + line.toInt)
   127           else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
   128         jEdit.openFiles(view, null, args)
   129     }
   130   }
   131 
   132   override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
   133     new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
   134 
   135   override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
   136     : Option[Hyperlink] =
   137   {
   138     if (snapshot.is_outdated) None
   139     else {
   140       snapshot.state.find_command(snapshot.version, command.id) match {
   141         case None => None
   142         case Some((node, _)) =>
   143           val file_name = command.node_name.node
   144           val sources =
   145             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   146               (if (offset == 0) Iterator.empty
   147                else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
   148           val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   149           Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
   150       }
   151     }
   152   }
   153 }