src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Tue Nov 19 20:59:05 2013 +0100 (2013-11-19)
changeset 54522 761be40990f1
parent 54521 744ea0025e11
child 54528 842adea880a4
permissions -rw-r--r--
tuned signature;
     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     val edits = PIDE.document_models().flatMap(_.flushed_edits())
    27     if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
    28   }
    29 
    30   private val delay_flush =
    31     Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    32 
    33   def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
    34 
    35 
    36   /* current situation */
    37 
    38   override def current_context: View =
    39     Swing_Thread.require { jEdit.getActiveView() }
    40 
    41   override def current_node(view: View): Option[Document.Node.Name] =
    42     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    43 
    44   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    45     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    46 
    47   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    48   {
    49     Swing_Thread.require()
    50 
    51     JEdit_Lib.jedit_buffer(name.node) match {
    52       case Some(buffer) =>
    53         PIDE.document_model(buffer) match {
    54           case Some(model) => model.snapshot
    55           case None => session.snapshot(name)
    56         }
    57       case None => session.snapshot(name)
    58     }
    59   }
    60 
    61   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    62   {
    63     Swing_Thread.require()
    64 
    65     val text_area = view.getTextArea
    66     PIDE.document_view(text_area) match {
    67       case Some(doc_view) =>
    68         val node = snapshot.version.nodes(doc_view.model.node_name)
    69         val caret = snapshot.revert(text_area.getCaretPosition)
    70         if (caret < text_area.getBuffer.getLength) {
    71           val caret_commands = node.command_range(caret)
    72           if (caret_commands.hasNext) {
    73             val (cmd0, _) = caret_commands.next
    74             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    75           }
    76           else None
    77         }
    78         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    79       case None => None
    80     }
    81   }
    82 
    83 
    84   /* overlays */
    85 
    86   private var overlays = Document.Overlays.empty
    87 
    88   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    89     synchronized { overlays(name) }
    90 
    91   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    92     synchronized { overlays = overlays.insert(command, fn, args) }
    93 
    94   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    95     synchronized { overlays = overlays.remove(command, fn, args) }
    96 
    97 
    98   /* hyperlinks */
    99 
   100   def goto(view: View, file_name: String, line: Int = 0, column: Int = 0)
   101   {
   102     Swing_Thread.require()
   103 
   104     JEdit_Lib.jedit_buffer(file_name) match {
   105       case Some(buffer) =>
   106         view.goToBuffer(buffer)
   107         val text_area = view.getTextArea
   108 
   109         try {
   110           val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
   111           text_area.moveCaretPosition(line_start)
   112           if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
   113         }
   114         catch {
   115           case _: ArrayIndexOutOfBoundsException =>
   116           case _: IllegalArgumentException =>
   117         }
   118 
   119       case None =>
   120         val args =
   121           if (line <= 0) Array(file_name)
   122           else if (column <= 0) Array(file_name, "+line:" + line.toInt)
   123           else Array(file_name, "+line:" + line.toInt + "," + column.toInt)
   124         jEdit.openFiles(view, null, args)
   125     }
   126   }
   127 
   128   override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink =
   129     new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) }
   130 
   131   override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
   132     : Option[Hyperlink] =
   133   {
   134     if (snapshot.is_outdated) None
   135     else {
   136       snapshot.state.find_command(snapshot.version, command.id) match {
   137         case None => None
   138         case Some((node, _)) =>
   139           val file_name = command.node_name.node
   140           val sources =
   141             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   142               (if (offset == 0) Iterator.empty
   143                else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
   144           val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   145           Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
   146       }
   147     }
   148   }
   149 }