src/Tools/jEdit/src/rich_text_area.scala

 
   private val set_state = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
     {
       painter_rendering = get_rendering()
       painter_clip = gfx.getClip
       caret_focus =
         if (caret_enabled && !painter_rendering.snapshot.is_outdated) {

 
   private val reset_state = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
     {
       painter_rendering = null
       painter_clip = null
       caret_focus = Rendering.Focus.empty
     }
   }
 
-  def robust_rendering(body: JEdit_Rendering => Unit)
+  def robust_rendering(body: JEdit_Rendering => Unit): Unit =
   {
     robust_body(()) { body(painter_rendering) }
   }
 
 

 
     def is_active: Boolean = the_text_info.isDefined
     def text_info: Option[(String, Text.Info[A])] = the_text_info
     def info: Option[Text.Info[A]] = the_text_info.map(_._2)
 
-    def update(new_info: Option[Text.Info[A]])
+    def update(new_info: Option[Text.Info[A]]): Unit =
     {
       val old_text_info = the_text_info
       val new_text_info =
         new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
 

         } JEdit_Lib.invalidate_range(text_area, r2)
         the_text_info = new_text_info
       }
     }
 
-    def update_rendering(r: JEdit_Rendering, range: Text.Range)
-    { update(rendering(r)(range)) }
-
-    def reset { update(None) }
+    def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit =
+      update(rendering(r)(range))
+
+    def reset: Unit = update(None)
   }
 
   // owned by GUI thread
 
   private val highlight_area =

 
   private def area_active(): Boolean =
     active_areas.exists({ case (area, _) => area.is_active })
 
   private val focus_listener = new FocusAdapter {
-    override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
+    override def focusLost(e: FocusEvent): Unit = { robust_body(()) { active_reset() } }
   }
 
   private val window_listener = new WindowAdapter {
-    override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
-    override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
+    override def windowIconified(e: WindowEvent): Unit = { robust_body(()) { active_reset() } }
+    override def windowDeactivated(e: WindowEvent): Unit = { robust_body(()) { active_reset() } }
   }
 
   private val mouse_listener = new MouseAdapter {
-    override def mouseClicked(e: MouseEvent) {
+    override def mouseClicked(e: MouseEvent): Unit =
+    {
       robust_body(()) {
         hyperlink_area.info match {
           case Some(Text.Info(range, link)) =>
             if (!link.external) {
               try { text_area.moveCaretPosition(range.start) }

         SwingUtilities.convertPointFromScreen(point, painter)
         painter.contains(point)
     }
 
   private val mouse_motion_listener = new MouseMotionAdapter {
-    override def mouseDragged(evt: MouseEvent) {
+    override def mouseDragged(evt: MouseEvent): Unit =
+    {
       robust_body(()) {
         active_reset()
         Completion_Popup.Text_Area.dismissed(text_area)
         Pretty_Tooltip.dismiss_descendant(text_area.getPainter)
       }
     }
 
-    override def mouseMoved(evt: MouseEvent) {
+    override def mouseMoved(evt: MouseEvent): Unit =
+    {
       robust_body(()) {
         val x = evt.getX
         val y = evt.getY
         val control = JEdit_Lib.command_modifier(evt)
 

 
   private val background_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
     {
       robust_rendering { rendering =>
         val fm = text_area.getPainter.getFontMetrics
 
         for (i <- physical_lines.indices) {

 
   private val text_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
     {
       robust_rendering { rendering =>
         val painter = text_area.getPainter
         val fm = painter.getFontMetrics
         val lm = painter.getFont.getLineMetrics(" ", painter.getFontRenderContext)

 
   private val foreground_painter = new TextAreaExtension
   {
     override def paintScreenLineRange(gfx: Graphics2D,
       first_line: Int, last_line: Int, physical_lines: Array[Int],
-      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int): Unit =
     {
       robust_rendering { rendering =>
         val search_pattern = get_search_pattern()
         for (i <- physical_lines.indices) {
           if (physical_lines(i) != -1) {

   /* caret -- outside of text range */
 
   private class Caret_Painter(before: Boolean) extends TextAreaExtension
   {
     override def paintValidLine(gfx: Graphics2D,
-      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int): Unit =
     {
       robust_rendering { _ =>
         if (before) gfx.clipRect(0, 0, 0, 0)
         else gfx.setClip(painter_clip)
       }

   private val after_caret_painter2 = new Caret_Painter(false)
 
   private val caret_painter = new TextAreaExtension
   {
     override def paintValidLine(gfx: Graphics2D,
-      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int): Unit =
     {
       robust_rendering { rendering =>
         if (caret_visible) {
           val caret = text_area.getCaretPosition
           if (caret_enabled && start <= caret && caret == end - 1) {

   }
 
 
   /* activation */
 
-  def activate()
+  def activate(): Unit =
   {
     val painter = text_area.getPainter
     painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
     painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)

     text_area.addKeyListener(key_listener)
     text_area.addFocusListener(focus_listener)
     view.addWindowListener(window_listener)
   }
 
-  def deactivate()
+  def deactivate(): Unit =
   {
     active_reset()
     val painter = text_area.getPainter
     view.removeWindowListener(window_listener)
     text_area.removeFocusListener(focus_listener)