src/Tools/VSCode/src/channel.scala
author wenzelm
Sun, 01 Jan 2017 13:15:50 +0100
changeset 64733 20174e871623
parent 64717 d2b50eb3d9ab
child 64777 ca09695eb43c
permissions -rw-r--r--
automatically build session image;
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
64717
d2b50eb3d9ab tuned signature;
wenzelm
parents: 64686
diff changeset
    17
class Channel(in: InputStream, out: OutputStream, log: Logger = No_Logger)
64605
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
  /* read message */
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
  private val Content_Length = """^\s*Content-Length:\s*(\d+)\s*$""".r
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    22
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    23
  private def read_line(): String =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    24
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    25
    val buffer = new ByteArrayOutputStream(100)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    26
    var c = 0
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    27
    while ({ c = in.read; c != -1 && c != 10 }) buffer.write(c)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    28
    Library.trim_line(buffer.toString(UTF8.charset_name))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    29
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    30
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    31
  private def read_header(): List[String] =
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
    val header = new mutable.ListBuffer[String]
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    34
    var line = ""
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    35
    while ({ line = read_line(); line != "" }) header += line
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    36
    header.toList
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    37
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    38
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
  private def read_content(n: Int): String =
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
    val buffer = new Array[Byte](n)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    42
    var i = 0
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    43
    var m = 0
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    44
    do {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    45
      m = in.read(buffer, i, n - i)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    46
      if (m != -1) i += m
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    47
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    48
    while (m != -1 && n > i)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    49
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
    if (i == n) new String(buffer, UTF8.charset)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    51
    else error("Bad message content (unexpected EOF after " + i + " of " + n + " bytes)")
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
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    54
  def read(): Option[JSON.T] =
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
    read_header() match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    57
      case Nil => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    58
      case Content_Length(s) :: _ =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    59
        s match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    60
          case Value.Int(n) if n >= 0 =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    61
            val msg = read_content(n)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    62
            log("IN:\n" + msg)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    63
            Some(JSON.parse(msg))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    64
          case _ => error("Bad Content-Length: " + s)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    65
        }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    66
      case header => error(cat_lines("Malformed header:" :: header))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    67
    }
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
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
  /* write message */
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
  def write(json: JSON.T)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    74
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    75
    val msg = JSON.Format(json)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    76
    log("OUT:\n" + msg)
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 content = UTF8.bytes(msg)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    79
    val header = UTF8.bytes("Content-Length: " + content.length + "\r\n\r\n")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    80
    out.synchronized {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    81
      out.write(header)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    82
      out.write(content)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    83
      out.flush
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    84
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    85
  }
64642
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    86
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    87
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    88
  /* display message */
c231206a84c8 display messages, according to regular Isabelle Output;
wenzelm
parents: 64605
diff changeset
    89
64686
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    90
  def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    91
    write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
64642
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 error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    94
  def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    95
  def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    96
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    97
  def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    98
  def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
7888be4fa496 clarified signature;
wenzelm
parents: 64675
diff changeset
    99
  def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   100
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   101
64733
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   102
  /* progress */
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   103
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   104
  def make_progress(verbose: Boolean = false): Progress =
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   105
    new Progress {
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   106
      override def echo(msg: String): Unit = log_writeln(msg)
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   107
      override def theory(session: String, theory: String): Unit =
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   108
        if (verbose) echo(session + ": theory " + theory)
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   109
    }
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   110
20174e871623 automatically build session image;
wenzelm
parents: 64717
diff changeset
   111
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   112
  /* diagnostics */
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   113
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   114
  def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
c557279d93f2 support for diagnostics;
wenzelm
parents: 64658
diff changeset
   115
    write(Protocol.PublishDiagnostics(uri, diagnostics))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   116
}