# 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) {