# HG changeset patch
# User wenzelm
# Date 1353875000 -3600
# Node ID 54be125d8cdcc8774c287f93e76179badd710f27
# Parent  6626bc5ed053887c9b1f006992b8602cba18015e
tuned signature;

diff -r 6626bc5ed053 -r 54be125d8cdc src/Pure/System/build.scala
--- 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)
diff -r 6626bc5ed053 -r 54be125d8cdc src/Pure/System/options.scala
--- 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
 }
 
diff -r 6626bc5ed053 -r 54be125d8cdc src/Tools/jEdit/src/document_model.scala
--- 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)
     {
diff -r 6626bc5ed053 -r 54be125d8cdc src/Tools/jEdit/src/document_view.scala
--- 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 =>
diff -r 6626bc5ed053 -r 54be125d8cdc src/Tools/jEdit/src/info_dockable.scala
--- 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() }
diff -r 6626bc5ed053 -r 54be125d8cdc src/Tools/jEdit/src/output_dockable.scala
--- 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() }
diff -r 6626bc5ed053 -r 54be125d8cdc src/Tools/jEdit/src/plugin.scala
--- 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")
       }
 
diff -r 6626bc5ed053 -r 54be125d8cdc src/Tools/jEdit/src/symbols_dockable.scala
--- 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 =