src/Tools/jEdit/src/jedit/TheoryView.scala

 
 
   private var col: Text.Changed = null
 
   private val col_timer = new Timer(300, new ActionListener() {
-    override def actionPerformed(e: ActionEvent) = commit()
+    override def actionPerformed(e: ActionEvent) = commit
   })
 
   col_timer.stop
   col_timer.setRepeats(true)
 

     val start = text_area.offsetToXY(begin)
     val stop =
       if (finish < buffer.getLength) text_area.offsetToXY(finish)
       else {
         val p = text_area.offsetToXY(finish - 1)
-        p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
+        val metrics = text_area.getPainter.getFontMetrics
+        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
         p
       }
 
     if (start != null && stop != null) {
       gfx.setColor(color)

   val changes = new EventBus[Text.Changed]
 
 
   /* BufferListener methods */
 
-  private def commit() {
+  private def commit {
     if (col != null)
       changes.event(col)
     col = null
     if (col_timer.isRunning())
       col_timer.stop()
   }
 
-  private def delay_commit() {
+  private def delay_commit {
     if (col_timer.isRunning())
       col_timer.restart()
     else
       col_timer.start()
   }

     if (col == null)
       col = new Text.Changed(offset, length, 0)
     else if (col.start <= offset && offset <= col.start + col.added)
       col = new Text.Changed(col.start, col.added + length, col.removed)
     else {
-      commit()
+      commit
       col = new Text.Changed(offset, length, 0)
     }
-    delay_commit()
+    delay_commit
   }
 
   override def preContentRemoved(buffer: JEditBuffer,
     start_line: Int, start: Int, num_lines: Int, removed: Int) =
   {
     if (col == null)
       col = new Text.Changed(start, 0, removed)
     else if (col.start > start + removed || start > col.start + col.added) {
-      commit()
+      commit
       col = new Text.Changed(start, 0, removed)
     }
     else {
       val offset = start - col.start
       val diff = col.added - removed

           (offset max 0, diff - (offset max 0))
         else
           (diff - (offset min 0), offset min 0)
       col = new Text.Changed(start min col.start, added, col.removed - add_removed)
     }
-    delay_commit()
+    delay_commit
   }
 
   override def bufferLoaded(buffer: JEditBuffer) { }
   override def foldHandlerChanged(buffer: JEditBuffer) { }
   override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }