# HG changeset patch # User wenzelm # Date 1291300652 -3600 # Node ID 9e1136e8bb1f8f0ac4e4cbf1fe9afea3aa9dc530 # Parent e2929572d5c761cf73442362b66f80727d4541fb# Parent 996e55b3ae347d6c6cd75861dcc920bf71f3cd3e merged diff -r e2929572d5c7 -r 9e1136e8bb1f src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Pure/General/markup.scala Thu Dec 02 15:37:32 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 e2929572d5c7 -r 9e1136e8bb1f src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Pure/General/timing.scala Thu Dec 02 15:37:32 2010 +0100 @@ -6,15 +6,27 @@ 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 + + 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" +} + +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 e2929572d5c7 -r 9e1136e8bb1f src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Pure/System/isabelle_process.scala Thu Dec 02 15:37:32 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 e2929572d5c7 -r 9e1136e8bb1f src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Pure/System/session.scala Thu Dec 02 15:37:32 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 e2929572d5c7 -r 9e1136e8bb1f src/Pure/System/swing_thread.scala --- a/src/Pure/System/swing_thread.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Pure/System/swing_thread.scala Thu Dec 02 15:37:32 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 e2929572d5c7 -r 9e1136e8bb1f src/Pure/library.scala --- a/src/Pure/library.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Pure/library.scala Thu Dec 02 15:37:32 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 e2929572d5c7 -r 9e1136e8bb1f src/Tools/jEdit/plugin/Isabelle.props --- a/src/Tools/jEdit/plugin/Isabelle.props Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Tools/jEdit/plugin/Isabelle.props Thu Dec 02 15:37:32 2010 +0100 @@ -32,8 +32,8 @@ options.isabelle.tooltip-margin.title=Tooltip Margin 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.tooltip-dismiss-delay=8.0 +options.isabelle.startup-timeout=10.0 options.isabelle.auto-start.title=Auto Start options.isabelle.auto-start=true diff -r e2929572d5c7 -r 9e1136e8bb1f src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu Dec 02 15:37:32 2010 +0100 @@ -63,7 +63,7 @@ extends TokenMarker.LineContext(dummy_rules, prev) { override def hashCode: Int = line - override def equals(that: Any) = + override def equals(that: Any): Boolean = that match { case other: Line_Context => line == other.line case _ => false diff -r e2929572d5c7 -r 9e1136e8bb1f src/Tools/jEdit/src/jedit/isabelle_options.scala --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Thu Dec 02 15:37:32 2010 +0100 @@ -7,6 +7,8 @@ package isabelle.jedit +import isabelle._ + import javax.swing.JSpinner import scala.swing.CheckBox @@ -39,7 +41,8 @@ tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40)) addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin) - tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000)) + tooltip_dismiss_delay.setValue( + Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt) addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay) } @@ -58,7 +61,7 @@ Isabelle.Int_Property("tooltip-margin") = tooltip_margin.getValue().asInstanceOf[Int] - Isabelle.Int_Property("tooltip-dismiss-delay") = - tooltip_dismiss_delay.getValue().asInstanceOf[Int] + Isabelle.Time_Property("tooltip-dismiss-delay") = + Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int]) } } diff -r e2929572d5c7 -r 9e1136e8bb1f src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Thu Dec 02 15:32:48 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Thu Dec 02 15:37:32 2010 +0100 @@ -70,6 +70,26 @@ jEdit.setIntegerProperty(OPTION_PREFIX + name, value) } + 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) + } + + 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 */ @@ -100,14 +120,14 @@ Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?) HTML.encode(text) + "" - def tooltip_dismiss_delay(): Int = - Int_Property("tooltip-dismiss-delay", 8000) max 500 + def tooltip_dismiss_delay(): Time = + Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5) def setup_tooltips() { Swing_Thread.now { val manager = javax.swing.ToolTipManager.sharedInstance - manager.setDismissDelay(tooltip_dismiss_delay()) + manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt) } } @@ -210,7 +230,7 @@ def start_session() { - val timeout = Int_Property("startup-timeout") max 1000 + 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")