src/Tools/VSCode/src/channel.scala
author wenzelm
Wed, 28 Dec 2016 17:49:47 +0100
changeset 64686 7888be4fa496
parent 64675 c557279d93f2
child 64717 d2b50eb3d9ab
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/VSCode/src/channel.scala
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     3
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     4
Channel with JSON RPC protocol.
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     5
*/
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     6
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     7
package isabelle.vscode
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     8
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     9
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    10
import isabelle._
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    11
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
import java.io.{InputStream, OutputStream, FileOutputStream, ByteArrayOutputStream}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    13
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    14
import scala.collection.mutable
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    15
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    16
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    17
class Channel(in: InputStream, out: OutputStream, log_file: Option[Path] = None)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    18
{
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    19
  val log: Logger = Logger.make(log_file)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    20
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    21
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    22
  /* read message */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    23
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    24
  private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    25
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    26
  private def read_line(): String =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    27
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    28
    val buffer = new ByteArrayOutputStream(100)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    29
    var c = 0
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    30
    while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    31
    Library.trim_line(buffer.toString(UTF8.charset_name))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    32
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    33
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    34
  private def read_header(): List[String] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    35
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    36
    val header = new mutable.ListBuffer[String]
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    37
    var line = ""
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    38
    while ({ line = read_line(); line != "" }) header += line
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
    header.toList
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    40
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    41
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    42
  private def read_content(n: Int): String =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    43
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    44
    val buffer = new Array[Byte](n)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    45
    var i = 0
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    46
    var m = 0
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    47
    do {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    48
      m = in.read(buffer, i, n - i)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    49
      if (m != -1) i += m
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    51
    while (m != -1 && n > i)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    52
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    53
    if (i == n) new String(buffer, UTF8.charset)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    54
    else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    55
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    56
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    57
  def read(): Option[JSON.T] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    58
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    59
    read_header() match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    60
      case Nil => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    61
      case Content_Length(s) :: _ =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    62
        s match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    63
          case Value.Int(n) if n >= 0 =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    64
            val msg = read_content(n)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    65
            log("IN:\n" + msg)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    66
            Some(JSON.parse(msg))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    67
          case _ => error("Bad Content-Length: " + s)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    68
        }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    69
      case header => error(cat_lines("Malformed header:" :: header))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    70
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    71
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    72
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    73
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    74
  /* write message */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    75
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    76
  def write(json: JSON.T)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    77
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    78
    val msg = JSON.Format(json)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    79
    log("OUT:\n" + msg)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    80
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    81
    val content = UTF8.bytes(msg)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    82
    val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    83
    out.synchronized {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    84
      out.write(header)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    85
      out.write(content)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    86
      out.flush
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    87
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    88
  }
64642
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    89
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    90
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    91
  /* display message */
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    92
64686
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    93
  def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    94
    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
64642
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    95
64686
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    96
  def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    97
  def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    98
  def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    99
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
   100
  def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
   101
  def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
   102
  def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   103
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   104
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   105
  /* diagnostics */
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   106
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   107
  def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   108
    write(Protocol.PublishDiagnostics(uri, diagnostics))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   109
}