src/Tools/jEdit/src/jedit_editor.scala

 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.browser.VFSBrowser
 import org.gjt.sp.jedit.io.{VFSManager, VFSFile}
 
 
-class JEdit_Editor extends Editor[View]
-{
+class JEdit_Editor extends Editor[View] {
   /* session */
 
   override def session: Session = PIDE.session
 
   def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit =

     GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
 
   override def current_node_snapshot(view: View): Option[Document.Snapshot] =
     GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) }
 
-  override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
-  {
+  override def node_snapshot(name: Document.Node.Name): Document.Snapshot = {
     GUI_Thread.require {}
     Document_Model.get(name) match {
       case Some(model) => model.snapshot()
       case None => session.snapshot(name)
     }
   }
 
-  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
-  {
+  override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = {
     GUI_Thread.require {}
 
     val text_area = view.getTextArea
     val buffer = view.getBuffer
 

     Document_Model.remove_overlay(command, fn, args)
 
 
   /* navigation */
 
-  def push_position(view: View): Unit =
-  {
+  def push_position(view: View): Unit = {
     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
     if (navigator != null) {
       try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
       catch { case _: NoSuchMethodException => }
     }
   }
 
-  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit =
-  {
+  def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit = {
     GUI_Thread.require {}
 
     push_position(view)
 
     if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)

   }
 
   def goto_file(focus: Boolean, view: View, name: String): Unit =
     goto_file(focus, view, Line.Node_Position.offside(name))
 
-  def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit =
-  {
+  def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit = {
     GUI_Thread.require {}
 
     push_position(view)
 
     val name = pos.name

           jEdit.openFiles(view, null, args)
         }
     }
   }
 
-  def goto_doc(view: View, path: Path): Unit =
-  {
+  def goto_doc(view: View, path: Path): Unit = {
     if (path.is_pdf) Doc.view(path)
     else goto_file(true, view, File.platform_path(path))
   }
 
 

           def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset)
           override def toString: String = "buffer " + quote(model.node_name.node)
         }
     }
 
-  def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset)
-    : Option[Hyperlink] =
-  {
+  def hyperlink_source_file(
+    focus: Boolean,
+    source_name: String,
+    line1: Int,
+    offset: Symbol.Offset
+  ) : Option[Hyperlink] = {
     for (name <- PIDE.resources.source_file(source_name)) yield {
       def hyperlink(pos: Line.Position) =
         hyperlink_file(focus, Line.Node_Position(name, pos))
 
       if (offset > 0) {

       else hyperlink(Line.Position((line1 - 1) max 0))
     }
   }
 
   override def hyperlink_command(
-    focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
-      : Option[Hyperlink] =
-  {
+    focus: Boolean,
+    snapshot: Document.Snapshot,
+    id: Document_ID.Generic,
+    offset: Symbol.Offset = 0
+  ) : Option[Hyperlink] = {
     if (snapshot.is_outdated) None
     else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
   }
 
-  def is_hyperlink_position(snapshot: Document.Snapshot,
-    text_offset: Text.Offset, pos: Position.T): Boolean =
-  {
+  def is_hyperlink_position(
+    snapshot: Document.Snapshot,
+    text_offset: Text.Offset,
+    pos: Position.T
+  ): Boolean = {
     pos match {
       case Position.Item_Id(id, range) if range.start > 0 =>
         snapshot.find_command(id) match {
           case Some((node, command)) if snapshot.get_node(command.node_name) eq node =>
             node.command_start(command) match {