src/Tools/VSCode/src/channel.scala
author wenzelm
Sat Jun 09 21:52:16 2018 +0200 (12 months ago)
changeset 68410 4e27f5c361d2
parent 67856 ec9f1ec763a0
child 68957 eef4e983fd9d
permissions -rw-r--r--
clarified signature: more uniform theory_message (see also d7920eb7de54);
     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, File => JFile}
    13 
    14 import scala.collection.mutable
    15 
    16 
    17 class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger, verbose: Boolean = false)
    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     Bytes.read_line(in) match {
    25       case Some(bytes) => bytes.text
    26       case None => ""
    27     }
    28 
    29   private def read_header(): List[String] =
    30   {
    31     val header = new mutable.ListBuffer[String]
    32     var line = ""
    33     while ({ line = read_line(); line != "" }) header += line
    34     header.toList
    35   }
    36 
    37   private def read_content(n: Int): String =
    38   {
    39     val bytes = Bytes.read_stream(in, limit = n)
    40     if (bytes.length == n) bytes.text
    41     else error("Bad message content (unexpected EOF after " + bytes.length + " of " + n + " bytes)")
    42   }
    43 
    44   def read(): Option[JSON.T] =
    45   {
    46     read_header() match {
    47       case Nil => None
    48       case Content_Length(s) :: _ =>
    49         s match {
    50           case Value.Int(n) if n >= 0 =>
    51             val msg = read_content(n)
    52             val json = JSON.parse(msg)
    53             Protocol.Message.log("IN: " + n, json, log, verbose)
    54             Some(json)
    55           case _ => error("Bad Content-Length: " + s)
    56         }
    57       case header => error(cat_lines("Malformed header:" :: header))
    58     }
    59   }
    60 
    61 
    62   /* write message */
    63 
    64   def write(json: JSON.T)
    65   {
    66     val msg = JSON.Format(json)
    67     val content = UTF8.bytes(msg)
    68     val n = content.length
    69     val header = UTF8.bytes("Content-Length: " + n + "\r\n\r\n")
    70 
    71     Protocol.Message.log("OUT: " + n, json, log, verbose)
    72     out.synchronized {
    73       out.write(header)
    74       out.write(content)
    75       out.flush
    76     }
    77   }
    78 
    79 
    80   /* display message */
    81 
    82   def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
    83     write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
    84 
    85   def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
    86   def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
    87   def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
    88 
    89   def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
    90   def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
    91   def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
    92 
    93   object Error_Logger extends Logger
    94   {
    95     def apply(msg: => String) { log_error_message(msg) }
    96   }
    97 
    98 
    99   /* progress */
   100 
   101   def progress(verbose: Boolean = false): Progress =
   102     new Progress {
   103       override def echo(msg: String): Unit = log_writeln(msg)
   104       override def echo_warning(msg: String): Unit = log_warning(msg)
   105       override def echo_error_message(msg: String): Unit = log_error_message(msg)
   106       override def theory(session: String, theory: String): Unit =
   107         if (verbose) echo(Progress.theory_message(session, theory))
   108     }
   109 }