# 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) {