more abstract/uniform handling of time, preferring seconds as Double;

--- a/src/Pure/General/markup.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/General/markup.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -227,15 +227,14 @@
   {
     def apply(timing: isabelle.Timing): Markup =
       Markup(TIMING, List(
-        (ELAPSED, Double(timing.elapsed)),
-        (CPU, Double(timing.cpu)),
-        (GC, Double(timing.gc))))
+        (ELAPSED, Double(timing.elapsed.seconds)),
+        (CPU, Double(timing.cpu.seconds)),
+        (GC, Double(timing.gc.seconds))))
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, List(
-          (ELAPSED, Double(elapsed)),
-          (CPU, Double(cpu)),
-          (GC, Double(gc)))) => Some(isabelle.Timing(elapsed, cpu, gc))
+          (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
+            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
   }

--- a/src/Pure/General/timing.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/General/timing.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -6,15 +6,23 @@
 
 package isabelle
 
-
-sealed case class Timing(val elapsed: Double, cpu: Double, gc: Double)
+object Time
 {
-  private def print_time(seconds: Double): String =
-    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
-
-  def message: String =
-    print_time(elapsed) + "s elapsed time, " +
-    print_time(cpu) + "s cpu time, " +
-    print_time(gc) + "s GC time"
+  def seconds(s: Double): Time = new Time((s * 1000.0) round)
 }
 
+class Time(val ms: Long)
+{
+  def seconds: Double = ms / 1000.0
+  override def toString =
+    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
+  def message: String = toString + "s"
+}
+
+class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
+{
+  def message: String =
+    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
+  override def toString = message
+}
+

--- a/src/Pure/System/isabelle_process.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/System/isabelle_process.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -61,7 +61,7 @@
 }
 
 
-class Isabelle_Process(system: Isabelle_System, timeout: Int, receiver: Actor, args: String*)
+class Isabelle_Process(system: Isabelle_System, timeout: Time, receiver: Actor, args: String*)
 {
   import Isabelle_Process._
 
@@ -69,7 +69,7 @@
   /* demo constructor */
 
   def this(args: String*) =
-    this(new Isabelle_System, 10000,
+    this(new Isabelle_System, Time.seconds(10),
       actor { loop { react { case res => Console.println(res) } } }, args: _*)
 
 
@@ -141,7 +141,7 @@
   {
     val (startup_failed, startup_output) =
     {
-      val expired = System.currentTimeMillis() + timeout
+      val expired = System.currentTimeMillis() + timeout.ms
       val result = new StringBuilder(100)
 
       var finished: Option[Boolean] = None

--- a/src/Pure/System/session.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/System/session.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -36,13 +36,13 @@
   /* real time parameters */  // FIXME properties or settings (!?)
 
   // user input (e.g. text edits, cursor movement)
-  val input_delay = 300
+  val input_delay = Time.seconds(0.3)
 
   // prover output (markup, common messages)
-  val output_delay = 100
+  val output_delay = Time.seconds(0.1)
 
   // GUI layout updates
-  val update_delay = 500
+  val update_delay = Time.seconds(0.5)
 
 
   /* pervasive event buses */
@@ -74,15 +74,13 @@
     Simple_Thread.actor("command_change_buffer", daemon = true)
   //{{{
   {
-    import scala.compat.Platform.currentTime
-
     var changed: Set[Command] = Set()
     var flush_time: Option[Long] = None
 
     def flush_timeout: Long =
       flush_time match {
         case None => 5000L
-        case Some(time) => (time - currentTime) max 0
+        case Some(time) => (time - System.currentTimeMillis()) max 0
       }
 
     def flush()
@@ -94,9 +92,9 @@
 
     def invoke()
     {
-      val now = currentTime
+      val now = System.currentTimeMillis()
       flush_time match {
-        case None => flush_time = Some(now + output_delay)
+        case None => flush_time = Some(now + output_delay.ms)
         case Some(time) => if (now >= time) flush()
       }
     }
@@ -136,7 +134,7 @@
 
   private case object Interrupt_Prover
   private case class Edit_Version(edits: List[Document.Edit_Text])
-  private case class Start(timeout: Int, args: List[String])
+  private case class Start(timeout: Time, args: List[String])
 
   private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
   {
@@ -288,7 +286,7 @@
 
   /** main methods **/
 
-  def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
+  def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
 
   def stop() { command_change_buffer !? Stop; session_actor !? Stop }
 

--- a/src/Pure/System/swing_thread.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/System/swing_thread.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -44,12 +44,12 @@
 
   /* delayed actions */
 
-  private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
+  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): () => Unit =
   {
     val listener = new ActionListener {
       override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
     }
-    val timer = new Timer(time_span, listener)
+    val timer = new Timer(time.ms.toInt, listener)
     timer.setRepeats(false)
 
     def invoke() { if (first) timer.start() else timer.restart() }

--- a/src/Pure/library.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Pure/library.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -137,12 +137,12 @@
 
   def timeit[A](message: String)(e: => A) =
   {
-    val start = System.nanoTime()
+    val start = System.currentTimeMillis()
     val result = Exn.capture(e)
-    val stop = System.nanoTime()
+    val stop = System.currentTimeMillis()
     System.err.println(
       (if (message == null || message.isEmpty) "" else message + ": ") +
-        ((stop - start).toDouble / 1000000) + "ms elapsed time")
+        new Time(stop - start).message + " elapsed time")
     Exn.release(result)
   }
 }

--- a/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 01 20:34:40 2010 +0100
@@ -33,7 +33,7 @@
 options.isabelle.tooltip-margin=40
 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
 options.isabelle.tooltip-dismiss-delay=8000
-options.isabelle.startup-timeout=10000
+options.isabelle.startup-timeout=10.0
 options.isabelle.auto-start.title=Auto Start
 options.isabelle.auto-start=true
 

--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 15:38:05 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 20:34:40 2010 +0100
@@ -71,6 +71,17 @@
   }
 
 
+  object Double_Property
+  {
+    def apply(name: String): Double =
+      jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
+    def apply(name: String, default: Double): Double =
+      jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
+    def update(name: String, value: Double) =
+      jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
+  }
+
+
   /* font */
 
   def font_family(): String = jEdit.getProperty("view.font")
@@ -210,14 +221,14 @@
 
   def start_session()
   {
-    val timeout = Int_Property("startup-timeout") max 1000
+    val timeout = Double_Property("startup-timeout") max 5.0
     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(timeout, modes ::: List(logic))
+    session.start(Time.seconds(timeout), modes ::: List(logic))
   }
 }