src/Tools/VSCode/src/channel.scala
author wenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622 529bbb8977c7
parent 64605 9c1173a7e4cb
child 64642 c231206a84c8
permissions -rw-r--r--
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
     1 /*  Title:      Tools/VSCode/src/channel.scala
     2     Author:     Makarius
     3 
     4 Channel with JSON RPC protocol.
     5 */
     6 
     7 package isabelle.vscode
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
    13 
    14 import scala.collection.mutable
    15 
    16 
    17 class Channel(in: InputStream, out: OutputStream, log_file: Option[Path] = None)
    18 {
    19   val log: Logger = Logger.make(log_file)
    20 
    21 
    22   /* read message */
    23 
    24   private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
    25 
    26   private def read_line(): String =
    27   {
    28     val buffer = new ByteArrayOutputStream(100)
    29     var c = 0
    30     while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
    31     Library.trim_line(buffer.toString(UTF8.charset_name))
    32   }
    33 
    34   private def read_header(): List[String] =
    35   {
    36     val header = new mutable.ListBuffer[String]
    37     var line = ""
    38     while ({ line = read_line(); line != "" }) header += line
    39     header.toList
    40   }
    41 
    42   private def read_content(n: Int): String =
    43   {
    44     val buffer = new Array[Byte](n)
    45     var i = 0
    46     var m = 0
    47     do {
    48       m = in.read(buffer, i, n - i)
    49       if (m != -1) i += m
    50     }
    51     while (m != -1 && n > i)
    52 
    53     if (i == n) new String(buffer, UTF8.charset)
    54     else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
    55   }
    56 
    57   def read(): Option[JSON.T] =
    58   {
    59     read_header() match {
    60       case Nil => None
    61       case Content_Length(s) :: _ =>
    62         s match {
    63           case Value.Int(n) if n >= 0 =>
    64             val msg = read_content(n)
    65             log("IN:\n" + msg)
    66             Some(JSON.parse(msg))
    67           case _ => error("Bad Content-Length: " + s)
    68         }
    69       case header => error(cat_lines("Malformed header:" :: header))
    70     }
    71   }
    72 
    73 
    74   /* write message */
    75 
    76   def write(json: JSON.T)
    77   {
    78     val msg = JSON.Format(json)
    79     log("OUT:\n" + msg)
    80 
    81     val content = UTF8.bytes(msg)
    82     val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
    83     out.synchronized {
    84       out.write(header)
    85       out.write(content)
    86       out.flush
    87     }
    88   }
    89 }