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