--- a/src/Pure/System/build.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Pure/System/build.scala Sun Nov 25 21:23:20 2012 +0100
@@ -472,7 +472,7 @@
def is_finished: Boolean = result.is_finished
@volatile private var timeout = false
- private val time = Time.seconds(info.options.real("timeout"))
+ private val time = info.options.seconds("timeout")
private val timer: Option[Timer] =
if (time.seconds > 0.0) {
val t = new Timer("build", true)
--- a/src/Pure/System/options.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Pure/System/options.scala Sun Nov 25 21:23:20 2012 +0100
@@ -229,6 +229,12 @@
}
val string = new String_Access
+ class Seconds_Access
+ {
+ def apply(name: String): Time = Time.seconds(real(name))
+ }
+ val seconds = new Seconds_Access
+
/* external updates */
@@ -410,5 +416,11 @@
}
}
val string = new String_Access
+
+ class Seconds_Access
+ {
+ def apply(name: String): Time = options.seconds(name)
+ }
+ val seconds = new Seconds_Access
}
--- a/src/Tools/jEdit/src/document_model.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Nov 25 21:23:20 2012 +0100
@@ -115,7 +115,7 @@
}
private val delay_flush =
- Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) { flush() }
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
def +=(edit: Text.Edit)
{
--- a/src/Tools/jEdit/src/document_view.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sun Nov 25 21:23:20 2012 +0100
@@ -147,7 +147,7 @@
/* caret handling */
private val delay_caret_update =
- Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
session.caret_focus.event(Session.Caret_Focus)
}
@@ -161,7 +161,7 @@
private object overview extends Text_Overview(this)
{
val delay_repaint =
- Swing_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay"))) { repaint() }
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
}
@@ -172,7 +172,7 @@
react {
case _: Session.Raw_Edits =>
Swing_Thread.later {
- overview.delay_repaint.postpone(Time.seconds(PIDE.options.real("editor_input_delay")))
+ overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
}
case changed: Session.Commands_Changed =>
--- a/src/Tools/jEdit/src/info_dockable.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sun Nov 25 21:23:20 2012 +0100
@@ -115,8 +115,7 @@
/* resize */
private val delay_resize =
- Swing_Thread.delay_first(
- Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/output_dockable.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sun Nov 25 21:23:20 2012 +0100
@@ -136,8 +136,7 @@
/* resize */
private val delay_resize =
- Swing_Thread.delay_first(
- Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
+ Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/plugin.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 25 21:23:20 2012 +0100
@@ -141,7 +141,7 @@
/* theory files */
private lazy val delay_load =
- Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_load_delay")))
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
{
val view = jEdit.getActiveView()
@@ -286,7 +286,7 @@
val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
PIDE.session = new Session(thy_load) {
- override def output_delay = Time.seconds(PIDE.options.real("editor_output_delay"))
+ override def output_delay = PIDE.options.seconds("editor_output_delay")
override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}
--- a/src/Tools/jEdit/src/symbols_dockable.scala Sun Nov 25 21:10:29 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sun Nov 25 21:23:20 2012 +0100
@@ -71,7 +71,7 @@
add(results_panel, BorderPanel.Position.Center)
listenTo(search)
val delay_search =
- Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
results_panel.contents.clear
val results =