src/Tools/VSCode/src/channel.scala

more uniform Bytes.read_line/read_block operations;

/*  Title:      Tools/VSCode/src/channel.scala
    Author:     Makarius

Channel with JSON RPC protocol.
*/

package isabelle.vscode


import isabelle._

import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream, File => JFile}

import scala.collection.mutable


class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false)
{
  /* read message */

  private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r

  private def read_line(): String =
    Bytes.read_line(in) match {
      case Some(bytes) => bytes.text
      case None => ""
    }

  private def read_header(): List[String] =
  {
    val header = new mutable.ListBuffer[String]
    var line = ""
    while ({ line = read_line(); line != "" }) header += line
    header.toList
  }

  private def read_content(n: Int): String =
  {
    val bytes = Bytes.read_stream(in, limit = n)
    if (bytes.length == n) bytes.text
    else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)")
  }

  def read(): Option[JSON.T] =
  {
    read_header() match {
      case Nil => None
      case Content_Length(s) :: _ =>
        s match {
          case Value.Int(n) if n >= 0 =>
            val msg = read_content(n)
            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))
    }
  }


  /* write message */

  def write(json: JSON.T)
  {
    val msg = JSON.Format(json)
    val content = UTF8.bytes(msg)
    val n = content.length
    val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n")

    Protocol.Message.log("OUT: " + n, json, log, verbose)
    out.synchronized {
      out.write(header)
      out.write(content)
      out.flush
    }
  }


  /* display message */

  def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))

  def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
  def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
  def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }

  def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
  def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
  def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }

  object Error_Logger extends Logger
  {
    def apply(msg: => String) { log_error_message(msg) }
  }


  /* progress */

  def make_progress(verbose: Boolean = false): Progress =
    new Progress {
      override def echo(msg: String): Unit = log_writeln(msg)
      override def echo_warning(msg: String): Unit = log_warning(msg)
      override def echo_error_message(msg: String): Unit = log_error_message(msg)
      override def theory(session: String, theory: String): Unit =
        if (verbose) echo(session + ": theory " + theory)
    }
}