# HG changeset patch # User wenzelm # Date 1489589428 -3600 # Node ID 7e6ecd04b5fe202ef289567e5b5b9ccb6fed157c # Parent c97abf0fa0c12f5b3882bec0d0bed0ea29fe6133 dynamic session_options for tuning parameters and initial prover options; diff -r c97abf0fa0c1 -r 7e6ecd04b5fe etc/options --- a/etc/options Wed Mar 15 15:39:15 2017 +0100 +++ b/etc/options Wed Mar 15 15:50:28 2017 +0100 @@ -153,6 +153,9 @@ public option editor_prune_delay : real = 15 -- "delay to prune history (delete old versions)" +option editor_prune_size : int = 0 + -- "retained size of pruned history (delete old versions)" + public option editor_update_delay : real = 0.5 -- "delay for physical GUI updates" diff -r c97abf0fa0c1 -r 7e6ecd04b5fe src/Pure/PIDE/batch_session.scala --- a/src/Pure/PIDE/batch_session.scala Wed Mar 15 15:39:15 2017 +0100 +++ b/src/Pure/PIDE/batch_session.scala Wed Mar 15 15:50:28 2017 +0100 @@ -33,7 +33,7 @@ val progress = new Console_Progress(verbose = verbose) - val prover_session = new Session(resources) + val prover_session = new Session(options, resources) val batch_session = new Batch_Session(prover_session) val handler = new Build.Handler(progress, session) diff -r c97abf0fa0c1 -r 7e6ecd04b5fe src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Mar 15 15:39:15 2017 +0100 +++ b/src/Pure/PIDE/session.scala Wed Mar 15 15:50:28 2017 +0100 @@ -114,7 +114,7 @@ } -class Session(val resources: Resources) extends Document.Session +class Session(session_options: => Options, val resources: Resources) extends Document.Session { session => @@ -127,13 +127,13 @@ @volatile var verbose: Boolean = false - /* tuning parameters */ + /* dynamic session options */ - def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages) - def prune_delay: Time = Time.seconds(15.0) // prune history (delete old versions) - def prune_size: Int = 0 // size of retained history - def syslog_limit: Int = 100 - def reparse_limit: Int = 0 + def output_delay: Time = session_options.seconds("editor_output_delay") + def prune_delay: Time = session_options.seconds("editor_prune_delay") + def prune_size: Int = session_options.int("editor_prune_size") + def syslog_limit: Int = session_options.int("editor_syslog_limit") + def reparse_limit: Int = session_options.int("editor_reparse_limit") /* outlets */ @@ -442,6 +442,7 @@ accumulate(state_id, output.message) case _ if output.is_init => + prover.get.options(session_options) phase = Session.Ready debugger.ready() diff -r c97abf0fa0c1 -r 7e6ecd04b5fe src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Mar 15 15:39:15 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Mar 15 15:50:28 2017 +0100 @@ -233,12 +233,7 @@ delay_load.invoke() } - Some(new Session(resources) { - override def output_delay = options.seconds("editor_output_delay") - override def prune_delay = options.seconds("editor_prune_delay") - override def syslog_limit = options.int("editor_syslog_limit") - override def reparse_limit = options.int("editor_reparse_limit") - }) + Some(new Session(options, resources)) } catch { case ERROR(msg) => reply(msg); None } @@ -255,7 +250,6 @@ Session.Consumer(getClass.getName) { case Session.Ready => session.phase_changed -= session_phase - session.update_options(options) reply("") case Session.Terminated(rc) if rc != 0 => session.phase_changed -= session_phase diff -r c97abf0fa0c1 -r 7e6ecd04b5fe src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Mar 15 15:39:15 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Wed Mar 15 15:50:28 2017 +0100 @@ -87,16 +87,7 @@ /* session */ private var _session: Session = null - private def init_session() - { - _session = - new Session(resources) { - override def output_delay = options.seconds("editor_output_delay") - override def prune_delay = options.seconds("editor_prune_delay") - override def syslog_limit = options.int("editor_syslog_limit") - override def reparse_limit = options.int("editor_reparse_limit") - } - } + private def init_session(): Unit = _session = new Session(options.value, resources) def session: Session = _session @@ -208,7 +199,6 @@ } case Session.Ready => - session.update_options(options.value) init_models() if (!Isabelle.continuous_checking) {