src/Tools/jEdit/src/jedit_editor.scala
author wenzelm
Tue Jan 05 15:40:25 2016 +0100 (2016-01-05)
changeset 62062 ee610059b0e9
parent 61728 5f5ff1eab407
child 62248 dca0bac351b2
permissions -rw-r--r--
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
     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(hidden: Boolean = false)
    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(hidden, doc_blobs)) ::: removed_perspective
    44     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   def stable_tip_version(): Option[Document.Version] =
    53     GUI_Thread.require {
    54       if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable))
    55         session.current_state().stable_tip_version
    56       else None
    57     }
    58 
    59 
    60   /* current situation */
    61 
    62   override def current_context: View =
    63     GUI_Thread.require { jEdit.getActiveView() }
    64 
    65   override def current_node(view: View): Option[Document.Node.Name] =
    66     GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) }
    67 
    68   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
    69     GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    70 
    71   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    72   {
    73     GUI_Thread.require {}
    74 
    75     JEdit_Lib.jedit_buffer(name) match {
    76       case Some(buffer) =>
    77         PIDE.document_model(buffer) match {
    78           case Some(model) => model.snapshot
    79           case None => session.snapshot(name)
    80         }
    81       case None => session.snapshot(name)
    82     }
    83   }
    84 
    85   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    86   {
    87     GUI_Thread.require {}
    88 
    89     val text_area = view.getTextArea
    90     val buffer = view.getBuffer
    91 
    92     PIDE.document_view(text_area) match {
    93       case Some(doc_view) if doc_view.model.is_theory =>
    94         val node = snapshot.version.nodes(doc_view.model.node_name)
    95         val caret = snapshot.revert(text_area.getCaretPosition)
    96         if (caret < buffer.getLength) {
    97           val caret_command_iterator = node.command_iterator(caret)
    98           if (caret_command_iterator.hasNext) {
    99             val (cmd0, _) = caret_command_iterator.next
   100             node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
   101           }
   102           else None
   103         }
   104         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
   105       case _ =>
   106         PIDE.document_model(buffer) match {
   107           case Some(model) if !model.is_theory =>
   108             snapshot.version.nodes.load_commands(model.node_name) match {
   109               case cmd :: _ => Some(cmd)
   110               case Nil => None
   111             }
   112           case _ => None
   113         }
   114     }
   115   }
   116 
   117 
   118   /* overlays */
   119 
   120   private val overlays = Synchronized(Document.Overlays.empty)
   121 
   122   override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
   123     overlays.value(name)
   124 
   125   override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
   126     overlays.change(_.insert(command, fn, args))
   127 
   128   override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
   129     overlays.change(_.remove(command, fn, args))
   130 
   131 
   132   /* navigation */
   133 
   134   def push_position(view: View)
   135   {
   136     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
   137     if (navigator != null) {
   138       try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
   139       catch { case _: NoSuchMethodException => }
   140     }
   141   }
   142 
   143   def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset)
   144   {
   145     GUI_Thread.require {}
   146 
   147     push_position(view)
   148 
   149     if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
   150     try { view.getTextArea.moveCaretPosition(offset) }
   151     catch {
   152       case _: ArrayIndexOutOfBoundsException =>
   153       case _: IllegalArgumentException =>
   154     }
   155   }
   156 
   157   def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0)
   158   {
   159     GUI_Thread.require {}
   160 
   161     push_position(view)
   162 
   163     JEdit_Lib.jedit_buffer(name) match {
   164       case Some(buffer) =>
   165         if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
   166         val text_area = view.getTextArea
   167 
   168         try {
   169           val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
   170           text_area.moveCaretPosition(line_start)
   171           if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
   172         }
   173         catch {
   174           case _: ArrayIndexOutOfBoundsException =>
   175           case _: IllegalArgumentException =>
   176         }
   177 
   178       case None if (new JFile(name)).isDirectory =>
   179         VFSBrowser.browseDirectory(view, name)
   180 
   181       case None =>
   182         val args =
   183           if (line <= 0) Array(name)
   184           else if (column <= 0) Array(name, "+line:" + line.toInt)
   185           else Array(name, "+line:" + line.toInt + "," + column.toInt)
   186         jEdit.openFiles(view, null, args)
   187     }
   188   }
   189 
   190   def goto_doc(view: View, path: Path)
   191   {
   192     if (path.is_file)
   193       goto_file(true, view, File.platform_path(path))
   194     else {
   195       Standard_Thread.fork("documentation") {
   196         try { Doc.view(path) }
   197         catch {
   198           case exn: Throwable =>
   199             GUI_Thread.later {
   200               GUI.error_dialog(view,
   201                 "Documentation error", GUI.scrollable_text(Exn.message(exn)))
   202             }
   203         }
   204       }
   205     }
   206   }
   207 
   208 
   209   /* hyperlinks */
   210 
   211   def hyperlink_doc(name: String): Option[Hyperlink] =
   212     Doc.contents().collectFirst({
   213       case doc: Doc.Text_File if doc.name == name => doc.path
   214       case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
   215         new Hyperlink {
   216           val external = !path.is_file
   217           def follow(view: View): Unit = goto_doc(view, path)
   218           override def toString: String = "doc " + quote(name)
   219         })
   220 
   221   def hyperlink_url(name: String): Hyperlink =
   222     new Hyperlink {
   223       val external = true
   224       def follow(view: View): Unit =
   225         Standard_Thread.fork("hyperlink_url") {
   226           try { Isabelle_System.open(name) }
   227           catch {
   228             case exn: Throwable =>
   229               GUI_Thread.later {
   230                 GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
   231               }
   232           }
   233         }
   234       override def toString: String = "URL " + quote(name)
   235     }
   236 
   237   def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink =
   238     new Hyperlink {
   239       val external = false
   240       def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset)
   241       override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
   242     }
   243 
   244   def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink =
   245     new Hyperlink {
   246       val external = false
   247       def follow(view: View): Unit = goto_file(focus, view, name, line, column)
   248       override def toString: String = "file " + quote(name)
   249     }
   250 
   251   def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset)
   252     : Option[Hyperlink] =
   253   {
   254     val opt_name =
   255       if (Path.is_wellformed(source_name)) {
   256         if (Path.is_valid(source_name)) {
   257           val path = Path.explode(source_name)
   258           Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path))
   259         }
   260         else None
   261       }
   262       else Some(source_name)
   263 
   264     opt_name match {
   265       case Some(name) =>
   266         JEdit_Lib.jedit_buffer(name) match {
   267           case Some(buffer) if offset > 0 =>
   268             val (line, column) =
   269               JEdit_Lib.buffer_lock(buffer) {
   270                 ((1, 1) /:
   271                   (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
   272                     zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
   273                       Symbol.advance_line_column)
   274               }
   275             Some(hyperlink_file(focus, name, line, column))
   276           case _ => Some(hyperlink_file(focus, name, line))
   277         }
   278       case None => None
   279     }
   280   }
   281 
   282   override def hyperlink_command(
   283     focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0)
   284       : Option[Hyperlink] =
   285   {
   286     if (snapshot.is_outdated) None
   287     else {
   288       snapshot.state.find_command(snapshot.version, command.id) match {
   289         case None => None
   290         case Some((node, _)) =>
   291           val file_name = command.node_name.node
   292           val sources_iterator =
   293             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   294               (if (offset == 0) Iterator.empty
   295                else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
   296           val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
   297           Some(hyperlink_file(focus, file_name, line, column))
   298       }
   299     }
   300   }
   301 
   302   def hyperlink_command_id(
   303     focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
   304       : Option[Hyperlink] =
   305   {
   306     snapshot.state.find_command(snapshot.version, id) match {
   307       case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset)
   308       case None => None
   309     }
   310   }
   311 
   312   def is_hyperlink_position(snapshot: Document.Snapshot,
   313     text_offset: Text.Offset, pos: Position.T): Boolean =
   314   {
   315     pos match {
   316       case Position.Id_Offset0(id, offset) if offset > 0 =>
   317         snapshot.state.find_command(snapshot.version, id) match {
   318           case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
   319             node.command_start(command) match {
   320               case Some(start) => text_offset == start + command.chunk.decode(offset)
   321               case None => false
   322             }
   323           case _ => false
   324         }
   325       case _ => false
   326     }
   327   }
   328 
   329   def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
   330       : Option[Hyperlink] =
   331     pos match {
   332       case Position.Line_File(line, name) =>
   333         val offset = Position.Offset.unapply(pos) getOrElse 0
   334         hyperlink_source_file(focus, name, line, offset)
   335       case Position.Id_Offset0(id, offset) =>
   336         hyperlink_command_id(focus, snapshot, id, offset)
   337       case _ => None
   338     }
   339 
   340   def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
   341       : Option[Hyperlink] =
   342     pos match {
   343       case Position.Def_Line_File(line, name) =>
   344         val offset = Position.Def_Offset.unapply(pos) getOrElse 0
   345         hyperlink_source_file(focus, name, line, offset)
   346       case Position.Def_Id_Offset0(id, offset) =>
   347         hyperlink_command_id(focus, snapshot, id, offset)
   348       case _ => None
   349     }
   350 }