src/Tools/jEdit/src/document_view.scala
changeset 49411 1da54e9bda68
parent 49410 34acbcc33adf
child 49424 491363c6feb4
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 20:23:25 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 20:34:19 2012 +0200
     1.3 @@ -67,6 +67,11 @@
     1.4  {
     1.5    private val session = model.session
     1.6  
     1.7 +  def get_rendering(): Isabelle_Rendering =
     1.8 +    Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
     1.9 +
    1.10 +  val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _)
    1.11 +
    1.12  
    1.13    /* perspective */
    1.14  
    1.15 @@ -97,12 +102,7 @@
    1.16    }
    1.17  
    1.18  
    1.19 -  /* text area painting */
    1.20 -
    1.21 -  def get_rendering(): Isabelle_Rendering =
    1.22 -    Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    1.23 -
    1.24 -  val text_area_painter = new Text_Area_Painter(text_area.getView, text_area, get_rendering _)
    1.25 +  /* gutter */
    1.26  
    1.27    private val gutter_painter = new TextAreaExtension
    1.28    {
    1.29 @@ -110,7 +110,7 @@
    1.30        first_line: Int, last_line: Int, physical_lines: Array[Int],
    1.31        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    1.32      {
    1.33 -      text_area_painter.robust_body(()) {
    1.34 +      rich_text_area.robust_body(()) {
    1.35          Swing_Thread.assert()
    1.36  
    1.37          val gutter = text_area.getGutter
    1.38 @@ -225,7 +225,7 @@
    1.39      val painter = text_area.getPainter
    1.40  
    1.41      painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
    1.42 -    text_area_painter.activate()
    1.43 +    rich_text_area.activate()
    1.44      text_area.getGutter.addExtension(gutter_painter)
    1.45      text_area.addCaretListener(caret_listener)
    1.46      text_area.addLeftOfScrollBar(overview)
    1.47 @@ -242,7 +242,7 @@
    1.48      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
    1.49      text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
    1.50      text_area.getGutter.removeExtension(gutter_painter)
    1.51 -    text_area_painter.deactivate()
    1.52 +    rich_text_area.deactivate()
    1.53      painter.removeExtension(update_perspective)
    1.54    }
    1.55  }