--- a/src/Tools/jEdit/src/plugin.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 25 21:23:20 2012 +0100
@@ -141,7 +141,7 @@
/* theory files */
private lazy val delay_load =
- Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_load_delay")))
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
{
val view = jEdit.getActiveView()
@@ -286,7 +286,7 @@
val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
PIDE.session = new Session(thy_load) {
- override def output_delay = Time.seconds(PIDE.options.real("editor_output_delay"))
+ override def output_delay = PIDE.options.seconds("editor_output_delay")
override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}