--- 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()
}