# HG changeset patch
# User wenzelm
# Date 1495728449 -7200
# Node ID d2f19f05c0e956c65c8d213a6af03dcb491b6817
# Parent  5b42937d3b2d852aa5a6cbf8b0229198df89a1ac
clarified message logging;

diff -r 5b42937d3b2d -r d2f19f05c0e9 src/Tools/VSCode/src/channel.scala
--- a/src/Tools/VSCode/src/channel.scala	Thu May 25 17:32:35 2017 +0200
+++ b/src/Tools/VSCode/src/channel.scala	Thu May 25 18:07:29 2017 +0200
@@ -14,7 +14,7 @@
 import scala.collection.mutable
 
 
-class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger)
+class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false)
 {
   /* read message */
 
@@ -59,8 +59,9 @@
         s match {
           case Value.Int(n) if n >= 0 =>
             val msg = read_content(n)
-            log("IN: " + n + "\n" + msg)
-            Some(JSON.parse(msg))
+            val json = JSON.parse(msg)
+            Protocol.Message.log("IN: " + n, json, log, verbose)
+            Some(json)
           case _ => error("Bad Content-Length: " + s)
         }
       case header => error(cat_lines("Malformed header:" :: header))
@@ -77,7 +78,7 @@
     val n = content.length
     val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n")
 
-    log("OUT: " + n + "\n" + msg)
+    Protocol.Message.log("OUT: " + n, json, log, verbose)
     out.synchronized {
       out.write(header)
       out.write(content)
diff -r 5b42937d3b2d -r d2f19f05c0e9 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Thu May 25 17:32:35 2017 +0200
+++ b/src/Tools/VSCode/src/protocol.scala	Thu May 25 18:07:29 2017 +0200
@@ -20,6 +20,22 @@
   object Message
   {
     val empty: Map[String, JSON.T] = Map("jsonrpc" -> "2.0")
+
+    def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean)
+    {
+      val header: Map[String, Any] =
+        json match {
+          case obj: Map[Any, Any] =>
+            (obj.get("method"), obj.get("id")) match {
+              case (Some(method), Some(id)) => Map("method" -> method, "id" -> id)
+              case (Some(method), None) => Map("method" -> method)
+              case _ => Map.empty
+            }
+          case _ => Map.empty
+        }
+      if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))
+      else logger(prefix + " " + JSON.Format(header))
+    }
   }
 
 
diff -r 5b42937d3b2d -r d2f19f05c0e9 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu May 25 17:32:35 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Thu May 25 18:07:29 2017 +0200
@@ -34,6 +34,7 @@
       var modes: List[String] = Nil
       var options = Options.init()
       var system_mode = false
+      var verbose = false
 
       val getopts = Getopts("""
 Usage: isabelle vscode_server [OPTIONS]
@@ -45,6 +46,7 @@
     -m MODE      add print mode for output
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -s           system build mode for session image
+    -v           verbose logging
 
   Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
 """,
@@ -53,13 +55,14 @@
         "l:" -> (arg => logic = arg),
         "m:" -> (arg => modes = arg :: modes),
         "o:" -> (arg => options = options + arg),
-        "s" -> (_ => system_mode = true))
+        "s" -> (_ => system_mode = true),
+        "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val log = Logger.make(log_file)
-      val channel = new Channel(System.in, System.out, log)
+      val channel = new Channel(System.in, System.out, log, verbose)
       val server = new Server(channel, options, logic, dirs, modes, system_mode, log)
 
       // prevent spurious garbage on the main protocol channel