# HG changeset patch
# User wenzelm
# Date 1291283163 -3600
# Node ID aee98c88c5874bee7846c75553e1cd7b5ccabbee
# Parent  58d25beedcea2900d82af0905b86edd8e6711d97
builtin time bounds (again);

diff -r 58d25beedcea -r aee98c88c587 src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Thu Dec 02 10:44:33 2010 +0100
+++ b/src/Pure/General/timing.scala	Thu Dec 02 10:46:03 2010 +0100
@@ -14,6 +14,10 @@
 class Time(val ms: Long)
 {
   def seconds: Double = ms / 1000.0
+
+  def min(t: Time): Time = if (ms < t.ms) this else t
+  def max(t: Time): Time = if (ms > t.ms) this else t
+
   override def toString =
     String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
   def message: String = toString + "s"
diff -r 58d25beedcea -r aee98c88c587 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 02 10:44:33 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 02 10:46:03 2010 +0100
@@ -121,7 +121,7 @@
       HTML.encode(text) + "</pre></html>"
 
   def tooltip_dismiss_delay(): Time =
-    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0))
+    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
 
   def setup_tooltips()
   {
@@ -230,7 +230,7 @@
 
   def start_session()
   {
-    val timeout = Time_Property("startup-timeout", Time.seconds(10))
+    val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
     val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
     val logic = {
       val logic = Property("logic")