more abstract/uniform handling of time, preferring seconds as Double;
authorwenzelm
Wed Dec 01 20:34:40 2010 +0100 (2010-12-01 ago)
changeset 408488662b9b1f123
parent 40847 df8c7dc30214
child 40849 09270033330e
more abstract/uniform handling of time, preferring seconds as Double;
src/Pure/General/markup.scala
src/Pure/General/timing.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/session.scala
src/Pure/System/swing_thread.scala
src/Pure/library.scala
src/Tools/jEdit/plugin/Isabelle.props
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Pure/General/markup.scala	Wed Dec 01 15:38:05 2010 +0100
     1.2 +++ b/src/Pure/General/markup.scala	Wed Dec 01 20:34:40 2010 +0100
     1.3 @@ -227,15 +227,14 @@
     1.4    {
     1.5      def apply(timing: isabelle.Timing): Markup =
     1.6        Markup(TIMING, List(
     1.7 -        (ELAPSED, Double(timing.elapsed)),
     1.8 -        (CPU, Double(timing.cpu)),
     1.9 -        (GC, Double(timing.gc))))
    1.10 +        (ELAPSED, Double(timing.elapsed.seconds)),
    1.11 +        (CPU, Double(timing.cpu.seconds)),
    1.12 +        (GC, Double(timing.gc.seconds))))
    1.13      def unapply(markup: Markup): Option[isabelle.Timing] =
    1.14        markup match {
    1.15          case Markup(TIMING, List(
    1.16 -          (ELAPSED, Double(elapsed)),
    1.17 -          (CPU, Double(cpu)),
    1.18 -          (GC, Double(gc)))) => Some(isabelle.Timing(elapsed, cpu, gc))
    1.19 +          (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
    1.20 +            Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
    1.21          case _ => None
    1.22        }
    1.23    }
     2.1 --- a/src/Pure/General/timing.scala	Wed Dec 01 15:38:05 2010 +0100
     2.2 +++ b/src/Pure/General/timing.scala	Wed Dec 01 20:34:40 2010 +0100
     2.3 @@ -6,15 +6,23 @@
     2.4  
     2.5  package isabelle
     2.6  
     2.7 -
     2.8 -sealed case class Timing(val elapsed: Double, cpu: Double, gc: Double)
     2.9 +object Time
    2.10  {
    2.11 -  private def print_time(seconds: Double): String =
    2.12 -    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
    2.13 -
    2.14 -  def message: String =
    2.15 -    print_time(elapsed) + "s elapsed time, " +
    2.16 -    print_time(cpu) + "s cpu time, " +
    2.17 -    print_time(gc) + "s GC time"
    2.18 +  def seconds(s: Double): Time = new Time((s * 1000.0) round)
    2.19  }
    2.20  
    2.21 +class Time(val ms: Long)
    2.22 +{
    2.23 +  def seconds: Double = ms / 1000.0
    2.24 +  override def toString =
    2.25 +    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
    2.26 +  def message: String = toString + "s"
    2.27 +}
    2.28 +
    2.29 +class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
    2.30 +{
    2.31 +  def message: String =
    2.32 +    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
    2.33 +  override def toString = message
    2.34 +}
    2.35 +
     3.1 --- a/src/Pure/System/isabelle_process.scala	Wed Dec 01 15:38:05 2010 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Dec 01 20:34:40 2010 +0100
     3.3 @@ -61,7 +61,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Isabelle_Process(system: Isabelle_System, timeout: Int, receiver: Actor, args: String*)
     3.8 +class Isabelle_Process(system: Isabelle_System, timeout: Time, receiver: Actor, args: String*)
     3.9  {
    3.10    import Isabelle_Process._
    3.11  
    3.12 @@ -69,7 +69,7 @@
    3.13    /* demo constructor */
    3.14  
    3.15    def this(args: String*) =
    3.16 -    this(new Isabelle_System, 10000,
    3.17 +    this(new Isabelle_System, Time.seconds(10),
    3.18        actor { loop { react { case res => Console.println(res) } } }, args: _*)
    3.19  
    3.20  
    3.21 @@ -141,7 +141,7 @@
    3.22    {
    3.23      val (startup_failed, startup_output) =
    3.24      {
    3.25 -      val expired = System.currentTimeMillis() + timeout
    3.26 +      val expired = System.currentTimeMillis() + timeout.ms
    3.27        val result = new StringBuilder(100)
    3.28  
    3.29        var finished: Option[Boolean] = None
     4.1 --- a/src/Pure/System/session.scala	Wed Dec 01 15:38:05 2010 +0100
     4.2 +++ b/src/Pure/System/session.scala	Wed Dec 01 20:34:40 2010 +0100
     4.3 @@ -36,13 +36,13 @@
     4.4    /* real time parameters */  // FIXME properties or settings (!?)
     4.5  
     4.6    // user input (e.g. text edits, cursor movement)
     4.7 -  val input_delay = 300
     4.8 +  val input_delay = Time.seconds(0.3)
     4.9  
    4.10    // prover output (markup, common messages)
    4.11 -  val output_delay = 100
    4.12 +  val output_delay = Time.seconds(0.1)
    4.13  
    4.14    // GUI layout updates
    4.15 -  val update_delay = 500
    4.16 +  val update_delay = Time.seconds(0.5)
    4.17  
    4.18  
    4.19    /* pervasive event buses */
    4.20 @@ -74,15 +74,13 @@
    4.21      Simple_Thread.actor("command_change_buffer", daemon = true)
    4.22    //{{{
    4.23    {
    4.24 -    import scala.compat.Platform.currentTime
    4.25 -
    4.26      var changed: Set[Command] = Set()
    4.27      var flush_time: Option[Long] = None
    4.28  
    4.29      def flush_timeout: Long =
    4.30        flush_time match {
    4.31          case None => 5000L
    4.32 -        case Some(time) => (time - currentTime) max 0
    4.33 +        case Some(time) => (time - System.currentTimeMillis()) max 0
    4.34        }
    4.35  
    4.36      def flush()
    4.37 @@ -94,9 +92,9 @@
    4.38  
    4.39      def invoke()
    4.40      {
    4.41 -      val now = currentTime
    4.42 +      val now = System.currentTimeMillis()
    4.43        flush_time match {
    4.44 -        case None => flush_time = Some(now + output_delay)
    4.45 +        case None => flush_time = Some(now + output_delay.ms)
    4.46          case Some(time) => if (now >= time) flush()
    4.47        }
    4.48      }
    4.49 @@ -136,7 +134,7 @@
    4.50  
    4.51    private case object Interrupt_Prover
    4.52    private case class Edit_Version(edits: List[Document.Edit_Text])
    4.53 -  private case class Start(timeout: Int, args: List[String])
    4.54 +  private case class Start(timeout: Time, args: List[String])
    4.55  
    4.56    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    4.57    {
    4.58 @@ -288,7 +286,7 @@
    4.59  
    4.60    /** main methods **/
    4.61  
    4.62 -  def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
    4.63 +  def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
    4.64  
    4.65    def stop() { command_change_buffer !? Stop; session_actor !? Stop }
    4.66  
     5.1 --- a/src/Pure/System/swing_thread.scala	Wed Dec 01 15:38:05 2010 +0100
     5.2 +++ b/src/Pure/System/swing_thread.scala	Wed Dec 01 20:34:40 2010 +0100
     5.3 @@ -44,12 +44,12 @@
     5.4  
     5.5    /* delayed actions */
     5.6  
     5.7 -  private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
     5.8 +  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): () => Unit =
     5.9    {
    5.10      val listener = new ActionListener {
    5.11        override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
    5.12      }
    5.13 -    val timer = new Timer(time_span, listener)
    5.14 +    val timer = new Timer(time.ms.toInt, listener)
    5.15      timer.setRepeats(false)
    5.16  
    5.17      def invoke() { if (first) timer.start() else timer.restart() }
     6.1 --- a/src/Pure/library.scala	Wed Dec 01 15:38:05 2010 +0100
     6.2 +++ b/src/Pure/library.scala	Wed Dec 01 20:34:40 2010 +0100
     6.3 @@ -137,12 +137,12 @@
     6.4  
     6.5    def timeit[A](message: String)(e: => A) =
     6.6    {
     6.7 -    val start = System.nanoTime()
     6.8 +    val start = System.currentTimeMillis()
     6.9      val result = Exn.capture(e)
    6.10 -    val stop = System.nanoTime()
    6.11 +    val stop = System.currentTimeMillis()
    6.12      System.err.println(
    6.13        (if (message == null || message.isEmpty) "" else message + ": ") +
    6.14 -        ((stop - start).toDouble / 1000000) + "ms elapsed time")
    6.15 +        new Time(stop - start).message + " elapsed time")
    6.16      Exn.release(result)
    6.17    }
    6.18  }
     7.1 --- a/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 01 15:38:05 2010 +0100
     7.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props	Wed Dec 01 20:34:40 2010 +0100
     7.3 @@ -33,7 +33,7 @@
     7.4  options.isabelle.tooltip-margin=40
     7.5  options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
     7.6  options.isabelle.tooltip-dismiss-delay=8000
     7.7 -options.isabelle.startup-timeout=10000
     7.8 +options.isabelle.startup-timeout=10.0
     7.9  options.isabelle.auto-start.title=Auto Start
    7.10  options.isabelle.auto-start=true
    7.11  
     8.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 15:38:05 2010 +0100
     8.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 01 20:34:40 2010 +0100
     8.3 @@ -71,6 +71,17 @@
     8.4    }
     8.5  
     8.6  
     8.7 +  object Double_Property
     8.8 +  {
     8.9 +    def apply(name: String): Double =
    8.10 +      jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
    8.11 +    def apply(name: String, default: Double): Double =
    8.12 +      jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
    8.13 +    def update(name: String, value: Double) =
    8.14 +      jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
    8.15 +  }
    8.16 +
    8.17 +
    8.18    /* font */
    8.19  
    8.20    def font_family(): String = jEdit.getProperty("view.font")
    8.21 @@ -210,14 +221,14 @@
    8.22  
    8.23    def start_session()
    8.24    {
    8.25 -    val timeout = Int_Property("startup-timeout") max 1000
    8.26 +    val timeout = Double_Property("startup-timeout") max 5.0
    8.27      val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    8.28      val logic = {
    8.29        val logic = Property("logic")
    8.30        if (logic != null && logic != "") logic
    8.31        else Isabelle.default_logic()
    8.32      }
    8.33 -    session.start(timeout, modes ::: List(logic))
    8.34 +    session.start(Time.seconds(timeout), modes ::: List(logic))
    8.35    }
    8.36  }
    8.37