src/Tools/jEdit/src/jedit_lib.scala

   def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
 
   def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A =
   {
     val undo_in_progress = buffer.isUndoInProgress
-    def set(b: Boolean) { Untyped.set[Boolean](buffer, "undoInProgress", b) }
+    def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
     try { set(true); body } finally { set(undo_in_progress) }
   }
 
 
   /* main jEdit components */

       Some(Text.Range(start, end))
     }
     else None
   }
 
-  def invalidate_range(text_area: TextArea, range: Text.Range)
+  def invalidate_range(text_area: TextArea, range: Text.Range): Unit =
   {
     val buffer = text_area.getBuffer
     buffer_range(buffer).try_restrict(range) match {
       case Some(range1) if !range1.is_singularity =>
         try {

         catch { case _: ArrayIndexOutOfBoundsException => }
       case _ =>
     }
   }
 
-  def invalidate(text_area: TextArea)
+  def invalidate(text_area: TextArea): Unit =
   {
     val visible_lines = text_area.getVisibleLines
     if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
   }
 

     }
 
 
   /* key event handling */
 
-  def request_focus_view(alt_view: View = null)
-  {
+  def request_focus_view(alt_view: View = null): Unit =
     isabelle.jedit_base.JEdit_Lib.request_focus_view(alt_view)
-  }
-
-  def propagate_key(view: View, evt: KeyEvent)
+
+  def propagate_key(view: View, evt: KeyEvent): Unit =
   {
     if (view != null && !evt.isConsumed)
       view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
   }
 
   def key_listener(
     key_typed: KeyEvent => Unit = _ => (),
     key_pressed: KeyEvent => Unit = _ => (),
     key_released: KeyEvent => Unit = _ => ()): KeyListener =
   {
-    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
+    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit =
     {
       val evt = KeyEventWorkaround.processKeyEvent(evt0)
       if (evt != null) handle(evt)
     }
 
     new KeyListener
     {
-      def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
-      def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
-      def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
+      def keyTyped(evt: KeyEvent): Unit = process_key_event(evt, key_typed)
+      def keyPressed(evt: KeyEvent): Unit = process_key_event(evt, key_pressed)
+      def keyReleased(evt: KeyEvent): Unit = process_key_event(evt, key_released)
     }
   }
 
   def special_key(evt: KeyEvent): Boolean =
   {