tuned signature;
authorwenzelm
Sun Nov 25 21:23:20 2012 +0100 (2012-11-25)
changeset 5020754be125d8cdc
parent 50206 6626bc5ed053
child 50208 1382ad6d4774
tuned signature;
src/Pure/System/build.scala
src/Pure/System/options.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/symbols_dockable.scala
     1.1 --- a/src/Pure/System/build.scala	Sun Nov 25 21:10:29 2012 +0100
     1.2 +++ b/src/Pure/System/build.scala	Sun Nov 25 21:23:20 2012 +0100
     1.3 @@ -472,7 +472,7 @@
     1.4      def is_finished: Boolean = result.is_finished
     1.5  
     1.6      @volatile private var timeout = false
     1.7 -    private val time = Time.seconds(info.options.real("timeout"))
     1.8 +    private val time = info.options.seconds("timeout")
     1.9      private val timer: Option[Timer] =
    1.10        if (time.seconds > 0.0) {
    1.11          val t = new Timer("build", true)
     2.1 --- a/src/Pure/System/options.scala	Sun Nov 25 21:10:29 2012 +0100
     2.2 +++ b/src/Pure/System/options.scala	Sun Nov 25 21:23:20 2012 +0100
     2.3 @@ -229,6 +229,12 @@
     2.4    }
     2.5    val string = new String_Access
     2.6  
     2.7 +  class Seconds_Access
     2.8 +  {
     2.9 +    def apply(name: String): Time = Time.seconds(real(name))
    2.10 +  }
    2.11 +  val seconds = new Seconds_Access
    2.12 +
    2.13  
    2.14    /* external updates */
    2.15  
    2.16 @@ -410,5 +416,11 @@
    2.17      }
    2.18    }
    2.19    val string = new String_Access
    2.20 +
    2.21 +  class Seconds_Access
    2.22 +  {
    2.23 +    def apply(name: String): Time = options.seconds(name)
    2.24 +  }
    2.25 +  val seconds = new Seconds_Access
    2.26  }
    2.27  
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 25 21:10:29 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 25 21:23:20 2012 +0100
     3.3 @@ -115,7 +115,7 @@
     3.4      }
     3.5  
     3.6      private val delay_flush =
     3.7 -      Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) { flush() }
     3.8 +      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
     3.9  
    3.10      def +=(edit: Text.Edit)
    3.11      {
     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 21:10:29 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 21:23:20 2012 +0100
     4.3 @@ -147,7 +147,7 @@
     4.4    /* caret handling */
     4.5  
     4.6    private val delay_caret_update =
     4.7 -    Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
     4.8 +    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
     4.9        session.caret_focus.event(Session.Caret_Focus)
    4.10      }
    4.11  
    4.12 @@ -161,7 +161,7 @@
    4.13    private object overview extends Text_Overview(this)
    4.14    {
    4.15      val delay_repaint =
    4.16 -      Swing_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay"))) { repaint() }
    4.17 +      Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
    4.18    }
    4.19  
    4.20  
    4.21 @@ -172,7 +172,7 @@
    4.22        react {
    4.23          case _: Session.Raw_Edits =>
    4.24            Swing_Thread.later {
    4.25 -            overview.delay_repaint.postpone(Time.seconds(PIDE.options.real("editor_input_delay")))
    4.26 +            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    4.27            }
    4.28  
    4.29          case changed: Session.Commands_Changed =>
     5.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 21:23:20 2012 +0100
     5.3 @@ -115,8 +115,7 @@
     5.4    /* resize */
     5.5  
     5.6    private val delay_resize =
     5.7 -    Swing_Thread.delay_first(
     5.8 -      Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
     5.9 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    5.10  
    5.11    addComponentListener(new ComponentAdapter {
    5.12      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     6.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 21:23:20 2012 +0100
     6.3 @@ -136,8 +136,7 @@
     6.4    /* resize */
     6.5  
     6.6    private val delay_resize =
     6.7 -    Swing_Thread.delay_first(
     6.8 -      Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
     6.9 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    6.10  
    6.11    addComponentListener(new ComponentAdapter {
    6.12      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:10:29 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:23:20 2012 +0100
     7.3 @@ -141,7 +141,7 @@
     7.4    /* theory files */
     7.5  
     7.6    private lazy val delay_load =
     7.7 -    Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_load_delay")))
     7.8 +    Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
     7.9      {
    7.10        val view = jEdit.getActiveView()
    7.11  
    7.12 @@ -286,7 +286,7 @@
    7.13        val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
    7.14  
    7.15        PIDE.session = new Session(thy_load) {
    7.16 -        override def output_delay = Time.seconds(PIDE.options.real("editor_output_delay"))
    7.17 +        override def output_delay = PIDE.options.seconds("editor_output_delay")
    7.18          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
    7.19        }
    7.20  
     8.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 21:10:29 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 21:23:20 2012 +0100
     8.3 @@ -71,7 +71,7 @@
     8.4        add(results_panel, BorderPanel.Position.Center)
     8.5        listenTo(search)
     8.6        val delay_search =
     8.7 -        Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
     8.8 +        Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
     8.9            val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
    8.10            results_panel.contents.clear
    8.11            val results =