src/Tools/VSCode/src/channel.scala
author wenzelm
Tue Jan 03 14:17:03 2017 +0100 (2017-01-03)
changeset 64759 100941134718
parent 64733 20174e871623
child 64777 ca09695eb43c
permissions -rw-r--r--
clarified master_dir: file-URL;
     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: Logger = No_Logger)
    18 {
    19   /* read message */
    20 
    21   private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
    22 
    23   private def read_line(): String =
    24   {
    25     val buffer = new ByteArrayOutputStream(100)
    26     var c = 0
    27     while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
    28     Library.trim_line(buffer.toString(UTF8.charset_name))
    29   }
    30 
    31   private def read_header(): List[String] =
    32   {
    33     val header = new mutable.ListBuffer[String]
    34     var line = ""
    35     while ({ line = read_line(); line != "" }) header += line
    36     header.toList
    37   }
    38 
    39   private def read_content(n: Int): String =
    40   {
    41     val buffer = new Array[Byte](n)
    42     var i = 0
    43     var m = 0
    44     do {
    45       m = in.read(buffer, i, n - i)
    46       if (m != -1) i += m
    47     }
    48     while (m != -1 && n > i)
    49 
    50     if (i == n) new String(buffer, UTF8.charset)
    51     else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
    52   }
    53 
    54   def read(): Option[JSON.T] =
    55   {
    56     read_header() match {
    57       case Nil => None
    58       case Content_Length(s) :: _ =>
    59         s match {
    60           case Value.Int(n) if n >= 0 =>
    61             val msg = read_content(n)
    62             log("IN:\n" + msg)
    63             Some(JSON.parse(msg))
    64           case _ => error("Bad Content-Length: " + s)
    65         }
    66       case header => error(cat_lines("Malformed header:" :: header))
    67     }
    68   }
    69 
    70 
    71   /* write message */
    72 
    73   def write(json: JSON.T)
    74   {
    75     val msg = JSON.Format(json)
    76     log("OUT:\n" + msg)
    77 
    78     val content = UTF8.bytes(msg)
    79     val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
    80     out.synchronized {
    81       out.write(header)
    82       out.write(content)
    83       out.flush
    84     }
    85   }
    86 
    87 
    88   /* display message */
    89 
    90   def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
    91     write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
    92 
    93   def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
    94   def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
    95   def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
    96 
    97   def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
    98   def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
    99   def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
   100 
   101 
   102   /* progress */
   103 
   104   def make_progress(verbose: Boolean = false): Progress =
   105     new Progress {
   106       override def echo(msg: String): Unit = log_writeln(msg)
   107       override def theory(session: String, theory: String): Unit =
   108         if (verbose) echo(session + ": theory " + theory)
   109     }
   110 
   111 
   112   /* diagnostics */
   113 
   114   def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
   115     write(Protocol.PublishDiagnostics(uri, diagnostics))
   116 }