src/Tools/jEdit/src/debugger_dockable.scala

 import org.gjt.sp.jedit.{jEdit, View}
 import org.gjt.sp.jedit.menu.EnhancedMenuItem
 import org.gjt.sp.jedit.textarea.JEditTextArea
 
 
-object Debugger_Dockable
-{
+object Debugger_Dockable {
   /* breakpoints */
 
-  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] =
-  {
+  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] = {
     GUI_Thread.require {}
 
     Document_View.get(text_area) match {
       case Some(doc_view) =>
         val rendering = doc_view.get_rendering()

       List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
     }
     else Nil
 }
 
-class Debugger_Dockable(view: View, position: String) extends Dockable(view, position)
-{
+class Debugger_Dockable(view: View, position: String) extends Dockable(view, position) {
   GUI_Thread.require {}
 
   private val debugger = PIDE.session.debugger
 
 

 
   val pretty_text_area = new Pretty_Text_Area(view)
 
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
-  private def handle_resize(): Unit =
-  {
+  private def handle_resize(): Unit = {
     GUI_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   }
 
-  private def handle_update(): Unit =
-  {
+  private def handle_update(): Unit = {
     GUI_Thread.require {}
 
     val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
     val (new_threads, new_output) = debugger.status(tree_selection())
 

       case _ => None
     }
 
   def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
 
-  private def update_tree(threads: Debugger.Threads): Unit =
-  {
+  private def update_tree(threads: Debugger.Threads): Unit = {
     val thread_contexts =
       (for ((a, b) <- threads.iterator)
         yield Debugger.Context(a, b)).toList
 
     val new_tree_selection =

     }
 
     tree.revalidate()
   }
 
-  def update_vals(): Unit =
-  {
+  def update_vals(): Unit = {
     tree_selection() match {
       case Some(c) if c.stack_state.isDefined =>
         debugger.print_vals(c, sml_button.selected, context_field.getText)
       case Some(c) =>
         debugger.clear_output(c.thread_name)

     }
   }
 
   tree.addTreeSelectionListener(
     new TreeSelectionListener {
-      override def valueChanged(e: TreeSelectionEvent): Unit =
-      {
+      override def valueChanged(e: TreeSelectionEvent): Unit = {
         update_focus()
         update_vals()
       }
     })
   tree.addMouseListener(
     new MouseAdapter {
-      override def mouseClicked(e: MouseEvent): Unit =
-      {
+      override def mouseClicked(e: MouseEvent): Unit = {
         val click = tree.getPathForLocation(e.getX, e.getY)
         if (click != null && e.getClickCount == 1)
           update_focus()
       }
     })

 
   private val context_label = new Label("Context:") {
     tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
   }
   private val context_field =
-    new Completion_Popup.History_Text_Field("isabelle-debugger-context")
-    {
-      override def processKeyEvent(evt: KeyEvent): Unit =
-      {
+    new Completion_Popup.History_Text_Field("isabelle-debugger-context") {
+      override def processKeyEvent(evt: KeyEvent): Unit = {
         if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
           eval_expression()
         super.processKeyEvent(evt)
       }
       setColumns(20)

 
   private val expression_label = new Label("ML:") {
     tooltip = "Isabelle/ML or Standard ML expression"
   }
   private val expression_field =
-    new Completion_Popup.History_Text_Field("isabelle-debugger-expression")
-    {
-      override def processKeyEvent(evt: KeyEvent): Unit =
-      {
+    new Completion_Popup.History_Text_Field("isabelle-debugger-expression") {
+      override def processKeyEvent(evt: KeyEvent): Unit = {
         if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
           eval_expression()
         super.processKeyEvent(evt)
       }
       { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }

   private val eval_button = new Button("<html><b>Eval</b></html>") {
       tooltip = "Evaluate ML expression within optional context"
       reactions += { case ButtonClicked(_) => eval_expression() }
     }
 
-  private def eval_expression(): Unit =
-  {
+  private def eval_expression(): Unit = {
     context_field.addCurrentToHistory()
     expression_field.addCurrentToHistory()
     tree_selection() match {
       case Some(c) if c.debug_index.isDefined =>
         debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)

 
   addFocusListener(new FocusAdapter {
     override def focusGained(e: FocusEvent): Unit = update_focus()
   })
 
-  private def update_focus(): Unit =
-  {
+  private def update_focus(): Unit = {
     for (c <- tree_selection()) {
       debugger.set_focus(c)
       for {
         pos <- c.debug_position
         link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)

           break_button.selected = debugger.is_break()
           handle_update()
         }
     }
 
-  override def init(): Unit =
-  {
+  override def init(): Unit = {
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
     debugger.init()
     handle_update()
     jEdit.propertiesChanged()
   }
 
-  override def exit(): Unit =
-  {
+  override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.debugger_updates -= main
     delay_resize.revoke()
     debugger.exit()
     jEdit.propertiesChanged()