dynamic session_options for tuning parameters and initial prover options;
authorwenzelm
Wed Mar 15 15:50:28 2017 +0100 (2017-03-15)
changeset 652647e6ecd04b5fe
parent 65263 c97abf0fa0c1
child 65265 f994a61376eb
dynamic session_options for tuning parameters and initial prover options;
etc/options
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/session.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/etc/options	Wed Mar 15 15:39:15 2017 +0100
     1.2 +++ b/etc/options	Wed Mar 15 15:50:28 2017 +0100
     1.3 @@ -153,6 +153,9 @@
     1.4  public option editor_prune_delay : real = 15
     1.5    -- "delay to prune history (delete old versions)"
     1.6  
     1.7 +option editor_prune_size : int = 0
     1.8 +  -- "retained size of pruned history (delete old versions)"
     1.9 +
    1.10  public option editor_update_delay : real = 0.5
    1.11    -- "delay for physical GUI updates"
    1.12  
     2.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Mar 15 15:39:15 2017 +0100
     2.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Mar 15 15:50:28 2017 +0100
     2.3 @@ -33,7 +33,7 @@
     2.4  
     2.5      val progress = new Console_Progress(verbose = verbose)
     2.6  
     2.7 -    val prover_session = new Session(resources)
     2.8 +    val prover_session = new Session(options, resources)
     2.9      val batch_session = new Batch_Session(prover_session)
    2.10  
    2.11      val handler = new Build.Handler(progress, session)
     3.1 --- a/src/Pure/PIDE/session.scala	Wed Mar 15 15:39:15 2017 +0100
     3.2 +++ b/src/Pure/PIDE/session.scala	Wed Mar 15 15:50:28 2017 +0100
     3.3 @@ -114,7 +114,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Session(val resources: Resources) extends Document.Session
     3.8 +class Session(session_options: => Options, val resources: Resources) extends Document.Session
     3.9  {
    3.10    session =>
    3.11  
    3.12 @@ -127,13 +127,13 @@
    3.13    @volatile var verbose: Boolean = false
    3.14  
    3.15  
    3.16 -  /* tuning parameters */
    3.17 +  /* dynamic session options */
    3.18  
    3.19 -  def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
    3.20 -  def prune_delay: Time = Time.seconds(15.0)  // prune history (delete old versions)
    3.21 -  def prune_size: Int = 0  // size of retained history
    3.22 -  def syslog_limit: Int = 100
    3.23 -  def reparse_limit: Int = 0
    3.24 +  def output_delay: Time = session_options.seconds("editor_output_delay")
    3.25 +  def prune_delay: Time = session_options.seconds("editor_prune_delay")
    3.26 +  def prune_size: Int = session_options.int("editor_prune_size")
    3.27 +  def syslog_limit: Int = session_options.int("editor_syslog_limit")
    3.28 +  def reparse_limit: Int = session_options.int("editor_reparse_limit")
    3.29  
    3.30  
    3.31    /* outlets */
    3.32 @@ -442,6 +442,7 @@
    3.33                accumulate(state_id, output.message)
    3.34  
    3.35              case _ if output.is_init =>
    3.36 +              prover.get.options(session_options)
    3.37                phase = Session.Ready
    3.38                debugger.ready()
    3.39  
     4.1 --- a/src/Tools/VSCode/src/server.scala	Wed Mar 15 15:39:15 2017 +0100
     4.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Mar 15 15:50:28 2017 +0100
     4.3 @@ -233,12 +233,7 @@
     4.4                  delay_load.invoke()
     4.5            }
     4.6  
     4.7 -        Some(new Session(resources) {
     4.8 -          override def output_delay = options.seconds("editor_output_delay")
     4.9 -          override def prune_delay = options.seconds("editor_prune_delay")
    4.10 -          override def syslog_limit = options.int("editor_syslog_limit")
    4.11 -          override def reparse_limit = options.int("editor_reparse_limit")
    4.12 -        })
    4.13 +        Some(new Session(options, resources))
    4.14        }
    4.15        catch { case ERROR(msg) => reply(msg); None }
    4.16  
    4.17 @@ -255,7 +250,6 @@
    4.18          Session.Consumer(getClass.getName) {
    4.19            case Session.Ready =>
    4.20              session.phase_changed -= session_phase
    4.21 -            session.update_options(options)
    4.22              reply("")
    4.23            case Session.Terminated(rc) if rc != 0 =>
    4.24              session.phase_changed -= session_phase
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 15:39:15 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 15:50:28 2017 +0100
     5.3 @@ -87,16 +87,7 @@
     5.4    /* session */
     5.5  
     5.6    private var _session: Session = null
     5.7 -  private def init_session()
     5.8 -  {
     5.9 -    _session =
    5.10 -      new Session(resources) {
    5.11 -        override def output_delay = options.seconds("editor_output_delay")
    5.12 -        override def prune_delay = options.seconds("editor_prune_delay")
    5.13 -        override def syslog_limit = options.int("editor_syslog_limit")
    5.14 -        override def reparse_limit = options.int("editor_reparse_limit")
    5.15 -      }
    5.16 -  }
    5.17 +  private def init_session(): Unit = _session = new Session(options.value, resources)
    5.18    def session: Session = _session
    5.19  
    5.20  
    5.21 @@ -208,7 +199,6 @@
    5.22        }
    5.23  
    5.24      case Session.Ready =>
    5.25 -      session.update_options(options.value)
    5.26        init_models()
    5.27  
    5.28        if (!Isabelle.continuous_checking) {