src/Tools/VSCode/src/channel.scala
changeset 65922 d2f19f05c0e9
parent 65829 07e86b942a84
child 67805 2d9a265b294e
     1.1 --- a/src/Tools/VSCode/src/channel.scala	Thu May 25 17:32:35 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/channel.scala	Thu May 25 18:07:29 2017 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  import scala.collection.mutable
     1.5  
     1.6  
     1.7 -class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger)
     1.8 +class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false)
     1.9  {
    1.10    /* read message */
    1.11  
    1.12 @@ -59,8 +59,9 @@
    1.13          s match {
    1.14            case Value.Int(n) if n >= 0 =>
    1.15              val msg = read_content(n)
    1.16 -            log("IN: " + n + "\n" + msg)
    1.17 -            Some(JSON.parse(msg))
    1.18 +            val json = JSON.parse(msg)
    1.19 +            Protocol.Message.log("IN: " + n, json, log, verbose)
    1.20 +            Some(json)
    1.21            case _ => error("Bad Content-Length: " + s)
    1.22          }
    1.23        case header => error(cat_lines("Malformed header:" :: header))
    1.24 @@ -77,7 +78,7 @@
    1.25      val n = content.length
    1.26      val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n")
    1.27  
    1.28 -    log("OUT: " + n + "\n" + msg)
    1.29 +    Protocol.Message.log("OUT: " + n, json, log, verbose)
    1.30      out.synchronized {
    1.31        out.write(header)
    1.32        out.write(content)