src/Tools/jEdit/src/query_dockable.scala

 import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
 
 import org.gjt.sp.jedit.View
 
 
-object Query_Dockable
-{
-  private abstract class Operation(view: View)
-  {
+object Query_Dockable {
+  private abstract class Operation(view: View) {
     val pretty_text_area = new Pretty_Text_Area(view)
     def query_operation: Query_Operation[View]
     def query: JComponent
     def select: Unit
     def page: TabbedPane.Page
   }
 }
 
-class Query_Dockable(view: View, position: String) extends Dockable(view, position)
-{
+class Query_Dockable(view: View, position: String) extends Dockable(view, position) {
   /* common GUI components */
 
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
-  private def make_query(property: String, tooltip: String, apply_query: () => Unit)
-      : Completion_Popup.History_Text_Field =
-    new Completion_Popup.History_Text_Field(property)
-    {
-      override def processKeyEvent(evt: KeyEvent): Unit =
-      {
+  private def make_query(
+    property: String,
+    tooltip: String,
+    apply_query: () => Unit
+  ): Completion_Popup.History_Text_Field = {
+    new Completion_Popup.History_Text_Field(property) {
+      override def processKeyEvent(evt: KeyEvent): Unit = {
         if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
         super.processKeyEvent(evt)
       }
       { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
       setColumns(40)
       setToolTipText(tooltip)
       setFont(GUI.imitate_font(getFont, scale = 1.2))
     }
+  }
 
 
   /* consume status */
 
   def consume_status(
-    process_indicator: Process_Indicator, status: Query_Operation.Status.Value): Unit =
-  {
+    process_indicator: Process_Indicator,
+    status: Query_Operation.Status.Value
+  ): Unit = {
     status match {
       case Query_Operation.Status.WAITING =>
         process_indicator.update("Waiting for evaluation of context ...", 5)
       case Query_Operation.Status.RUNNING =>
         process_indicator.update("Running find operation ...", 15)

   }
 
 
   /* find theorems */
 
-  private val find_theorems = new Query_Dockable.Operation(view)
-  {
+  private val find_theorems = new Query_Dockable.Operation(view) {
     /* query */
 
     private val process_indicator = new Process_Indicator
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_theorems",
         consume_status(process_indicator, _),
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
-    private def apply_query(): Unit =
-    {
+    private def apply_query(): Unit = {
       query.addCurrentToHistory()
       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
     }
 
     private val query_label = new Label("Find:") {

   }
 
 
   /* find consts */
 
-  private val find_consts = new Query_Dockable.Operation(view)
-  {
+  private val find_consts = new Query_Dockable.Operation(view) {
     /* query */
 
     private val process_indicator = new Process_Indicator
 
     val query_operation =
       new Query_Operation(PIDE.editor, view, "find_consts",
         consume_status(process_indicator, _),
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
-    private def apply_query(): Unit =
-    {
+    private def apply_query(): Unit = {
       query.addCurrentToHistory()
       query_operation.apply_query(List(query.getText))
     }
 
     private val query_label = new Label("Find:") {

   }
 
 
   /* print operation */
 
-  private val print_operation = new Query_Dockable.Operation(view)
-  {
+  private val print_operation = new Query_Dockable.Operation(view) {
     /* items */
 
-    private class Item(val name: String, description: String, sel: Boolean)
-    {
+    private class Item(val name: String, description: String, sel: Boolean) {
       val checkbox = new CheckBox(name) {
         tooltip = "Print " + description
         selected = sel
         reactions += { case ButtonClicked(_) => apply_query() }
       }

     private var _items: List[Item] = Nil
 
     private def selected_items(): List[String] =
       for (item <- _items if item.checkbox.selected) yield item.name
 
-    private def update_items(): List[Item] =
-    {
+    private def update_items(): List[Item] = {
       val old_items = _items
       def was_selected(name: String): Boolean =
         old_items.find(item => item.name == name) match {
           case None => false
           case Some(item) => item.checkbox.selected

       }
     }
 
     private val control_panel = Wrap_Panel()
 
-    def select: Unit =
-    {
+    def select: Unit = {
       control_panel.contents.clear()
       control_panel.contents += query_label
       update_items().foreach(item => control_panel.contents += item.checkbox)
       control_panel.contents ++=
         List(process_indicator.component, apply_button,

 
   /* operations */
 
   private val operations = List(find_theorems, find_consts, print_operation)
 
-  private val operations_pane = new TabbedPane
-  {
+  private val operations_pane = new TabbedPane {
     pages ++= operations.map(_.page)
     listenTo(selection)
     reactions += { case SelectionChanged(_) => select_operation() }
   }
 
   private def get_operation(): Option[Query_Dockable.Operation] =
     try { Some(operations(operations_pane.selection.index)) }
     catch { case _: IndexOutOfBoundsException => None }
 
-  private def select_operation(): Unit =
-  {
+  private def select_operation(): Unit = {
     for (op <- get_operation()) { op.select; op.query.requestFocus() }
     operations_pane.revalidate()
   }
 
-  override def focusOnDefaultComponent(): Unit =
-  {
+  override def focusOnDefaultComponent(): Unit = {
     for (op <- get_operation()) op.query.requestFocus()
   }
 
   select_operation()
   set_content(operations_pane)

   private val main =
     Session.Consumer[Session.Global_Options](getClass.getName) {
       case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
     }
 
-  override def init(): Unit =
-  {
+  override def init(): Unit = {
     PIDE.session.global_options += main
     handle_resize()
     operations.foreach(op => op.query_operation.activate())
   }
 
-  override def exit(): Unit =
-  {
+  override def exit(): Unit = {
     operations.foreach(op => op.query_operation.deactivate())
     PIDE.session.global_options -= main
     delay_resize.revoke()
   }
 }