src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Tue Feb 11 21:58:31 2014 +0100 (2014-02-11)
changeset 55432 9c53198dbb1c
parent 54706 d3c656f0b7ab
child 55781 b3a4207fb9a6
permissions -rw-r--r--
maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;
     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 java.io.{File => JFile}
    14 
    15 import org.gjt.sp.jedit.{jEdit, View}
    16 import org.gjt.sp.jedit.browser.VFSBrowser
    17 
    18 
    19 class JEdit_Editor extends Editor[View]
    20 {
    21   /* session */
    22 
    23   override def session: Session = PIDE.session
    24 
    25   override def flush()
    26   {
    27     Swing_Thread.require()
    28 
    29     val edits = PIDE.document_models().flatMap(_.flushed_edits())
    30     if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
    31   }
    32 
    33   private val delay_flush =
    34     Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    35 
    36   def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
    37 
    38 
    39   /* current situation */
    40 
    41   override def current_context: View =
    42     Swing_Thread.require { jEdit.getActiveView() }
    43 
    44   override def current_node(view: View): Option[Document.Node.Name] =
    45     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    46 
    47   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    48     Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    49 
    50   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    51   {
    52     Swing_Thread.require()
    53 
    54     JEdit_Lib.jedit_buffer(name.node) match {
    55       case Some(buffer) =>
    56         PIDE.document_model(buffer) match {
    57           case Some(model) => model.snapshot
    58           case None => session.snapshot(name)
    59         }
    60       case None => session.snapshot(name)
    61     }
    62   }
    63 
    64   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    65   {
    66     Swing_Thread.require()
    67 
    68     val text_area = view.getTextArea
    69     val buffer = view.getBuffer
    70 
    71     PIDE.document_view(text_area) match {
    72       case Some(doc_view) if doc_view.model.is_theory =>
    73         val node = snapshot.version.nodes(doc_view.model.node_name)
    74         val caret = snapshot.revert(text_area.getCaretPosition)
    75         if (caret < buffer.getLength) {
    76           val caret_commands = node.command_range(caret)
    77           if (caret_commands.hasNext) {
    78             val (cmd0, _) = caret_commands.next
    79             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    80           }
    81           else None
    82         }
    83         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    84       case _ =>
    85         PIDE.document_model(buffer) match {
    86           case Some(model) if !model.is_theory =>
    87             snapshot.version.nodes.thy_load_commands(model.node_name) match {
    88               case cmd :: _ => Some(cmd)
    89               case Nil => None
    90             }
    91           case _ => None
    92         }
    93     }
    94   }
    95 
    96 
    97   /* overlays */
    98 
    99   private var overlays = Document.Overlays.empty
   100 
   101   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
   102     synchronized { overlays(name) }
   103 
   104   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
   105     synchronized { overlays = overlays.insert(command, fn, args) }
   106 
   107   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
   108     synchronized { overlays = overlays.remove(command, fn, args) }
   109 
   110 
   111   /* hyperlinks */
   112 
   113   def goto(view: View, name: String, line: Int = 0, column: Int = 0)
   114   {
   115     Swing_Thread.require()
   116 
   117     JEdit_Lib.jedit_buffer(name) match {
   118       case Some(buffer) =>
   119         view.goToBuffer(buffer)
   120         val text_area = view.getTextArea
   121 
   122         try {
   123           val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
   124           text_area.moveCaretPosition(line_start)
   125           if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
   126         }
   127         catch {
   128           case _: ArrayIndexOutOfBoundsException =>
   129           case _: IllegalArgumentException =>
   130         }
   131 
   132       case None if (new JFile(name)).isDirectory =>
   133         VFSBrowser.browseDirectory(view, name)
   134 
   135       case None =>
   136         val args =
   137           if (line <= 0) Array(name)
   138           else if (column <= 0) Array(name, "+line:" + line.toInt)
   139           else Array(name, "+line:" + line.toInt + "," + column.toInt)
   140         jEdit.openFiles(view, null, args)
   141     }
   142   }
   143 
   144   override def hyperlink_url(name: String): Hyperlink =
   145     new Hyperlink {
   146       def follow(view: View) =
   147         default_thread_pool.submit(() =>
   148           try { Isabelle_System.open(name) }
   149           catch {
   150             case exn: Throwable =>
   151               GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
   152           })
   153     }
   154 
   155   override def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
   156     new Hyperlink { def follow(view: View) = goto(view, name, line, column) }
   157 
   158   override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0)
   159     : Option[Hyperlink] =
   160   {
   161     if (snapshot.is_outdated) None
   162     else {
   163       snapshot.state.find_command(snapshot.version, command.id) match {
   164         case None => None
   165         case Some((node, _)) =>
   166           val file_name = command.node_name.node
   167           val sources =
   168             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   169               (if (offset == 0) Iterator.empty
   170                else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
   171           val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   172           Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } })
   173       }
   174     }
   175   }
   176 }