src/Tools/VSCode/src/channel.scala
author wenzelm
Wed Dec 21 16:02:52 2016 +0100 (2016-12-21)
changeset 64642 c231206a84c8
parent 64605 9c1173a7e4cb
child 64658 fb42c780d903
permissions -rw-r--r--
display messages, according to regular Isabelle Output;
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@64605
    12
import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
wenzelm@64605
    13
wenzelm@64605
    14
import scala.collection.mutable
wenzelm@64605
    15
wenzelm@64605
    16
wenzelm@64605
    17
class Channel(in: InputStream, out: OutputStream, log_file: Option[Path] = None)
wenzelm@64605
    18
{
wenzelm@64605
    19
  val log: Logger = Logger.make(log_file)
wenzelm@64605
    20
wenzelm@64605
    21
wenzelm@64605
    22
  /* read message */
wenzelm@64605
    23
wenzelm@64605
    24
  private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
wenzelm@64605
    25
wenzelm@64605
    26
  private def read_line(): String =
wenzelm@64605
    27
  {
wenzelm@64605
    28
    val buffer = new ByteArrayOutputStream(100)
wenzelm@64605
    29
    var c = 0
wenzelm@64605
    30
    while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
wenzelm@64605
    31
    Library.trim_line(buffer.toString(UTF8.charset_name))
wenzelm@64605
    32
  }
wenzelm@64605
    33
wenzelm@64605
    34
  private def read_header(): List[String] =
wenzelm@64605
    35
  {
wenzelm@64605
    36
    val header = new mutable.ListBuffer[String]
wenzelm@64605
    37
    var line = ""
wenzelm@64605
    38
    while ({ line = read_line(); line != "" }) header += line
wenzelm@64605
    39
    header.toList
wenzelm@64605
    40
  }
wenzelm@64605
    41
wenzelm@64605
    42
  private def read_content(n: Int): String =
wenzelm@64605
    43
  {
wenzelm@64605
    44
    val buffer = new Array[Byte](n)
wenzelm@64605
    45
    var i = 0
wenzelm@64605
    46
    var m = 0
wenzelm@64605
    47
    do {
wenzelm@64605
    48
      m = in.read(buffer, i, n - i)
wenzelm@64605
    49
      if (m != -1) i += m
wenzelm@64605
    50
    }
wenzelm@64605
    51
    while (m != -1 && n > i)
wenzelm@64605
    52
wenzelm@64605
    53
    if (i == n) new String(buffer, UTF8.charset)
wenzelm@64605
    54
    else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
wenzelm@64605
    55
  }
wenzelm@64605
    56
wenzelm@64605
    57
  def read(): Option[JSON.T] =
wenzelm@64605
    58
  {
wenzelm@64605
    59
    read_header() match {
wenzelm@64605
    60
      case Nil => None
wenzelm@64605
    61
      case Content_Length(s) :: _ =>
wenzelm@64605
    62
        s match {
wenzelm@64605
    63
          case Value.Int(n) if n >= 0 =>
wenzelm@64605
    64
            val msg = read_content(n)
wenzelm@64605
    65
            log("IN:\n" + msg)
wenzelm@64605
    66
            Some(JSON.parse(msg))
wenzelm@64605
    67
          case _ => error("Bad Content-Length: " + s)
wenzelm@64605
    68
        }
wenzelm@64605
    69
      case header => error(cat_lines("Malformed header:" :: header))
wenzelm@64605
    70
    }
wenzelm@64605
    71
  }
wenzelm@64605
    72
wenzelm@64605
    73
wenzelm@64605
    74
  /* write message */
wenzelm@64605
    75
wenzelm@64605
    76
  def write(json: JSON.T)
wenzelm@64605
    77
  {
wenzelm@64605
    78
    val msg = JSON.Format(json)
wenzelm@64605
    79
    log("OUT:\n" + msg)
wenzelm@64605
    80
wenzelm@64605
    81
    val content = UTF8.bytes(msg)
wenzelm@64605
    82
    val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
wenzelm@64605
    83
    out.synchronized {
wenzelm@64605
    84
      out.write(header)
wenzelm@64605
    85
      out.write(content)
wenzelm@64605
    86
      out.flush
wenzelm@64605
    87
    }
wenzelm@64605
    88
  }
wenzelm@64642
    89
wenzelm@64642
    90
wenzelm@64642
    91
  /* display message */
wenzelm@64642
    92
wenzelm@64642
    93
  def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
wenzelm@64642
    94
    write(Protocol.DisplayMessage(message_type, message, show))
wenzelm@64642
    95
wenzelm@64642
    96
  def error_message(message: String, show: Boolean = true): Unit =
wenzelm@64642
    97
    display_message(Protocol.MessageType.Error, message, show)
wenzelm@64642
    98
  def warning(message: String, show: Boolean = true): Unit =
wenzelm@64642
    99
    display_message(Protocol.MessageType.Warning, message, show)
wenzelm@64642
   100
  def writeln(message: String, show: Boolean = true): Unit =
wenzelm@64642
   101
    display_message(Protocol.MessageType.Info, message, show)
wenzelm@64605
   102
}