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