src/Tools/jEdit/src/plugin.scala
changeset 57974 ba0b6c2338f0
parent 57867 abae8aff6262
child 57979 fc136831d6ca
equal deleted inserted replaced
57973:decf2e9289ab 57974:ba0b6c2338f0
   390         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
   390         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
   391 
   391 
   392       PIDE.session = new Session(resources) {
   392       PIDE.session = new Session(resources) {
   393         override def output_delay = PIDE.options.seconds("editor_output_delay")
   393         override def output_delay = PIDE.options.seconds("editor_output_delay")
   394         override def prune_delay = PIDE.options.seconds("editor_prune_delay")
   394         override def prune_delay = PIDE.options.seconds("editor_prune_delay")
       
   395         override def syslog_limit = PIDE.options.int("editor_syslog_limit")
   395         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   396         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
   396       }
   397       }
   397 
   398 
   398       PIDE.session.phase_changed += session_phase
   399       PIDE.session.phase_changed += session_phase
   399       PIDE.startup_failure = None
   400       PIDE.startup_failure = None