/* Title: Tools/jEdit/src/jedit_editor.scala
Author: Makarius
PIDE editor operations for jEdit.
*/
package isabelle.jedit
import isabelle._
import java.io.{File => JFile}
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.browser.VFSBrowser
class JEdit_Editor extends Editor[View]
{
/* session */
override def session: Session = PIDE.session
// owned by GUI thread
private var removed_nodes = Set.empty[Document.Node.Name]
def remove_node(name: Document.Node.Name): Unit =
GUI_Thread.require { removed_nodes += name }
override def flush()
{
GUI_Thread.require {}
val doc_blobs = PIDE.document_blobs()
val models = PIDE.document_models()
val removed = removed_nodes; removed_nodes = Set.empty
val removed_perspective =
(removed -- models.iterator.map(_.node_name)).toList.map(
name => (name, Document.Node.no_perspective_text))
val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
if (edits.nonEmpty) session.update(doc_blobs, edits)
}
private val delay_flush =
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
def invoke(): Unit = delay_flush.invoke()
/* current situation */
override def current_context: View =
GUI_Thread.require { jEdit.getActiveView() }
override def current_node(view: View): Option[Document.Node.Name] =
GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
override def current_node_snapshot(view: View): Option[Document.Snapshot] =
GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
{
GUI_Thread.require {}
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
PIDE.document_model(buffer) match {
case Some(model) => model.snapshot
case None => session.snapshot(name)
}
case None => session.snapshot(name)
}
}
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
{
GUI_Thread.require {}
val text_area = view.getTextArea
val buffer = view.getBuffer
PIDE.document_view(text_area) match {
case Some(doc_view) if doc_view.model.is_theory =>
val node = snapshot.version.nodes(doc_view.model.node_name)
val caret = snapshot.revert(text_area.getCaretPosition)
if (caret < buffer.getLength) {
val caret_command_iterator = node.command_iterator(caret)
if (caret_command_iterator.hasNext) {
val (cmd0, _) = caret_command_iterator.next
node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
}
else None
}
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
case _ =>
PIDE.document_model(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.load_commands(model.node_name) match {
case cmd :: _ => Some(cmd)
case Nil => None
}
case _ => None
}
}
}
/* overlays */
private val overlays = Synchronized(Document.Overlays.empty)
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
overlays.value(name)
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
overlays.change(_.insert(command, fn, args))
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
overlays.change(_.remove(command, fn, args))
/* navigation */
def push_position(view: View)
{
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
if (navigator != null) {
try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
catch { case _: NoSuchMethodException => }
}
}
def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
{
GUI_Thread.require {}
push_position(view)
view.goToBuffer(buffer)
try { view.getTextArea.moveCaretPosition(offset) }
catch {
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
}
def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
{
GUI_Thread.require {}
push_position(view)
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
view.goToBuffer(buffer)
val text_area = view.getTextArea
try {
val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
text_area.moveCaretPosition(line_start)
if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
}
catch {
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
case None if (new JFile(name)).isDirectory =>
VFSBrowser.browseDirectory(view, name)
case None =>
val args =
if (line <= 0) Array(name)
else if (column <= 0) Array(name, "+line:" + line.toInt)
else Array(name, "+line:" + line.toInt + "," + column.toInt)
jEdit.openFiles(view, null, args)
}
}
/* hyperlinks */
def hyperlink_url(name: String): Hyperlink =
new Hyperlink {
val external = true
def follow(view: View): Unit =
Future.fork {
try { Isabelle_System.open(name) }
catch {
case exn: Throwable =>
GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
}
}
override def toString: String = "URL " + quote(name)
}
def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
new Hyperlink {
val external = false
def follow(view: View): Unit = goto_buffer(view, buffer, offset)
override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
}
def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
new Hyperlink {
val external = false
def follow(view: View): Unit = goto_file(view, name, line, column)
override def toString: String = "file " + quote(name)
}
def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
: Option[Hyperlink] =
{
val opt_name =
if (Path.is_wellformed(source_name)) {
if (Path.is_valid(source_name)) {
val path = Path.explode(source_name)
Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
}
else None
}
else Some(source_name)
opt_name match {
case Some(name) =>
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) if offset > 0 =>
val (line, column) =
JEdit_Lib.buffer_lock(buffer) {
((1, 1) /:
(Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
Symbol.advance_line_column)
}
Some(hyperlink_file(name, line, column))
case _ => Some(hyperlink_file(name, line))
}
case None => None
}
}
override def hyperlink_command(
snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
{
if (snapshot.is_outdated) None
else {
snapshot.state.find_command(snapshot.version, command.id) match {
case None => None
case Some((node, _)) =>
val file_name = command.node_name.node
val sources_iterator =
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
(if (offset == 0) Iterator.empty
else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
Some(hyperlink_file(file_name, line, column))
}
}
}
def hyperlink_command_id(
snapshot: Document.Snapshot,
id: Document_ID.Generic,
offset: Symbol.Offset = 0): Option[Hyperlink] =
{
snapshot.state.find_command(snapshot.version, id) match {
case Some((node, command)) => hyperlink_command(snapshot, command, offset)
case None => None
}
}
}