src/Tools/jEdit/src/document_view.scala
changeset 43390 7ee98a3802af
parent 43387 a59ae768249e
child 43392 fe4b8c52b1cc
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 15:58:01 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jun 14 17:24:23 2011 +0200
     1.3 @@ -69,24 +69,6 @@
     1.4  
     1.5    /** token handling **/
     1.6  
     1.7 -  /* extended token styles */
     1.8 -
     1.9 -  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
    1.10 -
    1.11 -  def extend_styles()
    1.12 -  {
    1.13 -    Swing_Thread.require()
    1.14 -    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
    1.15 -  }
    1.16 -  extend_styles()
    1.17 -
    1.18 -  def set_styles()
    1.19 -  {
    1.20 -    Swing_Thread.require()
    1.21 -    text_area.getPainter.setStyles(styles)
    1.22 -  }
    1.23 -
    1.24 -
    1.25    /* visible line ranges */
    1.26  
    1.27    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.