# HG changeset patch # User wenzelm # Date 1291232080 -3600 # Node ID 8662b9b1f1232716187d15daf0baa8def071c15e # Parent df8c7dc30214daded172e409934a8e89b0639bd5 more abstract/uniform handling of time, preferring seconds as Double; diff -r df8c7dc30214 -r 8662b9b1f123 src/Pure/General/markup.scala --- 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 } } diff -r df8c7dc30214 -r 8662b9b1f123 src/Pure/General/timing.scala --- 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 +} + diff -r df8c7dc30214 -r 8662b9b1f123 src/Pure/System/isabelle_process.scala --- 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 diff -r df8c7dc30214 -r 8662b9b1f123 src/Pure/System/session.scala --- 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 } diff -r df8c7dc30214 -r 8662b9b1f123 src/Pure/System/swing_thread.scala --- 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() } diff -r df8c7dc30214 -r 8662b9b1f123 src/Pure/library.scala --- 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) } } diff -r df8c7dc30214 -r 8662b9b1f123 src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r df8c7dc30214 -r 8662b9b1f123 src/Tools/jEdit/src/jedit/plugin.scala --- 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)) } }