more options;
authorwenzelm
Tue Sep 11 19:19:39 2012 +0200 (2012-09-11)
changeset 492882c9272cb4568
parent 49272 97f8cb455691
child 49289 60424f123621
more options;
etc/options
src/Pure/System/session.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/etc/options	Tue Sep 11 16:10:54 2012 +0200
     1.2 +++ b/etc/options	Tue Sep 11 19:19:39 2012 +0200
     1.3 @@ -80,3 +80,18 @@
     1.4  option timeout : real = 0
     1.5    -- "timeout for session build job (seconds > 0)"
     1.6  
     1.7 +
     1.8 +section {* Editor session parameters *}
     1.9 +
    1.10 +option editor_load_delay : real = 0.5
    1.11 +  -- "delay for file load operations (new buffers etc.)"
    1.12 +
    1.13 +option editor_input_delay : real = 0.3
    1.14 +  -- "delay for user input (text edits, cursor movement etc.)"
    1.15 +
    1.16 +option editor_output_delay : real = 0.1
    1.17 +  -- "delay for prover output (markup, common messages etc.)"
    1.18 +
    1.19 +option editor_update_delay : real = 0.5
    1.20 +  -- "delay for physical GUI updates"
    1.21 +
     2.1 --- a/src/Pure/System/session.scala	Tue Sep 11 16:10:54 2012 +0200
     2.2 +++ b/src/Pure/System/session.scala	Tue Sep 11 19:19:39 2012 +0200
     2.3 @@ -46,15 +46,14 @@
     2.4    @volatile var verbose: Boolean = false
     2.5  
     2.6  
     2.7 -  /* tuning parameters */  // FIXME properties or settings (!?)
     2.8 +  /* tuning parameters */
     2.9 +
    2.10 +  def output_delay: Time = Time.seconds(0.1)  // prover output (markup, common messages)
    2.11  
    2.12 -  val message_delay = Time.seconds(0.01)  // prover messages
    2.13 -  val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
    2.14 -  val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
    2.15 -  val update_delay = Time.seconds(0.5)  // GUI layout updates
    2.16 -  val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
    2.17 -  val prune_size = 0  // size of retained history
    2.18 -  val syslog_limit = 100
    2.19 +  private val message_delay = Time.seconds(0.01)  // incoming prover messages
    2.20 +  private val prune_delay = Time.seconds(60.0)  // prune history -- delete old versions
    2.21 +  private val prune_size = 0  // size of retained history
    2.22 +  private val syslog_limit = 100
    2.23  
    2.24  
    2.25    /* pervasive event buses */
     3.1 --- a/src/Tools/jEdit/etc/options	Tue Sep 11 16:10:54 2012 +0200
     3.2 +++ b/src/Tools/jEdit/etc/options	Tue Sep 11 19:19:39 2012 +0200
     3.3 @@ -17,9 +17,3 @@
     3.4  
     3.5  option jedit_tooltip_dismiss_delay : real = 8.0
     3.6    -- "global delay for Swing tooltips"
     3.7 -
     3.8 -
     3.9 -section {* Reactivity *}
    3.10 -
    3.11 -option jedit_load_delay : real = 0.5
    3.12 -  -- "delay for file load operations (new buffers etc.)"
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Sep 11 16:10:54 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Sep 11 19:19:39 2012 +0200
     4.3 @@ -115,7 +115,8 @@
     4.4      }
     4.5  
     4.6      private val delay_flush =
     4.7 -      Swing_Thread.delay_last(session.input_delay) { flush() }
     4.8 +      Swing_Thread.delay_last(
     4.9 +        Time.seconds(Isabelle.options.real("editor_input_delay"))) { flush() }
    4.10  
    4.11      def +=(edit: Text.Edit)
    4.12      {
     5.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Sep 11 16:10:54 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Sep 11 19:19:39 2012 +0200
     5.3 @@ -341,7 +341,7 @@
     5.4    }
     5.5  
     5.6    private val delay_caret_update =
     5.7 -    Swing_Thread.delay_last(session.input_delay) {
     5.8 +    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
     5.9        session.caret_focus.event(Session.Caret_Focus)
    5.10      }
    5.11  
    5.12 @@ -355,7 +355,8 @@
    5.13    private object overview extends Text_Overview(this)
    5.14    {
    5.15      val delay_repaint =
    5.16 -      Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }
    5.17 +      Swing_Thread.delay_first(
    5.18 +        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
    5.19    }
    5.20  
    5.21  
    5.22 @@ -366,7 +367,8 @@
    5.23        react {
    5.24          case _: Session.Raw_Edits =>
    5.25            Swing_Thread.later {
    5.26 -            overview.delay_repaint.postpone(Isabelle.session.input_delay)
    5.27 +            overview.delay_repaint.postpone(
    5.28 +              Time.seconds(Isabelle.options.real("editor_input_delay")))
    5.29            }
    5.30  
    5.31          case changed: Session.Commands_Changed =>
     6.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 16:10:54 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Sep 11 19:19:39 2012 +0200
     6.3 @@ -17,7 +17,8 @@
     6.4    // FIXME avoid hard-wired stuff
     6.5    private val relevant_options =
     6.6      Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
     6.7 -      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay")
     6.8 +      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
     6.9 +      "editor_input_delay", "editor_output_delay", "editor_update_delay")
    6.10  
    6.11    relevant_options.foreach(Isabelle.options.value.check_name _)
    6.12  
     7.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 11 16:10:54 2012 +0200
     7.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Sep 11 19:19:39 2012 +0200
     7.3 @@ -148,7 +148,8 @@
     7.4    /* resize */
     7.5  
     7.6    private val delay_resize =
     7.7 -    Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
     7.8 +    Swing_Thread.delay_first(
     7.9 +      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
    7.10  
    7.11    addComponentListener(new ComponentAdapter {
    7.12      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     8.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 16:10:54 2012 +0200
     8.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Sep 11 19:19:39 2012 +0200
     8.3 @@ -260,7 +260,7 @@
     8.4    /* theory files */
     8.5  
     8.6    private lazy val delay_load =
     8.7 -    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("jedit_load_delay")))
     8.8 +    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_load_delay")))
     8.9      {
    8.10        val view = jEdit.getActiveView()
    8.11  
    8.12 @@ -406,7 +406,9 @@
    8.13  
    8.14        val content = Isabelle_Logic.session_content(false)
    8.15        val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
    8.16 -      Isabelle.session = new Session(thy_load)
    8.17 +      Isabelle.session = new Session(thy_load) {
    8.18 +        override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
    8.19 +      }
    8.20  
    8.21        Isabelle.session.phase_changed += session_manager
    8.22        Isabelle.startup_failure = None