explicit Server.Context with output channels (concurrent write);
authorwenzelm
Mon Mar 12 16:32:33 2018 +0100 (15 months ago)
changeset 678390c2ed45ece20
parent 67838 3a6ab890832f
child 67840 a9d450fc5a49
explicit Server.Context with output channels (concurrent write);
support for Logger and Progress;
src/Pure/PIDE/markup.scala
src/Pure/System/tty_loop.scala
src/Pure/Tools/server.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Mar 12 11:37:30 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Mar 12 16:32:33 2018 +0100
     1.3 @@ -457,6 +457,7 @@
     1.4    val STDOUT = "stdout"
     1.5    val STDERR = "stderr"
     1.6    val EXIT = "exit"
     1.7 +  val LOGGER = "logger"
     1.8  
     1.9    val WRITELN_MESSAGE = "writeln_message"
    1.10    val STATE_MESSAGE = "state_message"
     2.1 --- a/src/Pure/System/tty_loop.scala	Mon Mar 12 11:37:30 2018 +0100
     2.2 +++ b/src/Pure/System/tty_loop.scala	Mon Mar 12 16:32:33 2018 +0100
     2.3 @@ -10,7 +10,9 @@
     2.4  import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader}
     2.5  
     2.6  
     2.7 -class TTY_Loop(writer: Writer, reader: Reader, interrupt: Option[() => Unit] = None)
     2.8 +class TTY_Loop(writer: Writer, reader: Reader,
     2.9 +  writer_lock: AnyRef = new Object,
    2.10 +  interrupt: Option[() => Unit] = None)
    2.11  {
    2.12    private val console_output = Future.thread[Unit]("console_output") {
    2.13      try {
    2.14 @@ -50,9 +52,11 @@
    2.15                writer.close()
    2.16                finished = true
    2.17              case line =>
    2.18 -              writer.write(line)
    2.19 -              writer.write("\n")
    2.20 -              writer.flush()
    2.21 +              writer_lock.synchronized {
    2.22 +                writer.write(line)
    2.23 +                writer.write("\n")
    2.24 +                writer.flush()
    2.25 +              }
    2.26            }
    2.27          }
    2.28        }
     3.1 --- a/src/Pure/Tools/server.scala	Mon Mar 12 11:37:30 2018 +0100
     3.2 +++ b/src/Pure/Tools/server.scala	Mon Mar 12 16:32:33 2018 +0100
     3.3 @@ -60,13 +60,13 @@
     3.4  
     3.5    object Command
     3.6    {
     3.7 -    type T = PartialFunction[(Server, Any), Any]
     3.8 +    type T = PartialFunction[(Context, Any), Any]
     3.9  
    3.10      private val table: Map[String, T] =
    3.11        Map(
    3.12          "echo" -> { case (_, t) => t },
    3.13          "help" -> { case (_, ()) => table.keySet.toList.sorted },
    3.14 -        "shutdown" -> { case (server, ()) => server.close(); () })
    3.15 +        "shutdown" -> { case (context, ()) => context.shutdown(); () })
    3.16  
    3.17      def unapply(name: String): Option[T] = table.get(name)
    3.18    }
    3.19 @@ -112,9 +112,14 @@
    3.20  
    3.21      private val in = new BufferedInputStream(socket.getInputStream)
    3.22      private val out = new BufferedOutputStream(socket.getOutputStream)
    3.23 +    private val out_lock: AnyRef = new Object
    3.24  
    3.25      def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
    3.26 -      new TTY_Loop(new OutputStreamWriter(out), new InputStreamReader(in), interrupt = interrupt)
    3.27 +      new TTY_Loop(
    3.28 +        new OutputStreamWriter(out),
    3.29 +        new InputStreamReader(in),
    3.30 +        writer_lock = out_lock,
    3.31 +        interrupt = interrupt)
    3.32  
    3.33      def read_message(): Option[String] =
    3.34        try {
    3.35 @@ -126,7 +131,7 @@
    3.36        }
    3.37        catch { case _: SocketException => None }
    3.38  
    3.39 -    def write_message(msg: String)
    3.40 +    def write_message(msg: String): Unit = out_lock.synchronized
    3.41      {
    3.42        val b = UTF8.bytes(msg)
    3.43        if (b.length > 100 || b.contains(10)) {
    3.44 @@ -150,8 +155,52 @@
    3.45        reply_error(Map("message" -> message) ++ more)
    3.46  
    3.47      def notify(arg: Any) { reply(Server.Reply.NOTE, arg) }
    3.48 -    def notify_message(message: String, more: (String, JSON.T)*): Unit =
    3.49 -      notify(Map("message" -> message) ++ more)
    3.50 +    def notify_message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
    3.51 +      notify(Map(Markup.KIND -> kind, "message" -> msg) ++ more)
    3.52 +  }
    3.53 +
    3.54 +
    3.55 +  /* context with output channels */
    3.56 +
    3.57 +  class Context private[Server](server: Server, connection: Connection)
    3.58 +  {
    3.59 +    context =>
    3.60 +
    3.61 +    def shutdown() { server.close() }
    3.62 +
    3.63 +    def message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
    3.64 +      connection.notify_message(kind, msg, more:_*)
    3.65 +    def writeln(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WRITELN, msg, more:_*)
    3.66 +    def warning(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WARNING, msg, more:_*)
    3.67 +    def error_message(msg: String, more: (String, JSON.T)*): Unit =
    3.68 +      message(Markup.ERROR_MESSAGE, msg, more:_*)
    3.69 +
    3.70 +    val logger: Connection_Logger = new Connection_Logger(context)
    3.71 +    def progress(): Connection_Progress = new Connection_Progress(context)
    3.72 +
    3.73 +    override def toString: String = connection.toString
    3.74 +  }
    3.75 +
    3.76 +  class Connection_Logger private[Server](context: Context) extends Logger
    3.77 +  {
    3.78 +    def apply(msg: => String): Unit = context.message(Markup.LOGGER, msg)
    3.79 +
    3.80 +    override def toString: String = context.toString
    3.81 +  }
    3.82 +
    3.83 +  class Connection_Progress private[Server](context: Context) extends Progress
    3.84 +  {
    3.85 +    override def echo(msg: String): Unit = context.writeln(msg)
    3.86 +    override def echo_warning(msg: String): Unit = context.warning(msg)
    3.87 +    override def echo_error_message(msg: String): Unit = context.error_message(msg)
    3.88 +    override def theory(session: String, theory: String): Unit =
    3.89 +      context.writeln(session + ": theory " + theory, "session" -> session, "theory" -> theory)
    3.90 +
    3.91 +    @volatile private var is_stopped = false
    3.92 +    override def stopped: Boolean = is_stopped
    3.93 +    def stop { is_stopped = true }
    3.94 +
    3.95 +    override def toString: String = context.toString
    3.96    }
    3.97  
    3.98  
    3.99 @@ -340,6 +389,8 @@
   3.100  
   3.101    private def handle(connection: Server.Connection)
   3.102    {
   3.103 +    val context = new Server.Context(server, connection)
   3.104 +
   3.105      connection.read_message() match {
   3.106        case Some(msg) if msg == password =>
   3.107          connection.reply_ok(())
   3.108 @@ -347,16 +398,15 @@
   3.109          while (!finished) {
   3.110            connection.read_message() match {
   3.111              case None => finished = true
   3.112 -            case Some("") =>
   3.113 -              connection.notify_message("Command 'help' provides list of commands")
   3.114 +            case Some("") => context.writeln("Command 'help' provides list of commands")
   3.115              case Some(msg) =>
   3.116                val (name, argument) = Server.Argument.split(msg)
   3.117                name match {
   3.118                  case Server.Command(cmd) =>
   3.119                    argument match {
   3.120                      case Server.Argument(arg) =>
   3.121 -                      if (cmd.isDefinedAt((server, arg))) {
   3.122 -                        Exn.capture { cmd((server, arg)) } match {
   3.123 +                      if (cmd.isDefinedAt((context, arg))) {
   3.124 +                        Exn.capture { cmd((context, arg)) } match {
   3.125                            case Exn.Res(res) => connection.reply_ok(res)
   3.126                            case Exn.Exn(ERROR(msg)) => connection.reply_error(msg)
   3.127                            case Exn.Exn(exn) => throw exn