Quelle channel.scala Sprache: Scala

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

Channel with JSON RPC protocol.
*/

package isabelle.vscode

import isabelle._

import java.io.{InputStream, OutputStream}

import scala.collection.mutable

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

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

  private def read_line(): String =
    Byte_Message.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.nonEmpty }) header += line
    header.toList
  }

  private def read_content(n: Int): String = {
    val bytes = Bytes.read_stream(in, limit = n)
    if (bytes.size == n) bytes.text
    else error("Bad message content (unexpected EOF after " + bytes.size + " 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)
            LSP.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): Unit = {
    val content = JSON.Format.bytes(json)
    val n = content.size
    val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n")

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

  /* display message */

  def display_message(message_type: Int, msg: String, show: Boolean): Unit =
    write(LSP.DisplayMessage(message_type, Output.writeln_text(msg), show))

  def error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, true)
  def warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, true)
  def writeln(msg: String): Unit = display_message(LSP.MessageType.Info, msg, true)

  def log_error_message(msg: String): Unit = display_message(LSP.MessageType.Error, msg, false)
  def log_warning(msg: String): Unit = display_message(LSP.MessageType.Warning, msg, false)
  def log_writeln(msg: String): Unit = display_message(LSP.MessageType.Info, msg, false)

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

  /* progress */

  def progress(verbose: Boolean = false): Progress = {
    val progress_verbose = verbose
    new Progress with Progress.Status {
      override val verbose: Boolean = progress_verbose
      override def status_output(msgs: Progress.Output): Unit =
        for (msg <- msgs if do_output(msg)) {
          val message = msg.message
          message.kind match {
            case Progress.Kind.writeln => log_writeln(message.text)
            case Progress.Kind.warning => log_warning(message.text)
            case Progress.Kind.error_message => log_error_message(message.text)
          }
        }
    }
  }
}

quality99%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.