src/Tools/jEdit/src/plugin.scala
changeset 50207 54be125d8cdc
parent 50206 6626bc5ed053
child 50208 1382ad6d4774
--- 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")
       }