src/Tools/jEdit/src/document_view.scala
changeset 50205 788c8263e634
parent 50199 6d04e2422769
child 50207 54be125d8cdc
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 20:31:49 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 20:59:32 2012 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4  {
     1.5    private val session = model.session
     1.6  
     1.7 -  def get_rendering(): Rendering = Rendering(model.snapshot(), Isabelle.options.value)
     1.8 +  def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
     1.9  
    1.10    val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
    1.11  
    1.12 @@ -147,7 +147,7 @@
    1.13    /* caret handling */
    1.14  
    1.15    private val delay_caret_update =
    1.16 -    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
    1.17 +    Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
    1.18        session.caret_focus.event(Session.Caret_Focus)
    1.19      }
    1.20  
    1.21 @@ -161,8 +161,7 @@
    1.22    private object overview extends Text_Overview(this)
    1.23    {
    1.24      val delay_repaint =
    1.25 -      Swing_Thread.delay_first(
    1.26 -        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
    1.27 +      Swing_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay"))) { repaint() }
    1.28    }
    1.29  
    1.30  
    1.31 @@ -173,8 +172,7 @@
    1.32        react {
    1.33          case _: Session.Raw_Edits =>
    1.34            Swing_Thread.later {
    1.35 -            overview.delay_repaint.postpone(
    1.36 -              Time.seconds(Isabelle.options.real("editor_input_delay")))
    1.37 +            overview.delay_repaint.postpone(Time.seconds(PIDE.options.real("editor_input_delay")))
    1.38            }
    1.39  
    1.40          case changed: Session.Commands_Changed =>