src/Tools/VSCode/src/server.scala
changeset 64717 d2b50eb3d9ab
parent 64710 72ca4e5f976e
child 64720 8cc2d7c4ada1
     1.1 --- a/src/Tools/VSCode/src/server.scala	Sat Dec 31 11:15:20 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Sat Dec 31 11:39:57 2016 +0100
     1.3 @@ -64,8 +64,9 @@
     1.4              dirs = dirs, sessions = List(logic)).ok)
     1.5          error("Missing logic image " + quote(logic))
     1.6  
     1.7 -      val channel = new Channel(System.in, System.out, log_file)
     1.8 -      val server = new Server(channel, options, text_length, logic, dirs, modes)
     1.9 +      val log = Logger.make(log_file)
    1.10 +      val channel = new Channel(System.in, System.out, log)
    1.11 +      val server = new Server(channel, options, text_length, logic, dirs, modes, log)
    1.12  
    1.13        // prevent spurious garbage on the main protocol channel
    1.14        val orig_out = System.out
    1.15 @@ -77,7 +78,7 @@
    1.16      }
    1.17      catch {
    1.18        case exn: Throwable =>
    1.19 -        val channel = new Channel(System.in, System.out, None)
    1.20 +        val channel = new Channel(System.in, System.out, No_Logger)
    1.21          channel.error_message(Exn.message(exn))
    1.22          throw(exn)
    1.23      }
    1.24 @@ -90,7 +91,8 @@
    1.25    text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
    1.26    session_name: String = Server.default_logic,
    1.27    session_dirs: List[Path] = Nil,
    1.28 -  modes: List[String] = Nil)
    1.29 +  modes: List[String] = Nil,
    1.30 +  log: Logger = No_Logger)
    1.31  {
    1.32    /* server session */
    1.33  
    1.34 @@ -251,7 +253,7 @@
    1.35    }
    1.36  
    1.37    def exit() {
    1.38 -    channel.log("\n")
    1.39 +    log("\n")
    1.40      sys.exit(if (session_.value.isDefined) 1 else 0)
    1.41    }
    1.42  
    1.43 @@ -289,7 +291,7 @@
    1.44  
    1.45    def start()
    1.46    {
    1.47 -    channel.log("Server started " + Date.now())
    1.48 +    log("Server started " + Date.now())
    1.49  
    1.50      def handle(json: JSON.T)
    1.51      {
    1.52 @@ -304,10 +306,10 @@
    1.53              update_document(uri, text)
    1.54            case Protocol.DidCloseTextDocument(uri) =>
    1.55              close_document(uri)
    1.56 -          case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
    1.57 +          case Protocol.DidSaveTextDocument(uri) => log("SAVE " + uri)
    1.58            case Protocol.Hover(id, node_pos) => hover(id, node_pos)
    1.59            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
    1.60 -          case _ => channel.log("### IGNORED")
    1.61 +          case _ => log("### IGNORED")
    1.62          }
    1.63        }
    1.64        catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
    1.65 @@ -322,7 +324,7 @@
    1.66              case _ => handle(json)
    1.67            }
    1.68            loop()
    1.69 -        case None => channel.log("### TERMINATE")
    1.70 +        case None => log("### TERMINATE")
    1.71        }
    1.72      }
    1.73      loop()