more options;

--- a/etc/options	Tue Sep 11 16:10:54 2012 +0200
+++ b/etc/options	Tue Sep 11 19:19:39 2012 +0200
@@ -80,3 +80,18 @@
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
+
+section {* Editor session parameters *}
+
+option editor_load_delay : real = 0.5
+  -- "delay for file load operations (new buffers etc.)"
+
+option editor_input_delay : real = 0.3
+  -- "delay for user input (text edits, cursor movement etc.)"
+
+option editor_output_delay : real = 0.1
+  -- "delay for prover output (markup, common messages etc.)"
+
+option editor_update_delay : real = 0.5
+  -- "delay for physical GUI updates"
+

--- a/src/Pure/System/session.scala	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Sep 11 19:19:39 2012 +0200
@@ -46,15 +46,14 @@
   @volatile var verbose: Boolean = false
 
 
-  /* tuning parameters */  // FIXME properties or settings (!?)
+  /* tuning parameters */
+
+  def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
 
-  val message_delay = Time.seconds(0.01)  // prover messages
-  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
-  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
-  val update_delay = Time.seconds(0.5)  // GUI layout updates
-  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
-  val prune_size = 0  // size of retained history
-  val syslog_limit = 100
+  private val message_delay = Time.seconds(0.01)  // incoming prover messages
+  private val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
+  private val prune_size = 0  // size of retained history
+  private val syslog_limit = 100
 
 
   /* pervasive event buses */

--- a/src/Tools/jEdit/etc/options	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 11 19:19:39 2012 +0200
@@ -17,9 +17,3 @@
 
 option jedit_tooltip_dismiss_delay : real = 8.0
   -- "global delay for Swing tooltips"
-
-
-section {* Reactivity *}
-
-option jedit_load_delay : real = 0.5
-  -- "delay for file load operations (new buffers etc.)"

--- a/src/Tools/jEdit/src/document_model.scala	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Sep 11 19:19:39 2012 +0200
@@ -115,7 +115,8 @@
     }
 
     private val delay_flush =
-      Swing_Thread.delay_last(session.input_delay) { flush() }
+      Swing_Thread.delay_last(
+        Time.seconds(Isabelle.options.real("editor_input_delay"))) { flush() }
 
     def +=(edit: Text.Edit)
     {

--- a/src/Tools/jEdit/src/document_view.scala	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Sep 11 19:19:39 2012 +0200
@@ -341,7 +341,7 @@
   }
 
   private val delay_caret_update =
-    Swing_Thread.delay_last(session.input_delay) {
+    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
       session.caret_focus.event(Session.Caret_Focus)
     }
 
@@ -355,7 +355,8 @@
   private object overview extends Text_Overview(this)
   {
     val delay_repaint =
-      Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
+      Swing_Thread.delay_first(
+        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
   }
 
 
@@ -366,7 +367,8 @@
       react {
         case _: Session.Raw_Edits =>
           Swing_Thread.later {
-            overview.delay_repaint.postpone(Isabelle.session.input_delay)
+            overview.delay_repaint.postpone(
+              Time.seconds(Isabelle.options.real("editor_input_delay")))
           }
 
         case changed: Session.Commands_Changed =>

--- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 19:19:39 2012 +0200
@@ -17,7 +17,8 @@
   // FIXME avoid hard-wired stuff
   private val relevant_options =
     Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
-      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay")
+      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
+      "editor_input_delay", "editor_output_delay", "editor_update_delay")
 
   relevant_options.foreach(Isabelle.options.value.check_name _)
 

--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 11 19:19:39 2012 +0200
@@ -148,7 +148,8 @@
   /* resize */
 
   private val delay_resize =
-    Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
+    Swing_Thread.delay_first(
+      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }

--- a/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 16:10:54 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 19:19:39 2012 +0200
@@ -260,7 +260,7 @@
   /* theory files */
 
   private lazy val delay_load =
-    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("jedit_load_delay")))
+    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_load_delay")))
     {
       val view = jEdit.getActiveView()
 
@@ -406,7 +406,9 @@
 
       val content = Isabelle_Logic.session_content(false)
       val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
-      Isabelle.session = new Session(thy_load)
+      Isabelle.session = new Session(thy_load) {
+        override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
+      }
 
       Isabelle.session.phase_changed += session_manager
       Isabelle.startup_failure = None