# HG changeset patch
# User wenzelm
# Date 1347304652 -7200
# Node ID 332ab3748350fa836a78aff3ed89dbc01316189a
# Parent  c763444b34adc2073a7f2e1c80a840f03010f481
option jedit_load_delay;
tuned;

diff -r c763444b34ad -r 332ab3748350 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Sep 10 21:15:46 2012 +0200
+++ b/src/Pure/System/session.scala	Mon Sep 10 21:17:32 2012 +0200
@@ -52,7 +52,6 @@
   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 load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
   val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
   val prune_size = 0  // size of retained history
   val syslog_limit = 100
diff -r c763444b34ad -r 332ab3748350 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Sep 10 21:15:46 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Sep 10 21:17:32 2012 +0200
@@ -13,7 +13,10 @@
   -- "tooltip font size (according to HTML)"
 
 option jedit_tooltip_margin : int = 60
-  -- "margin for tooltip pretty-printing (in characters)"
+  -- "margin for tooltip pretty-printing"
 
 option jedit_tooltip_dismiss_delay : real = 8.0
-  -- "global delay for Swing tooltips (in seconds)"
+  -- "global delay for Swing tooltips"
+
+option jedit_load_delay : real = 0.5
+  -- "delay for file load operations (new buffers etc.)"
diff -r c763444b34ad -r 332ab3748350 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 10 21:15:46 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Mon Sep 10 21:17:32 2012 +0200
@@ -20,7 +20,8 @@
     Isabelle.options.make_component("jedit_relative_font_size"),
     Isabelle.options.make_component("jedit_tooltip_font_size"),
     Isabelle.options.make_component("jedit_tooltip_margin"),
-    Isabelle.options.make_component("jedit_tooltip_dismiss_delay"))
+    Isabelle.options.make_component("jedit_tooltip_dismiss_delay"),
+    Isabelle.options.make_component("jedit_load_delay"))
 
   override def _init()
   {
diff -r c763444b34ad -r 332ab3748350 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 10 21:15:46 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 10 21:17:32 2012 +0200
@@ -261,7 +261,7 @@
   /* theory files */
 
   private lazy val delay_load =
-    Swing_Thread.delay_last(Isabelle.session.load_delay)
+    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("jedit_load_delay")))
     {
       val view = jEdit.getActiveView()