--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/delay.scala Mon Apr 06 12:53:45 2020 +0200
@@ -0,0 +1,66 @@
+/* Title: Pure/Concurrent/delay.scala
+ Author: Makarius
+
+Delayed events.
+*/
+
+package isabelle
+
+
+object Delay
+{
+ // delayed event after first invocation
+ def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+ new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event )
+
+ // delayed event after last invocation
+ def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay =
+ new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event )
+}
+
+final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit)
+{
+ private var running: Option[Event_Timer.Request] = None
+
+ private def run: Unit =
+ {
+ val do_run = synchronized {
+ if (running.isDefined) { running = None; true } else false
+ }
+ if (do_run) {
+ try { event }
+ catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
+ }
+ }
+
+ def invoke(): Unit = synchronized
+ {
+ val new_run =
+ running match {
+ case Some(request) => if (first) false else { request.cancel; true }
+ case None => true
+ }
+ if (new_run)
+ running = Some(Event_Timer.request(Time.now() + delay)(run))
+ }
+
+ def revoke(): Unit = synchronized
+ {
+ running match {
+ case Some(request) => request.cancel; running = None
+ case None =>
+ }
+ }
+
+ def postpone(alt_delay: Time): Unit = synchronized
+ {
+ running match {
+ case Some(request) =>
+ val alt_time = Time.now() + alt_delay
+ if (request.time < alt_time && request.cancel) {
+ running = Some(Event_Timer.request(alt_time)(run))
+ }
+ case None =>
+ }
+ }
+}
--- a/src/Pure/Concurrent/isabelle_thread.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala Mon Apr 06 12:53:45 2020 +0200
@@ -95,65 +95,6 @@
def uninterruptible[A](body: => A): A =
interrupt_handler(Interrupt_Handler.uninterruptible)(body)
-
-
- /* delayed events */
-
- final class Delay private[Isabelle_Thread](
- first: Boolean, delay: => Time, log: Logger, event: => Unit)
- {
- private var running: Option[Event_Timer.Request] = None
-
- private def run: Unit =
- {
- val do_run = synchronized {
- if (running.isDefined) { running = None; true } else false
- }
- if (do_run) {
- try { event }
- catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
- }
- }
-
- def invoke(): Unit = synchronized
- {
- val new_run =
- running match {
- case Some(request) => if (first) false else { request.cancel; true }
- case None => true
- }
- if (new_run)
- running = Some(Event_Timer.request(Time.now() + delay)(run))
- }
-
- def revoke(): Unit = synchronized
- {
- running match {
- case Some(request) => request.cancel; running = None
- case None =>
- }
- }
-
- def postpone(alt_delay: Time): Unit = synchronized
- {
- running match {
- case Some(request) =>
- val alt_time = Time.now() + alt_delay
- if (request.time < alt_time && request.cancel) {
- running = Some(Event_Timer.request(alt_time)(run))
- }
- case None =>
- }
- }
- }
-
- // delayed event after first invocation
- def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
- new Delay(true, delay, log, event)
-
- // delayed event after last invocation
- def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
- new Delay(false, delay, log, event)
}
class Isabelle_Thread private(
--- a/src/Pure/GUI/gui_thread.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala Mon Apr 06 12:53:45 2020 +0200
@@ -54,13 +54,4 @@
promise
}
}
-
-
- /* delayed events */
-
- def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
- Isabelle_Thread.delay_first(delay) { later { event } }
-
- def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(delay) { later { event } }
}
--- a/src/Pure/General/file_watcher.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/General/file_watcher.scala Mon Apr 06 12:53:45 2020 +0200
@@ -84,7 +84,7 @@
/* changed directory entries */
- private val delay_changed = Isabelle_Thread.delay_last(delay)
+ private val delay_changed = Delay.last(delay)
{
val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
handle(changed)
--- a/src/Pure/PIDE/headless.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/PIDE/headless.scala Mon Apr 06 12:53:45 2020 +0200
@@ -304,12 +304,12 @@
val consumer =
{
val delay_nodes_status =
- Isabelle_Thread.delay_first(nodes_status_delay max Time.zero) {
+ Delay.first(nodes_status_delay max Time.zero) {
progress.nodes_status(use_theories_state.value.nodes_status)
}
val delay_commit_clean =
- Isabelle_Thread.delay_first(commit_cleanup_delay max Time.zero) {
+ Delay.first(commit_cleanup_delay max Time.zero) {
val clean_theories = use_theories_state.change_result(_.clean_theories)
if (clean_theories.nonEmpty) {
progress.echo("Removing " + clean_theories.length + " theories ...")
--- a/src/Pure/PIDE/session.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/PIDE/session.scala Mon Apr 06 12:53:45 2020 +0200
@@ -268,7 +268,7 @@
nodes = Set.empty
commands = Set.empty
}
- private val delay_flush = Isabelle_Thread.delay_first(output_delay) { flush() }
+ private val delay_flush = Delay.first(output_delay) { flush() }
def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
synchronized {
@@ -313,7 +313,7 @@
private object consolidation
{
private val delay =
- Isabelle_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+ Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
private val state = Synchronized(init_state)
@@ -382,7 +382,7 @@
/* manager thread */
private val delay_prune =
- Isabelle_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+ Delay.first(prune_delay) { manager.send(Prune_History) }
private val manager: Consumer_Thread[Any] =
{
--- a/src/Pure/Tools/debugger.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/Tools/debugger.scala Mon Apr 06 12:53:45 2020 +0200
@@ -155,7 +155,7 @@
private val state = Synchronized(Debugger.State())
private val delay_update =
- Isabelle_Thread.delay_first(session.output_delay) {
+ Delay.first(session.output_delay) {
session.debugger_updates.post(Debugger.Update)
}
--- a/src/Pure/build-jars Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Pure/build-jars Mon Apr 06 12:53:45 2020 +0200
@@ -28,6 +28,7 @@
src/Pure/Admin/other_isabelle.scala
src/Pure/Concurrent/consumer_thread.scala
src/Pure/Concurrent/counter.scala
+ src/Pure/Concurrent/delay.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/isabelle_thread.scala
--- a/src/Tools/Graphview/tree_panel.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Mon Apr 06 12:53:45 2020 +0200
@@ -112,7 +112,7 @@
private val selection_field_foreground = selection_field.foreground
private val selection_delay =
- GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) {
+ Delay.last(graphview.options.seconds("editor_input_delay"), gui = true) {
val (pattern, ok) =
selection_field.text match {
case null | "" => (None, true)
--- a/src/Tools/VSCode/src/server.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala Mon Apr 06 12:53:45 2020 +0200
@@ -127,12 +127,12 @@
/* input from client or file-system */
- private val delay_input: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+ private val delay_input: Delay =
+ Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ resources.flush_input(session, channel) }
- private val delay_load: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
+ private val delay_load: Delay =
+ Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
val (invoke_input, invoke_load) =
resources.resolve_dependencies(session, editor, file_watcher)
if (invoke_input) delay_input.invoke()
@@ -183,8 +183,8 @@
/* caret handling */
- private val delay_caret_update: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+ private val delay_caret_update: Delay =
+ Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ session.caret_focus.post(Session.Caret_Focus) }
private def update_caret(caret: Option[(JFile, Line.Position)])
@@ -199,8 +199,8 @@
private lazy val preview_panel = new Preview_Panel(resources)
- private lazy val delay_preview: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+ private lazy val delay_preview: Delay =
+ Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (preview_panel.flush(channel)) delay_preview.invoke()
}
@@ -214,8 +214,8 @@
/* output to client */
- private val delay_output: Isabelle_Thread.Delay =
- Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+ private val delay_output: Delay =
+ Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (resources.flush_output(channel)) delay_output.invoke()
}
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Apr 06 12:53:45 2020 +0200
@@ -373,7 +373,7 @@
}
private val input_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
action()
}
@@ -530,7 +530,7 @@
}
private val process_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) {
action()
}
--- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -362,7 +362,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/document_view.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Apr 06 12:53:45 2020 +0200
@@ -184,7 +184,7 @@
/* caret handling */
private val delay_caret_update =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
session.caret_focus.post(Session.Caret_Focus)
JEdit_Lib.invalidate(text_area)
}
--- a/src/Tools/jEdit/src/font_info.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/font_info.scala Mon Apr 06 12:53:45 2020 +0200
@@ -56,7 +56,7 @@
// owned by GUI thread
private var steps = 0
- private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+ private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
{
change_size(size =>
{
--- a/src/Tools/jEdit/src/info_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -80,7 +80,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Apr 06 12:53:45 2020 +0200
@@ -32,10 +32,10 @@
def purge() { flush_edits(purge = true) }
private val delay1_flush =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
private val delay2_flush =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() }
+ Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
def invoke(): Unit = delay1_flush.invoke()
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
--- a/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -59,10 +59,10 @@
}
private val input_delay =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart }
+ Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart }
private val update_delay =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart }
+ Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart }
/* controls */
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -151,7 +151,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/plugin.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Apr 06 12:53:45 2020 +0200
@@ -107,7 +107,7 @@
/* theory files */
lazy val delay_init =
- GUI_Thread.delay_last(options.seconds("editor_load_delay"))
+ Delay.last(options.seconds("editor_load_delay"), gui = true)
{
init_models()
}
@@ -178,7 +178,7 @@
}
private lazy val delay_load =
- GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() }
+ Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() }
private def file_watcher_action(changed: Set[JFile]): Unit =
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Apr 06 12:53:45 2020 +0200
@@ -191,7 +191,7 @@
Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
{
private val input_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
search_action(this)
}
getDocument.addDocumentListener(new DocumentListener {
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Apr 06 12:53:45 2020 +0200
@@ -77,7 +77,7 @@
private var active = true
private val pending_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
pending match {
case Some(body) => pending = None; body()
case None =>
@@ -99,7 +99,7 @@
}
private lazy val reactivate_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) {
+ Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
active = true
}
@@ -113,7 +113,7 @@
/* dismiss */
- private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
+ private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
{
dismiss_unfocused()
}
--- a/src/Tools/jEdit/src/query_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -320,7 +320,7 @@
}
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/session_build.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Mon Apr 06 12:53:45 2020 +0200
@@ -102,7 +102,7 @@
}
private val delay_exit =
- GUI_Thread.delay_first(Time.seconds(1.0))
+ Delay.first(Time.seconds(1.0), gui = true)
{
if (can_auto_close) conclude()
else {
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -144,7 +144,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Apr 06 12:53:45 2020 +0200
@@ -182,7 +182,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
peer.addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -58,7 +58,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -40,7 +40,7 @@
/* resize */
private val delay_resize =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/symbols_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -28,7 +28,7 @@
private val abbrevs_panel = new Abbrevs_Panel
private val abbrevs_refresh_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
+ Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh }
private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
{
@@ -129,7 +129,7 @@
val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
val search_delay =
- GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+ Delay.last(PIDE.options.seconds("editor_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 =
--- a/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 06 12:53:45 2020 +0200
@@ -21,7 +21,7 @@
private val syslog = new TextArea()
- private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay"))
+ 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
--- a/src/Tools/jEdit/src/text_overview.scala Mon Apr 06 12:36:00 2020 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Mon Apr 06 12:53:45 2020 +0200
@@ -75,7 +75,7 @@
private var current_overview = Overview()
private val delay_repaint =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() }
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() }
override def paintComponent(gfx: Graphics)
{
@@ -116,7 +116,7 @@
def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) }
private val delay_refresh =
- GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) {
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) {
if (!doc_view.rich_text_area.check_robust_body) invoke()
else {
JEdit_Lib.buffer_lock(buffer) {