src/Tools/VSCode/src/server.scala

 
       if (!Build.build(options = options, build_heap = true, no_build = true,
             dirs = dirs, sessions = List(logic)).ok)
         error("Missing logic image " + quote(logic))
 
-      val channel = new Channel(System.in, System.out, log_file)
-      val server = new Server(channel, options, text_length, logic, dirs, modes)
+      val log = Logger.make(log_file)
+      val channel = new Channel(System.in, System.out, log)
+      val server = new Server(channel, options, text_length, logic, dirs, modes, log)
 
       // prevent spurious garbage on the main protocol channel
       val orig_out = System.out
       try {
         System.setOut(new PrintStream(new OutputStream { def write(n: Int) {} }))

       }
       finally { System.setOut(orig_out) }
     }
     catch {
       case exn: Throwable =>
-        val channel = new Channel(System.in, System.out, None)
+        val channel = new Channel(System.in, System.out, No_Logger)
         channel.error_message(Exn.message(exn))
         throw(exn)
     }
   })
 }

   channel: Channel,
   options: Options,
   text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
   session_name: String = Server.default_logic,
   session_dirs: List[Path] = Nil,
-  modes: List[String] = Nil)
+  modes: List[String] = Nil,
+  log: Logger = No_Logger)
 {
   /* server session */
 
   private val session_ = Synchronized(None: Option[Session])
   def session: Session = session_.value getOrElse error("Server inactive")

         None
     })
   }
 
   def exit() {
-    channel.log("\n")
+    log("\n")
     sys.exit(if (session_.value.isDefined) 1 else 0)
   }
 
 
   /* hover */

 
   /* main loop */
 
   def start()
   {
-    channel.log("Server started " + Date.now())
+    log("Server started " + Date.now())
 
     def handle(json: JSON.T)
     {
       try {
         json match {

             update_document(uri, text)
           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
             update_document(uri, text)
           case Protocol.DidCloseTextDocument(uri) =>
             close_document(uri)
-          case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
+          case Protocol.DidSaveTextDocument(uri) => log("SAVE " + uri)
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
-          case _ => channel.log("### IGNORED")
+          case _ => log("### IGNORED")
         }
       }
       catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
     }
 

           json match {
             case bulk: List[_] => bulk.foreach(handle(_))
             case _ => handle(json)
           }
           loop()
-        case None => channel.log("### TERMINATE")
+        case None => log("### TERMINATE")
       }
     }
     loop()
   }
 }