src/Tools/jEdit/src/simplifier_trace_window.scala

 import javax.swing.SwingUtilities
 
 import org.gjt.sp.jedit.View
 
 
-private object Simplifier_Trace_Window
-{
-  sealed trait Trace_Tree
-  {
+private object Simplifier_Trace_Window {
+  sealed trait Trace_Tree {
     // FIXME replace with immutable tree builder
     var children: SortedMap[Long, Either[Simplifier_Trace.Item.Data, Elem_Tree]] = SortedMap.empty
     val serial: Long
     val parent: Option[Trace_Tree]
     val markup: String

     def tree_children: List[Elem_Tree] = children.values.toList.collect {
       case Right(tree) => tree
     }
   }
 
-  final class Root_Tree(val serial: Long) extends Trace_Tree
-  {
+  final class Root_Tree(val serial: Long) extends Trace_Tree {
     val parent = None
     val interesting = true
     val markup = ""
 
     def format: XML.Body =
       Pretty.separate(tree_children.flatMap(_.format))
   }
 
   final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
-    extends Trace_Tree
-  {
+  extends Trace_Tree {
     val serial = data.serial
     val markup = data.markup
 
     lazy val interesting: Boolean =
       data.markup == Markup.SIMP_TRACE_STEP ||

       tree_children.exists(_.interesting)
 
     private def body_contains(regex: Regex, body: XML.Body): Boolean =
       body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
 
-    def format: Option[XML.Tree] =
-    {
+    def format: Option[XML.Tree] = {
       def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
         Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content))
 
       lazy val bodies: XML.Body =
         children.values.toList.collect {

       case Nil =>
         ()
       case head :: tail =>
         lookup.get(head.parent) match {
           case Some(parent) =>
-            if (head.markup == Markup.SIMP_TRACE_HINT)
-            {
+            if (head.markup == Markup.SIMP_TRACE_HINT) {
               head.props match {
                 case Simplifier_Trace.Success(x)
                   if x ||
                      parent.markup == Markup.SIMP_TRACE_LOG ||
                      parent.markup == Markup.SIMP_TRACE_STEP =>

                 case _ =>
                   // ignore
               }
               walk_trace(tail, lookup)
             }
-            else if (head.markup == Markup.SIMP_TRACE_IGNORE)
-            {
+            else if (head.markup == Markup.SIMP_TRACE_IGNORE) {
               parent.parent match {
                 case None =>
                   Output.error_message(
                     "Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
                 case Some(tree) =>
                   tree.children -= head.parent
                   walk_trace(tail, lookup)
               }
             }
-            else
-            {
+            else {
               val entry = new Elem_Tree(head, Some(parent))
               parent.children += ((head.serial, Right(entry)))
               walk_trace(tail, lookup + (head.serial -> entry))
             }
 

 
 }
 
 
 class Simplifier_Trace_Window(
-  view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
-{
+  view: View,
+  snapshot: Document.Snapshot,
+  trace: Simplifier_Trace.Trace
+) extends Frame {
   GUI_Thread.require {}
 
   private val pretty_text_area = new Pretty_Text_Area(view)
   private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
 

 
   do_update()
   open()
   do_paint()
 
-  def do_update(): Unit =
-  {
+  def do_update(): Unit = {
     val xml = tree.format
     pretty_text_area.update(snapshot, Command.Results.empty, xml)
   }
 
-  def do_paint(): Unit =
-  {
+  def do_paint(): Unit = {
     GUI_Thread.later {
       pretty_text_area.resize(
         Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
     }
   }