src/Tools/jEdit/src/plugin.scala
changeset 52815 eaad5fe7bb1b
parent 52807 b859a180936b
child 52816 c608e0ade554
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 18:08:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 19:59:14 2013 +0200
     1.3 @@ -35,6 +35,8 @@
     1.4    @volatile var plugin: Plugin = null
     1.5    @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
     1.6  
     1.7 +  def options_changed() { session.global_options.event(Session.Global_Options(options.value)) }
     1.8 +
     1.9    def thy_load(): JEdit_Thy_Load =
    1.10      session.thy_load.asInstanceOf[JEdit_Thy_Load]
    1.11  
    1.12 @@ -115,39 +117,6 @@
    1.13        Document_View.exit(text_area)
    1.14      }
    1.15    }
    1.16 -
    1.17 -
    1.18 -  /* continuous checking */
    1.19 -
    1.20 -  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    1.21 -
    1.22 -  def continuous_checking: Boolean = options.bool(CONTINUOUS_CHECKING)
    1.23 -
    1.24 -  def continuous_checking_=(b: Boolean)
    1.25 -  {
    1.26 -    Swing_Thread.require()
    1.27 -
    1.28 -    if (continuous_checking != b) {
    1.29 -      options.bool(CONTINUOUS_CHECKING) = b
    1.30 -      PIDE.session.global_options.event(Session.Global_Options(options.value))
    1.31 -
    1.32 -      PIDE.session.update(
    1.33 -        (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    1.34 -          case (edits, buffer) =>
    1.35 -            JEdit_Lib.buffer_lock(buffer) {
    1.36 -              document_model(buffer) match {
    1.37 -                case Some(model) => model.flushed_edits() ::: edits
    1.38 -                case None => edits
    1.39 -              }
    1.40 -            }
    1.41 -        }
    1.42 -      )
    1.43 -    }
    1.44 -  }
    1.45 -
    1.46 -  def set_continuous_checking() { continuous_checking = true }
    1.47 -  def reset_continuous_checking() { continuous_checking = false }
    1.48 -  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    1.49  }
    1.50  
    1.51