# HG changeset patch
# User wenzelm
# Date 1291235001 -3600
# Node ID d804de9ac97055432580a07b2a3e1058e59ccae8
# Parent  09270033330e9c27367dba98a683f30d13c366c5
more abstract handling of Time properties;

diff -r 09270033330e -r d804de9ac970 src/Tools/jEdit/src/jedit/isabelle_options.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed Dec 01 21:07:50 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed Dec 01 21:23:21 2010 +0100
@@ -7,6 +7,8 @@
 package isabelle.jedit
 
 
+import isabelle._
+
 import javax.swing.JSpinner
 
 import scala.swing.CheckBox
@@ -40,7 +42,7 @@
     addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
 
     tooltip_dismiss_delay.setValue(
-      (Isabelle.Double_Property("tooltip-dismiss-delay", 8.0) * 1000) round)
+      Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
     addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
   }
 
@@ -59,7 +61,7 @@
     Isabelle.Int_Property("tooltip-margin") =
       tooltip_margin.getValue().asInstanceOf[Int]
 
-    Isabelle.Double_Property("tooltip-dismiss-delay") =
-      tooltip_dismiss_delay.getValue().asInstanceOf[Int].toDouble / 1000
+    Isabelle.Time_Property("tooltip-dismiss-delay") =
+      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
   }
 }
diff -r 09270033330e -r d804de9ac970 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 21:07:50 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 21:23:21 2010 +0100
@@ -70,7 +70,6 @@
       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
   }
 
-
   object Double_Property
   {
     def apply(name: String): Double =
@@ -81,6 +80,16 @@
       jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
   }
 
+  object Time_Property
+  {
+    def apply(name: String): Time =
+      Time.seconds(Double_Property(name))
+    def apply(name: String, default: Time): Time =
+      Time.seconds(Double_Property(name, default.seconds))
+    def update(name: String, value: Time) =
+      Double_Property.update(name, value.seconds)
+  }
+
 
   /* font */
 
@@ -112,7 +121,7 @@
       HTML.encode(text) + "</pre></html>"
 
   def tooltip_dismiss_delay(): Time =
-    Time.seconds(Double_Property("tooltip-dismiss-delay", 8.0) max 0.5)
+    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0))
 
   def setup_tooltips()
   {
@@ -221,14 +230,14 @@
 
   def start_session()
   {
-    val timeout = Double_Property("startup-timeout") max 5.0
+    val timeout = Time_Property("startup-timeout", Time.seconds(10))
     val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
     val logic = {
       val logic = Property("logic")
       if (logic != null && logic != "") logic
       else Isabelle.default_logic()
     }
-    session.start(Time.seconds(timeout), modes ::: List(logic))
+    session.start(timeout, modes ::: List(logic))
   }
 }