equal
deleted
inserted
replaced
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 |