src/Tools/jEdit/src/active.scala

--- a/src/Tools/jEdit/src/active.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Tools/jEdit/src/active.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -11,10 +11,8 @@
 import org.gjt.sp.jedit.{ServiceManager, View}
 
 
-object Active
-{
-  abstract class Handler
-  {
+object Active {
+  abstract class Handler {
     def handle(
       view: View, text: String, elem: XML.Elem,
       doc_view: Document_View, snapshot: Document.Snapshot): Boolean
@@ -24,8 +22,7 @@
     ServiceManager.getServiceNames(classOf[Handler]).toList
       .map(ServiceManager.getService(classOf[Handler], _))
 
-  def action(view: View, text: String, elem: XML.Elem): Unit =
-  {
+  def action(view: View, text: String, elem: XML.Elem): Unit = {
     GUI_Thread.require {}
 
     Document_View.get(view.getTextArea) match {
@@ -40,12 +37,11 @@
     }
   }
 
-  class Misc_Handler extends Active.Handler
-  {
+  class Misc_Handler extends Active.Handler {
     override def handle(
       view: View, text: String, elem: XML.Elem,
-      doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
-    {
+      doc_view: Document_View, snapshot: Document.Snapshot
+    ): Boolean = {
       val text_area = doc_view.text_area
       val model = doc_view.model
       val buffer = model.buffer