# HG changeset patch
# User wenzelm
# Date 1483653479 -3600
# Node ID 05b29c8f0addbf7ad7b00c5b7810ffab8a35e920
# Parent  a0e1f64be67cb1f1b5e3bc0787d8975bfc9eeda7
more informative error for spurious crash;

diff -r a0e1f64be67c -r 05b29c8f0add src/Pure/Concurrent/standard_thread.scala
--- a/src/Pure/Concurrent/standard_thread.scala	Thu Jan 05 22:38:06 2017 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala	Thu Jan 05 22:57:59 2017 +0100
@@ -50,7 +50,8 @@
 
   /* delayed events */
 
-  final class Delay private[Standard_Thread](first: Boolean, delay: => Time, event: => Unit)
+  final class Delay private[Standard_Thread](
+    first: Boolean, delay: => Time, log: Logger, event: => Unit)
   {
     private var running: Option[Event_Timer.Request] = None
 
@@ -59,7 +60,10 @@
       val do_run = synchronized {
         if (running.isDefined) { running = None; true } else false
       }
-      if (do_run) event
+      if (do_run) {
+        try { event }
+        catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
+      }
     }
 
     def invoke(): Unit = synchronized
@@ -95,8 +99,10 @@
   }
 
   // delayed event after first invocation
-  def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event)
+  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)(event: => Unit): Delay = new Delay(false, delay, event)
+  def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
+    new Delay(false, delay, log, event)
 }
diff -r a0e1f64be67c -r 05b29c8f0add src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Thu Jan 05 22:38:06 2017 +0100
+++ b/src/Tools/VSCode/src/channel.scala	Thu Jan 05 22:57:59 2017 +0100
@@ -98,6 +98,11 @@
   def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
   def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
 
+  object Error_Logger extends Logger
+  {
+    def apply(msg: => String) { log_error_message(msg) }
+  }
+
 
   /* progress */
 
diff -r a0e1f64be67c -r 05b29c8f0add src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Jan 05 22:38:06 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Jan 05 22:57:59 2017 +0100
@@ -111,11 +111,11 @@
   /* input from client or file-system */
 
   private val delay_input: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
+    Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     { resources.flush_input(session) }
 
   private val delay_load: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_load_delay")) {
+    Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
       val (invoke_input, invoke_load) = resources.resolve_dependencies(session, watcher)
       if (invoke_input) delay_input.invoke()
       if (invoke_load) delay_load.invoke
@@ -147,7 +147,7 @@
   /* output to client */
 
   private val delay_output: Standard_Thread.Delay =
-    Standard_Thread.delay_last(options.seconds("vscode_output_delay"))
+    Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
       if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke()
       else resources.flush_output(channel)