src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Mon Aug 12 17:11:27 2013 +0200 (2013-08-12)
changeset 52980 28f59ca8ce78
parent 52978 37fbb3fde380
child 53844 71f103629327
permissions -rw-r--r--
manage hyperlinks via PIDE editor interface;
     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)
    66     : Option[(Command, Text.Offset)] =
    67   {
    68     Swing_Thread.require()
    69 
    70     if (snapshot.is_outdated) None
    71     else {
    72       val text_area = view.getTextArea
    73       PIDE.document_view(text_area) match {
    74         case Some(doc_view) =>
    75           val node = snapshot.version.nodes(doc_view.model.node_name)
    76           val caret_commands = node.command_range(text_area.getCaretPosition)
    77           if (caret_commands.hasNext) Some(caret_commands.next) else None
    78         case None => None
    79       }
    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 }