# HG changeset patch # User wenzelm # Date 1347383979 -7200 # Node ID 2c9272cb456866c490a019446f6d661620b245e8 # Parent 97f8cb455691cfa942e0c74bd7ecaba16443702f more options; diff -r 97f8cb455691 -r 2c9272cb4568 etc/options --- a/etc/options Tue Sep 11 16:10:54 2012 +0200 +++ b/etc/options Tue Sep 11 19:19:39 2012 +0200 @@ -80,3 +80,18 @@ option timeout : real = 0 -- "timeout for session build job (seconds > 0)" + +section {* Editor session parameters *} + +option editor_load_delay : real = 0.5 + -- "delay for file load operations (new buffers etc.)" + +option editor_input_delay : real = 0.3 + -- "delay for user input (text edits, cursor movement etc.)" + +option editor_output_delay : real = 0.1 + -- "delay for prover output (markup, common messages etc.)" + +option editor_update_delay : real = 0.5 + -- "delay for physical GUI updates" + diff -r 97f8cb455691 -r 2c9272cb4568 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Pure/System/session.scala Tue Sep 11 19:19:39 2012 +0200 @@ -46,15 +46,14 @@ @volatile var verbose: Boolean = false - /* tuning parameters */ // FIXME properties or settings (!?) + /* tuning parameters */ + + def output_delay: Time = Time.seconds(0.1) // prover output (markup, common messages) - val message_delay = Time.seconds(0.01) // prover messages - val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement) - val output_delay = Time.seconds(0.1) // prover output (markup, common messages) - val update_delay = Time.seconds(0.5) // GUI layout updates - val prune_delay = Time.seconds(60.0) // prune history -- delete old versions - val prune_size = 0 // size of retained history - val syslog_limit = 100 + private val message_delay = Time.seconds(0.01) // incoming prover messages + private val prune_delay = Time.seconds(60.0) // prune history -- delete old versions + private val prune_size = 0 // size of retained history + private val syslog_limit = 100 /* pervasive event buses */ diff -r 97f8cb455691 -r 2c9272cb4568 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Tools/jEdit/etc/options Tue Sep 11 19:19:39 2012 +0200 @@ -17,9 +17,3 @@ option jedit_tooltip_dismiss_delay : real = 8.0 -- "global delay for Swing tooltips" - - -section {* Reactivity *} - -option jedit_load_delay : real = 0.5 - -- "delay for file load operations (new buffers etc.)" diff -r 97f8cb455691 -r 2c9272cb4568 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Tue Sep 11 19:19:39 2012 +0200 @@ -115,7 +115,8 @@ } private val delay_flush = - Swing_Thread.delay_last(session.input_delay) { flush() } + Swing_Thread.delay_last( + Time.seconds(Isabelle.options.real("editor_input_delay"))) { flush() } def +=(edit: Text.Edit) { diff -r 97f8cb455691 -r 2c9272cb4568 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Tue Sep 11 19:19:39 2012 +0200 @@ -341,7 +341,7 @@ } private val delay_caret_update = - Swing_Thread.delay_last(session.input_delay) { + Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) { session.caret_focus.event(Session.Caret_Focus) } @@ -355,7 +355,8 @@ private object overview extends Text_Overview(this) { val delay_repaint = - Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() } + Swing_Thread.delay_first( + Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() } } @@ -366,7 +367,8 @@ react { case _: Session.Raw_Edits => Swing_Thread.later { - overview.delay_repaint.postpone(Isabelle.session.input_delay) + overview.delay_repaint.postpone( + Time.seconds(Isabelle.options.real("editor_input_delay"))) } case changed: Session.Commands_Changed => diff -r 97f8cb455691 -r 2c9272cb4568 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 19:19:39 2012 +0200 @@ -17,7 +17,8 @@ // FIXME avoid hard-wired stuff private val relevant_options = Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size", - "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "jedit_load_delay") + "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay", + "editor_input_delay", "editor_output_delay", "editor_update_delay") relevant_options.foreach(Isabelle.options.value.check_name _) diff -r 97f8cb455691 -r 2c9272cb4568 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Tue Sep 11 19:19:39 2012 +0200 @@ -148,7 +148,8 @@ /* resize */ private val delay_resize = - Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() } + Swing_Thread.delay_first( + Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 97f8cb455691 -r 2c9272cb4568 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Sep 11 16:10:54 2012 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Sep 11 19:19:39 2012 +0200 @@ -260,7 +260,7 @@ /* theory files */ private lazy val delay_load = - Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("jedit_load_delay"))) + Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_load_delay"))) { val view = jEdit.getActiveView() @@ -406,7 +406,9 @@ val content = Isabelle_Logic.session_content(false) val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax) - Isabelle.session = new Session(thy_load) + Isabelle.session = new Session(thy_load) { + override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay")) + } Isabelle.session.phase_changed += session_manager Isabelle.startup_failure = None