clarified protocol errors;
authorwenzelm
Wed Dec 28 17:54:55 2016 +0100 (2016-12-28)
changeset 6468704806ad1e43a
parent 64686 7888be4fa496
child 64688 d8f194556c70
clarified protocol errors;
src/Tools/VSCode/src/server.scala
     1.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:49:47 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 28 17:54:55 2016 +0100
     1.3 @@ -308,7 +308,7 @@
     1.4            case _ => channel.log("### IGNORED")
     1.5          }
     1.6        }
     1.7 -      catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
     1.8 +      catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
     1.9      }
    1.10  
    1.11      @tailrec def loop()