--- 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
--- 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.)"
--- 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()
{
--- 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()