src/Tools/jEdit/src/text_overview.scala
changeset 61747 a870098fc27e
parent 61723 7feee72b5897
child 61904 30f70d1b97c9
equal deleted inserted replaced
61746:3df1b6a5837c 61747:a870098fc27e
    23   private val text_area = doc_view.text_area
    23   private val text_area = doc_view.text_area
    24   private val buffer = doc_view.model.buffer
    24   private val buffer = doc_view.model.buffer
    25 
    25 
    26   private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
    26   private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
    27 
    27 
    28   private val WIDTH = 10
    28   private val WIDTH = text_area.getPainter.getFontMetrics.stringWidth("A") max 10
    29   private val HEIGHT = 4
    29   private val HEIGHT = 4
    30 
    30 
    31   setPreferredSize(new Dimension(WIDTH, 0))
    31   setPreferredSize(new Dimension(WIDTH, 0))
    32 
    32 
    33   setRequestFocusEnabled(false)
    33   setRequestFocusEnabled(false)