src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Sun Oct 05 17:58:36 2014 +0200 (2014-10-05)
changeset 58545 30b75b7958d6
parent 57878 51a2f9140175
child 59080 611914621edb
permissions -rw-r--r--
citation tooltip/hyperlink based on open buffers with .bib 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, Buffer}
    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   // owned by GUI thread
    26   private var removed_nodes = Set.empty[Document.Node.Name]
    27 
    28   def remove_node(name: Document.Node.Name): Unit =
    29     GUI_Thread.require { removed_nodes += name }
    30 
    31   override def flush()
    32   {
    33     GUI_Thread.require {}
    34 
    35     val doc_blobs = PIDE.document_blobs()
    36     val models = PIDE.document_models()
    37 
    38     val removed = removed_nodes; removed_nodes = Set.empty
    39     val removed_perspective =
    40       (removed -- models.iterator.map(_.node_name)).toList.map(
    41         name => (name, Document.Node.no_perspective_text))
    42 
    43     val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
    44     if (!edits.isEmpty) session.update(doc_blobs, edits)
    45   }
    46 
    47   private val delay_flush =
    48     GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    49 
    50   def invoke(): Unit = delay_flush.invoke()
    51 
    52 
    53   /* current situation */
    54 
    55   override def current_context: View =
    56     GUI_Thread.require { jEdit.getActiveView() }
    57 
    58   override def current_node(view: View): Option[Document.Node.Name] =
    59     GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    60 
    61   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    62     GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    63 
    64   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    65   {
    66     GUI_Thread.require {}
    67 
    68     JEdit_Lib.jedit_buffer(name) match {
    69       case Some(buffer) =>
    70         PIDE.document_model(buffer) match {
    71           case Some(model) => model.snapshot
    72           case None => session.snapshot(name)
    73         }
    74       case None => session.snapshot(name)
    75     }
    76   }
    77 
    78   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    79   {
    80     GUI_Thread.require {}
    81 
    82     val text_area = view.getTextArea
    83     val buffer = view.getBuffer
    84 
    85     PIDE.document_view(text_area) match {
    86       case Some(doc_view) if doc_view.model.is_theory =>
    87         val node = snapshot.version.nodes(doc_view.model.node_name)
    88         val caret = snapshot.revert(text_area.getCaretPosition)
    89         if (caret < buffer.getLength) {
    90           val caret_command_iterator = node.command_iterator(caret)
    91           if (caret_command_iterator.hasNext) {
    92             val (cmd0, _) = caret_command_iterator.next
    93             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    94           }
    95           else None
    96         }
    97         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    98       case _ =>
    99         PIDE.document_model(buffer) match {
   100           case Some(model) if !model.is_theory =>
   101             snapshot.version.nodes.load_commands(model.node_name) match {
   102               case cmd :: _ => Some(cmd)
   103               case Nil => None
   104             }
   105           case _ => None
   106         }
   107     }
   108   }
   109 
   110 
   111   /* overlays */
   112 
   113   private val overlays = Synchronized(Document.Overlays.empty)
   114 
   115   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
   116     overlays.value(name)
   117 
   118   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
   119     overlays.change(_.insert(command, fn, args))
   120 
   121   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
   122     overlays.change(_.remove(command, fn, args))
   123 
   124 
   125   /* navigation */
   126 
   127   def push_position(view: View)
   128   {
   129     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
   130     if (navigator != null) {
   131       try {
   132         val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
   133         m.invoke(null, view)
   134       }
   135       catch { case _: NoSuchMethodException => }
   136     }
   137   }
   138 
   139   def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
   140   {
   141     GUI_Thread.require {}
   142 
   143     push_position(view)
   144 
   145     view.goToBuffer(buffer)
   146     try { view.getTextArea.moveCaretPosition(offset) }
   147     catch {
   148       case _: ArrayIndexOutOfBoundsException =>
   149       case _: IllegalArgumentException =>
   150     }
   151   }
   152 
   153   def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   154   {
   155     GUI_Thread.require {}
   156 
   157     push_position(view)
   158 
   159     JEdit_Lib.jedit_buffer(name) match {
   160       case Some(buffer) =>
   161         view.goToBuffer(buffer)
   162         val text_area = view.getTextArea
   163 
   164         try {
   165           val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
   166           text_area.moveCaretPosition(line_start)
   167           if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
   168         }
   169         catch {
   170           case _: ArrayIndexOutOfBoundsException =>
   171           case _: IllegalArgumentException =>
   172         }
   173 
   174       case None if (new JFile(name)).isDirectory =>
   175         VFSBrowser.browseDirectory(view, name)
   176 
   177       case None =>
   178         val args =
   179           if (line <= 0) Array(name)
   180           else if (column <= 0) Array(name, "+line:" + line.toInt)
   181           else Array(name, "+line:" + line.toInt + "," + column.toInt)
   182         jEdit.openFiles(view, null, args)
   183     }
   184   }
   185 
   186 
   187   /* hyperlinks */
   188 
   189   def hyperlink_url(name: String): Hyperlink =
   190     new Hyperlink {
   191       val external = true
   192       def follow(view: View): Unit =
   193         Future.fork {
   194           try { Isabelle_System.open(name) }
   195           catch {
   196             case exn: Throwable =>
   197               GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
   198           }
   199         }
   200       override def toString: String = "URL " + quote(name)
   201     }
   202 
   203   def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
   204     new Hyperlink {
   205       val external = false
   206       def follow(view: View): Unit = goto_buffer(view, buffer, offset)
   207       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
   208     }
   209 
   210   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
   211     new Hyperlink {
   212       val external = false
   213       def follow(view: View): Unit = goto_file(view, name, line, column)
   214       override def toString: String = "file " + quote(name)
   215     }
   216 
   217   def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
   218     : Option[Hyperlink] =
   219   {
   220     val opt_name =
   221       if (Path.is_wellformed(source_name)) {
   222         if (Path.is_valid(source_name)) {
   223           val path = Path.explode(source_name)
   224           Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
   225         }
   226         else None
   227       }
   228       else Some(source_name)
   229 
   230     opt_name match {
   231       case Some(name) =>
   232         JEdit_Lib.jedit_buffer(name) match {
   233           case Some(buffer) if offset > 0 =>
   234             val (line, column) =
   235               JEdit_Lib.buffer_lock(buffer) {
   236                 ((1, 1) /:
   237                   (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
   238                     zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
   239                       Symbol.advance_line_column)
   240               }
   241             Some(hyperlink_file(name, line, column))
   242           case _ => Some(hyperlink_file(name, line))
   243         }
   244       case None => None
   245     }
   246   }
   247 
   248   override def hyperlink_command(
   249     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
   250   {
   251     if (snapshot.is_outdated) None
   252     else {
   253       snapshot.state.find_command(snapshot.version, command.id) match {
   254         case None => None
   255         case Some((node, _)) =>
   256           val file_name = command.node_name.node
   257           val sources_iterator =
   258             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   259               (if (offset == 0) Iterator.empty
   260                else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
   261           val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
   262           Some(hyperlink_file(file_name, line, column))
   263       }
   264     }
   265   }
   266 
   267   def hyperlink_command_id(
   268     snapshot: Document.Snapshot,
   269     id: Document_ID.Generic,
   270     offset: Symbol.Offset = 0): Option[Hyperlink] =
   271   {
   272     snapshot.state.find_command(snapshot.version, id) match {
   273       case Some((node, command)) => hyperlink_command(snapshot, command, offset)
   274       case None => None
   275     }
   276   }
   277 }