# HG changeset patch # User wenzelm # Date 1670535483 -3600 # Node ID 6e2383488a558f6dcc694b969c140a8511414bf7 # Parent cc9ddf373bd2b48113cab04dbc077e504b76182a clarified signature: proper scopes and types; diff -r cc9ddf373bd2 -r 6e2383488a55 src/Pure/PIDE/document_editor.scala --- a/src/Pure/PIDE/document_editor.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Pure/PIDE/document_editor.scala Thu Dec 08 22:38:03 2022 +0100 @@ -28,8 +28,7 @@ private val syslog = session.make_syslog() private def update(text: String = syslog.content()): Unit = show(text) - private val delay = - Delay.first(session.session_options.seconds("editor_update_delay"), gui = true) { update() } + private val delay = Delay.first(session.update_delay, gui = true) { update() } override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } diff -r cc9ddf373bd2 -r 6e2383488a55 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Pure/PIDE/session.scala Thu Dec 08 22:38:03 2022 +0100 @@ -139,10 +139,15 @@ def session_options: Options = _session_options + def load_delay: Time = session_options.seconds("editor_load_delay") + def input_delay: Time = session_options.seconds("editor_input_delay") + def generated_input_delay: Time = session_options.seconds("editor_generated_input_delay") def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") + def update_delay: Time = session_options.seconds("editor_update_delay") + def chart_delay: Time = session_options.seconds("editor_chart_delay") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -339,7 +339,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -85,7 +85,7 @@ private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) } private val delay_resize: Delay = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() @@ -163,7 +163,7 @@ /* controls */ private lazy val delay_load: Delay = - Delay.last(PIDE.options.seconds("editor_load_delay"), gui = true) { + Delay.last(PIDE.session.load_delay, gui = true) { val models = Document_Model.get_models() val thy_files = PIDE.resources.resolve_dependencies(models, Nil) } diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Thu Dec 08 22:38:03 2022 +0100 @@ -367,7 +367,7 @@ @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { - PIDE.options.seconds("editor_output_delay").sleep() + PIDE.session.output_delay.sleep() await_stable_snapshot() } else snapshot diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Thu Dec 08 22:38:03 2022 +0100 @@ -186,7 +186,7 @@ /* caret handling */ private val delay_caret_update = - Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { + Delay.last(PIDE.session.input_delay, gui = true) { session.caret_focus.post(Session.Caret_Focus) JEdit_Lib.invalidate(text_area) } diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/font_info.scala --- a/src/Tools/jEdit/src/font_info.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/font_info.scala Thu Dec 08 22:38:03 2022 +0100 @@ -53,7 +53,7 @@ // owned by GUI thread private var steps = 0 - private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { + private val delay = Delay.last(PIDE.session.input_delay, gui = true) { change_size { size => var i = size.round while (steps != 0 && i > 0) { diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/info_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -81,7 +81,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Thu Dec 08 22:38:03 2022 +0100 @@ -31,10 +31,10 @@ def purge(): Unit = flush_edits(purge = true) private val delay_input: Delay = - Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() } + Delay.last(PIDE.session.input_delay, gui = true) { flush() } private val delay_generated_input: Delay = - Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() } + Delay.first(PIDE.session.generated_input_delay, gui = true) { flush() } def invoke(): Unit = delay_input.invoke() def invoke_generated(): Unit = { delay_input.invoke(); delay_generated_input.invoke() } diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/main_plugin.scala Thu Dec 08 22:38:03 2022 +0100 @@ -101,9 +101,7 @@ /* theory files */ lazy val delay_init: Delay = - Delay.last(options.seconds("editor_load_delay"), gui = true) { - init_models() - } + Delay.last(PIDE.session.load_delay, gui = true) { init_models() } private val delay_load_active = Synchronized(false) private def delay_load_finished(): Unit = delay_load_active.change(_ => false) @@ -151,7 +149,7 @@ } private lazy val delay_load: Delay = - Delay.last(options.seconds("editor_load_delay"), gui = true) { + Delay.last(session.load_delay, gui = true) { if (JEdit_Options.continuous_checking()) { if (!PerspectiveManager.isPerspectiveEnabled || JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke() @@ -164,7 +162,7 @@ if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated() lazy val file_watcher: File_Watcher = - File_Watcher(file_watcher_action, options.seconds("editor_load_delay")) + File_Watcher(file_watcher_action, session.load_delay) /* session phase */ diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -56,10 +56,10 @@ } private val input_delay = - Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart() } + Delay.first(PIDE.session.input_delay, gui = true) { update_chart() } private val update_delay = - Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart() } + Delay.first(PIDE.session.chart_delay, gui = true) { update_chart() } /* controls */ diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -123,7 +123,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Dec 08 22:38:03 2022 +0100 @@ -159,9 +159,7 @@ val search_field: Component = Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") { private val input_delay = - Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { - search_action(this) - } + Delay.last(PIDE.session.input_delay, gui = true) { search_action(this) } getDocument.addDocumentListener(new DocumentListener { def changedUpdate(e: DocumentEvent): Unit = input_delay.invoke() def insertUpdate(e: DocumentEvent): Unit = input_delay.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Dec 08 22:38:03 2022 +0100 @@ -114,9 +114,7 @@ /* dismiss */ private lazy val focus_delay = - Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { - dismiss_unfocused() - } + Delay.last(PIDE.session.input_delay, gui = true) { dismiss_unfocused() } def dismiss_unfocused(): Unit = { stack.span(tip => !tip.pretty_text_area.isFocusOwner) match { diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/query_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -305,7 +305,7 @@ } private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -130,7 +130,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Thu Dec 08 22:38:03 2022 +0100 @@ -167,7 +167,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } peer.addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -54,7 +54,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -35,7 +35,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -26,7 +26,7 @@ private val abbrevs_panel = new Abbrevs_Panel private val abbrevs_refresh_delay = - Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh() } + Delay.last(PIDE.session.update_delay, gui = true) { abbrevs_panel.refresh() } private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button { def update_font(): Unit = { font = GUI.font(size = font_size) } @@ -124,7 +124,7 @@ for (entry <- Symbol.symbols.entries if entry.code.isDefined) yield entry.symbol -> Word.lowercase(entry.symbol) val search_delay: Delay = - Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { + Delay.last(PIDE.session.input_delay, gui = true) { val search_words = Word.explode(Word.lowercase(search_field.text)) val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 val results = diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/syslog_dockable.scala --- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Dec 08 22:38:03 2022 +0100 @@ -19,10 +19,11 @@ private val syslog = new TextArea() - private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { - val text = PIDE.session.syslog.content() - if (text != syslog.text) syslog.text = text - } + private def syslog_delay = + Delay.first(PIDE.session.update_delay, gui = true) { + val text = PIDE.session.syslog.content() + if (text != syslog.text) syslog.text = text + } set_content(new ScrollPane(syslog)) diff -r cc9ddf373bd2 -r 6e2383488a55 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Thu Dec 08 22:11:36 2022 +0100 +++ b/src/Tools/jEdit/src/text_overview.scala Thu Dec 08 22:38:03 2022 +0100 @@ -74,7 +74,7 @@ private var current_overview = Overview() private val delay_repaint = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() } + Delay.first(PIDE.session.update_delay, gui = true) { repaint() } override def paintComponent(gfx: Graphics): Unit = { super.paintComponent(gfx) @@ -114,7 +114,7 @@ def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change { x => x.cancel(); x } } private val delay_refresh = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { + Delay.first(PIDE.session.update_delay, gui = true) { if (!doc_view.rich_text_area.check_robust_body) invoke() else { JEdit_Lib.buffer_lock(buffer) {