src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Mon Apr 07 23:02:29 2014 +0200 (2014-04-07)
changeset 56458 a8d960baa5c2
parent 56457 eea4bbe15745
child 56461 ae33d153f6cc
permissions -rw-r--r--
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
     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 doc_blobs = PIDE.document_blobs()
    30     val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
    31     if (!edits.isEmpty) session.update(doc_blobs, edits)
    32   }
    33 
    34   private val delay_flush =
    35     Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    36 
    37   def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
    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) 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): Option[Command] =
    66   {
    67     Swing_Thread.require()
    68 
    69     val text_area = view.getTextArea
    70     val buffer = view.getBuffer
    71 
    72     PIDE.document_view(text_area) match {
    73       case Some(doc_view) if doc_view.model.is_theory =>
    74         val node = snapshot.version.nodes(doc_view.model.node_name)
    75         val caret = snapshot.revert(text_area.getCaretPosition)
    76         if (caret < buffer.getLength) {
    77           val caret_command_iterator = node.command_iterator(caret)
    78           if (caret_command_iterator.hasNext) {
    79             val (cmd0, _) = caret_command_iterator.next
    80             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
    81           }
    82           else None
    83         }
    84         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    85       case _ =>
    86         PIDE.document_model(buffer) match {
    87           case Some(model) if !model.is_theory =>
    88             snapshot.version.nodes.load_commands(model.node_name) match {
    89               case cmd :: _ => Some(cmd)
    90               case Nil => None
    91             }
    92           case _ => None
    93         }
    94     }
    95   }
    96 
    97 
    98   /* overlays */
    99 
   100   private var overlays = Document.Overlays.empty
   101 
   102   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
   103     synchronized { overlays(name) }
   104 
   105   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
   106     synchronized { overlays = overlays.insert(command, fn, args) }
   107 
   108   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
   109     synchronized { overlays = overlays.remove(command, fn, args) }
   110 
   111 
   112   /* navigation */
   113 
   114   def push_position(view: View)
   115   {
   116     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
   117     if (navigator != null) {
   118       try {
   119         val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
   120         m.invoke(null, view)
   121       }
   122       catch { case _: NoSuchMethodException => }
   123     }
   124   }
   125 
   126   def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   127   {
   128     Swing_Thread.require()
   129 
   130     push_position(view)
   131 
   132     JEdit_Lib.jedit_buffer(name) match {
   133       case Some(buffer) =>
   134         view.goToBuffer(buffer)
   135         val text_area = view.getTextArea
   136 
   137         try {
   138           val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
   139           text_area.moveCaretPosition(line_start)
   140           if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
   141         }
   142         catch {
   143           case _: ArrayIndexOutOfBoundsException =>
   144           case _: IllegalArgumentException =>
   145         }
   146 
   147       case None if (new JFile(name)).isDirectory =>
   148         VFSBrowser.browseDirectory(view, name)
   149 
   150       case None =>
   151         val args =
   152           if (line <= 0) Array(name)
   153           else if (column <= 0) Array(name, "+line:" + line.toInt)
   154           else Array(name, "+line:" + line.toInt + "," + column.toInt)
   155         jEdit.openFiles(view, null, args)
   156     }
   157   }
   158 
   159 
   160   /* hyperlinks */
   161 
   162   override def hyperlink_command(
   163     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
   164   {
   165     if (snapshot.is_outdated) None
   166     else {
   167       snapshot.state.find_command(snapshot.version, command.id) match {
   168         case None => None
   169         case Some((node, _)) =>
   170           val file_name = command.node_name.node
   171           val sources_iterator =
   172             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   173               (if (offset == 0) Iterator.empty
   174                else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
   175           val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
   176           Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
   177       }
   178     }
   179   }
   180 
   181   def hyperlink_command_id(
   182     snapshot: Document.Snapshot,
   183     id: Document_ID.Generic,
   184     offset: Symbol.Offset): Option[Hyperlink] =
   185   {
   186     snapshot.state.find_command(snapshot.version, id) match {
   187       case Some((node, command)) => hyperlink_command(snapshot, command, offset)
   188       case None => None
   189     }
   190   }
   191 
   192   def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
   193     new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
   194 
   195   def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
   196     : Option[Hyperlink] =
   197   {
   198     val opt_name =
   199       if (Path.is_wellformed(source_name)) {
   200         if (Path.is_valid(source_name)) {
   201           val path = Path.explode(source_name)
   202           Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
   203         }
   204         else None
   205       }
   206       else Some(source_name)
   207 
   208     opt_name match {
   209       case Some(name) =>
   210         JEdit_Lib.jedit_buffer(name) match {
   211           case Some(buffer) if offset > 0 =>
   212             val (line, column) =
   213               JEdit_Lib.buffer_lock(buffer) {
   214                 ((1, 1) /:
   215                   (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
   216                     zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
   217                       Symbol.advance_line_column)
   218               }
   219             Some(hyperlink_file(name, line, column))
   220           case _ => Some(hyperlink_file(name, line))
   221         }
   222       case None => None
   223     }
   224   }
   225 
   226   def hyperlink_url(name: String): Hyperlink =
   227     new Hyperlink {
   228       def follow(view: View) =
   229         default_thread_pool.submit(() =>
   230           try { Isabelle_System.open(name) }
   231           catch {
   232             case exn: Throwable =>
   233               GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
   234           })
   235     }
   236 }