src/Tools/VSCode/src/channel.scala
author wenzelm
Sun Sep 09 11:53:53 2018 +0200 (10 months ago)
changeset 68957 eef4e983fd9d
parent 68410 4e27f5c361d2
child 69448 51e696887b81
permissions -rw-r--r--
clarified theory progress;
wenzelm@64605
     1
/*  Title:      Tools/VSCode/src/channel.scala
wenzelm@64605
     2
    Author:     Makarius
wenzelm@64605
     3
wenzelm@64605
     4
Channel with JSON RPC protocol.
wenzelm@64605
     5
*/
wenzelm@64605
     6
wenzelm@64605
     7
package isabelle.vscode
wenzelm@64605
     8
wenzelm@64605
     9
wenzelm@64605
    10
import isabelle._
wenzelm@64605
    11
wenzelm@64777
    12
import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream, File => JFile}
wenzelm@64605
    13
wenzelm@64605
    14
import scala.collection.mutable
wenzelm@64605
    15
wenzelm@64605
    16
wenzelm@65922
    17
class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false)
wenzelm@64605
    18
{
wenzelm@64605
    19
  /* read message */
wenzelm@64605
    20
wenzelm@64605
    21
  private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
wenzelm@64605
    22
wenzelm@64605
    23
  private def read_line(): String =
wenzelm@67805
    24
    Bytes.read_line(in) match {
wenzelm@67805
    25
      case Some(bytes) => bytes.text
wenzelm@67805
    26
      case None => ""
wenzelm@67805
    27
    }
wenzelm@64605
    28
wenzelm@64605
    29
  private def read_header(): List[String] =
wenzelm@64605
    30
  {
wenzelm@64605
    31
    val header = new mutable.ListBuffer[String]
wenzelm@64605
    32
    var line = ""
wenzelm@64605
    33
    while ({ line = read_line(); line != "" }) header += line
wenzelm@64605
    34
    header.toList
wenzelm@64605
    35
  }
wenzelm@64605
    36
wenzelm@64605
    37
  private def read_content(n: Int): String =
wenzelm@64605
    38
  {
wenzelm@67805
    39
    val bytes = Bytes.read_stream(in, limit = n)
wenzelm@67805
    40
    if (bytes.length == n) bytes.text
wenzelm@67805
    41
    else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)")
wenzelm@64605
    42
  }
wenzelm@64605
    43
wenzelm@64605
    44
  def read(): Option[JSON.T] =
wenzelm@64605
    45
  {
wenzelm@64605
    46
    read_header() match {
wenzelm@64605
    47
      case Nil => None
wenzelm@64605
    48
      case Content_Length(s) :: _ =>
wenzelm@64605
    49
        s match {
wenzelm@64605
    50
          case Value.Int(n) if n >= 0 =>
wenzelm@64605
    51
            val msg = read_content(n)
wenzelm@65922
    52
            val json = JSON.parse(msg)
wenzelm@65922
    53
            Protocol.Message.log("IN: " + n, json, log, verbose)
wenzelm@65922
    54
            Some(json)
wenzelm@64605
    55
          case _ => error("Bad Content-Length: " + s)
wenzelm@64605
    56
        }
wenzelm@64605
    57
      case header => error(cat_lines("Malformed header:" :: header))
wenzelm@64605
    58
    }
wenzelm@64605
    59
  }
wenzelm@64605
    60
wenzelm@64605
    61
wenzelm@64605
    62
  /* write message */
wenzelm@64605
    63
wenzelm@64605
    64
  def write(json: JSON.T)
wenzelm@64605
    65
  {
wenzelm@64605
    66
    val msg = JSON.Format(json)
wenzelm@65152
    67
    val content = UTF8.bytes(msg)
wenzelm@65152
    68
    val n = content.length
wenzelm@65152
    69
    val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n")
wenzelm@64605
    70
wenzelm@65922
    71
    Protocol.Message.log("OUT: " + n, json, log, verbose)
wenzelm@64605
    72
    out.synchronized {
wenzelm@64605
    73
      out.write(header)
wenzelm@64605
    74
      out.write(content)
wenzelm@64605
    75
      out.flush
wenzelm@64605
    76
    }
wenzelm@64605
    77
  }
wenzelm@64642
    78
wenzelm@64642
    79
wenzelm@64642
    80
  /* display message */
wenzelm@64642
    81
wenzelm@64686
    82
  def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
wenzelm@64686
    83
    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
wenzelm@64642
    84
wenzelm@64686
    85
  def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
wenzelm@64686
    86
  def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
wenzelm@64686
    87
  def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
wenzelm@64686
    88
wenzelm@64686
    89
  def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
wenzelm@64686
    90
  def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
wenzelm@64686
    91
  def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
wenzelm@64675
    92
wenzelm@64810
    93
  object Error_Logger extends Logger
wenzelm@64810
    94
  {
wenzelm@64810
    95
    def apply(msg: => String) { log_error_message(msg) }
wenzelm@64810
    96
  }
wenzelm@64810
    97
wenzelm@64675
    98
wenzelm@64733
    99
  /* progress */
wenzelm@64733
   100
wenzelm@67856
   101
  def progress(verbose: Boolean = false): Progress =
wenzelm@64733
   102
    new Progress {
wenzelm@64733
   103
      override def echo(msg: String): Unit = log_writeln(msg)
wenzelm@65829
   104
      override def echo_warning(msg: String): Unit = log_warning(msg)
wenzelm@65829
   105
      override def echo_error_message(msg: String): Unit = log_error_message(msg)
wenzelm@68957
   106
      override def theory(theory: Progress.Theory): Unit = if (verbose) echo(theory.message)
wenzelm@64733
   107
    }
wenzelm@64605
   108
}