--- 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
}
}
--- 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
+}
+
--- 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
--- 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 }
--- 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() }
--- 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)
}
}
--- 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
--- 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
--- 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])
}
}
--- 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) + "</pre></html>"
- 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")