src/Pure/Tools/server.scala
author wenzelm
Mon, 12 Mar 2018 16:32:33 +0100
changeset 67839 0c2ed45ece20
parent 67838 3a6ab890832f
child 67840 a9d450fc5a49
permissions -rw-r--r--
explicit Server.Context with output channels (concurrent write); support for Logger and Progress;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/server.scala
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     3
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     4
Resident Isabelle servers.
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     5
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     6
Message formats:
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     7
  - short message (single line):
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     8
      NAME ARGUMENT
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
     9
  - long message (multiple lines):
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
    10
      BYTE_LENGTH
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
    11
      NAME ARGUMENT
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    12
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    13
Argument formats:
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    14
  - Unit as empty string
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    15
  - XML.Elem in YXML notation
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    16
  - JSON.T in standard notation
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    17
*/
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    18
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    19
package isabelle
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    20
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    21
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
    22
import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
    23
  IOException}
67797
1cfc7541012e Entry.connection: proview password here;
wenzelm
parents: 67796
diff changeset
    24
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    25
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    26
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    27
object Server
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    28
{
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    29
  /* message argument */
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    30
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    31
  object Argument
67794
wenzelm
parents: 67793
diff changeset
    32
  {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    33
    def split(msg: String): (String, String) =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    34
    {
67838
3a6ab890832f allow "." in message name;
wenzelm
parents: 67837
diff changeset
    35
      val name =
3a6ab890832f allow "." in message name;
wenzelm
parents: 67837
diff changeset
    36
        msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c) || c == '.')
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    37
      val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    38
      (name, argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    39
    }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    40
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    41
    def print(arg: Any): String =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    42
      arg match {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    43
        case () => ""
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    44
        case t: XML.Elem => YXML.string_of_tree(t)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    45
        case t: JSON.T => JSON.Format(t)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    46
      }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    47
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    48
    def parse(argument: String): Any =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    49
      if (argument == "") ()
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    50
      else if (YXML.detect_elem(argument)) YXML.parse_elem(argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    51
      else JSON.parse(argument, strict = false)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    52
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    53
    def unapply(argument: String): Option[Any] =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    54
      try { Some(parse(argument)) }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    55
      catch { case ERROR(_) => None }
67794
wenzelm
parents: 67793
diff changeset
    56
  }
wenzelm
parents: 67793
diff changeset
    57
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    58
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    59
  /* input command */
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    60
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    61
  object Command
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    62
  {
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
    63
    type T = PartialFunction[(Context, Any), Any]
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    64
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    65
    private val table: Map[String, T] =
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    66
      Map(
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    67
        "echo" -> { case (_, t) => t },
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    68
        "help" -> { case (_, ()) => table.keySet.toList.sorted },
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
    69
        "shutdown" -> { case (context, ()) => context.shutdown(); () })
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    70
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    71
    def unapply(name: String): Option[T] = table.get(name)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    72
  }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    73
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    74
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    75
  /* output reply */
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
    76
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    77
  object Reply extends Enumeration
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    78
  {
67801
8f5f5fbe291b added Reply.NOTE for asynchronous notifications;
wenzelm
parents: 67800
diff changeset
    79
    val OK, ERROR, NOTE = Value
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
    80
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    81
    def unapply(msg: String): Option[(Reply.Value, Any)] =
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
    82
    {
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
    83
      if (msg == "") None
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
    84
      else {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    85
        val (name, argument) = Argument.split(msg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    86
        for {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    87
          reply <-
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    88
            try { Some(withName(name)) }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    89
            catch { case _: NoSuchElementException => None }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    90
          arg <- Argument.unapply(argument)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
    91
        } yield (reply, arg)
67800
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
    92
      }
fd30e767d900 more operations;
wenzelm
parents: 67799
diff changeset
    93
    }
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    94
  }
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    95
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    96
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    97
  /* socket connection */
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    98
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    99
  object Connection
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   100
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   101
    def apply(socket: Socket): Connection =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   102
      new Connection(socket)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   103
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   104
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   105
  class Connection private(socket: Socket)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   106
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   107
    override def toString: String = socket.toString
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   108
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   109
    def close() { socket.close }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   110
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   111
    def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   112
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   113
    private val in = new BufferedInputStream(socket.getInputStream)
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   114
    private val out = new BufferedOutputStream(socket.getOutputStream)
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   115
    private val out_lock: AnyRef = new Object
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   116
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
   117
    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   118
      new TTY_Loop(
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   119
        new OutputStreamWriter(out),
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   120
        new InputStreamReader(in),
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   121
        writer_lock = out_lock,
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   122
        interrupt = interrupt)
67837
932d01332c6c re-use existing in/out streams;
wenzelm
parents: 67834
diff changeset
   123
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   124
    def read_message(): Option[String] =
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   125
      try {
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   126
        Bytes.read_line(in).map(_.text) match {
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   127
          case Some(Value.Int(n)) =>
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   128
            Bytes.read_block(in, n).map(bytes => Library.trim_line(bytes.text))
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   129
          case res => res
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   130
        }
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   131
      }
67805
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 67801
diff changeset
   132
      catch { case _: SocketException => None }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   133
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   134
    def write_message(msg: String): Unit = out_lock.synchronized
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   135
    {
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   136
      val b = UTF8.bytes(msg)
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   137
      if (b.length > 100 || b.contains(10)) {
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   138
        out.write(UTF8.bytes((b.length + 1).toString))
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   139
        out.write(10)
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   140
      }
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   141
      out.write(b)
67805
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 67801
diff changeset
   142
      out.write(10)
2d9a265b294e more uniform Bytes.read_line/read_block operations;
wenzelm
parents: 67801
diff changeset
   143
      try { out.flush() } catch { case _: SocketException => }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   144
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   145
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   146
    def reply(r: Server.Reply.Value, arg: Any)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   147
    {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   148
      val argument = Argument.print(arg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   149
      write_message(if (argument == "") r.toString else r.toString + " " + argument)
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   150
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   151
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   152
    def reply_ok(arg: Any) { reply(Server.Reply.OK, arg) }
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   153
    def reply_error(arg: Any) { reply(Server.Reply.ERROR, arg) }
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   154
    def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   155
      reply_error(Map("message" -> message) ++ more)
67801
8f5f5fbe291b added Reply.NOTE for asynchronous notifications;
wenzelm
parents: 67800
diff changeset
   156
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   157
    def notify(arg: Any) { reply(Server.Reply.NOTE, arg) }
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   158
    def notify_message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   159
      notify(Map(Markup.KIND -> kind, "message" -> msg) ++ more)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   160
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   161
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   162
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   163
  /* context with output channels */
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   164
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   165
  class Context private[Server](server: Server, connection: Connection)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   166
  {
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   167
    context =>
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   168
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   169
    def shutdown() { server.close() }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   170
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   171
    def message(kind: String, msg: String, more: (String, JSON.T)*): Unit =
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   172
      connection.notify_message(kind, msg, more:_*)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   173
    def writeln(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WRITELN, msg, more:_*)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   174
    def warning(msg: String, more: (String, JSON.T)*): Unit = message(Markup.WARNING, msg, more:_*)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   175
    def error_message(msg: String, more: (String, JSON.T)*): Unit =
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   176
      message(Markup.ERROR_MESSAGE, msg, more:_*)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   177
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   178
    val logger: Connection_Logger = new Connection_Logger(context)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   179
    def progress(): Connection_Progress = new Connection_Progress(context)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   180
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   181
    override def toString: String = connection.toString
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   182
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   183
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   184
  class Connection_Logger private[Server](context: Context) extends Logger
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   185
  {
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   186
    def apply(msg: => String): Unit = context.message(Markup.LOGGER, msg)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   187
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   188
    override def toString: String = context.toString
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   189
  }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   190
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   191
  class Connection_Progress private[Server](context: Context) extends Progress
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   192
  {
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   193
    override def echo(msg: String): Unit = context.writeln(msg)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   194
    override def echo_warning(msg: String): Unit = context.warning(msg)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   195
    override def echo_error_message(msg: String): Unit = context.error_message(msg)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   196
    override def theory(session: String, theory: String): Unit =
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   197
      context.writeln(session + ": theory " + theory, "session" -> session, "theory" -> theory)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   198
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   199
    @volatile private var is_stopped = false
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   200
    override def stopped: Boolean = is_stopped
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   201
    def stop { is_stopped = true }
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   202
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   203
    override def toString: String = context.toString
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   204
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   205
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   206
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   207
  /* server info */
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   208
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   209
  sealed case class Info(name: String, port: Int, password: String)
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   210
  {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   211
    override def toString: String =
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   212
      "server " + quote(name) + " = " + print(port, password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   213
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   214
    def connection(): Connection =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   215
    {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   216
      val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   217
      connection.write_message(password)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   218
      connection
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   219
    }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   220
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   221
    def active(): Boolean =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   222
      try {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   223
        using(connection())(connection =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   224
          {
67832
069aa924671f clarified signature -- do not expose socket;
wenzelm
parents: 67823
diff changeset
   225
            connection.set_timeout(Time.seconds(2.0))
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   226
            connection.read_message() == Some(Reply.OK.toString)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   227
          })
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   228
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   229
      catch {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   230
        case _: IOException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   231
        case _: SocketException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   232
        case _: SocketTimeoutException => false
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   233
      }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   234
  }
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   235
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   236
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   237
  /* per-user servers */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   238
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   239
  val default_name = "isabelle"
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   240
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   241
  def print(port: Int, password: String): String =
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   242
    "127.0.0.1:" + port + " (password " + quote(password) + ")"
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   243
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   244
  object Data
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   245
  {
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   246
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   247
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66353
diff changeset
   248
    val name = SQL.Column.string("name").make_primary_key
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   249
    val port = SQL.Column.int("port")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   250
    val password = SQL.Column.string("password")
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   251
    val table = SQL.Table("isabelle_servers", List(name, port, password))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   252
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   253
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   254
  def list(db: SQLite.Database): List[Info] =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   255
    if (db.tables.contains(Data.table.name)) {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   256
      db.using_statement(Data.table.select())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   257
        stmt.execute_query().iterator(res =>
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   258
          Info(
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   259
            res.string(Data.name),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   260
            res.int(Data.port),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   261
            res.string(Data.password))).toList.sortBy(_.name))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   262
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   263
    else Nil
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   264
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   265
  def find(db: SQLite.Database, name: String): Option[Info] =
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   266
    list(db).find(server_info => server_info.name == name && server_info.active)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   267
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   268
  def init(name: String = default_name, port: Int = 0, existing_server: Boolean = false)
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   269
    : (Info, Option[Server]) =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   270
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   271
    using(SQLite.open_database(Data.database))(db =>
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   272
      {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   273
        db.transaction {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   274
          Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   275
          db.create_table(Data.table)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   276
          list(db).filterNot(_.active).foreach(server_info =>
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   277
            db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   278
              _.execute))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   279
        }
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   280
        db.transaction {
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   281
          find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   282
            case Some(server_info) => (server_info, None)
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   283
            case None =>
67821
82fb12061069 more uniform output: this may be parsed by another program;
wenzelm
parents: 67820
diff changeset
   284
              if (existing_server) error("Isabelle server " + quote(name) + " not running")
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   285
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   286
              val server = new Server(port)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   287
              val server_info = Info(name, server.port, server.password)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   288
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   289
              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   290
              db.using_statement(Data.table.insert())(stmt =>
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   291
              {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   292
                stmt.string(1) = server_info.name
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   293
                stmt.int(2) = server_info.port
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   294
                stmt.string(3) = server_info.password
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   295
                stmt.execute()
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   296
              })
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   297
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   298
              server.start
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   299
              (server_info, Some(server))
67799
f801cb14a0b3 more thorough init: purge inactive entries;
wenzelm
parents: 67798
diff changeset
   300
          }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   301
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   302
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   303
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   304
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   305
  def exit(name: String = default_name): Boolean =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   306
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   307
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   308
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   309
        find(db, name) match {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   310
          case Some(server_info) =>
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   311
            using(server_info.connection())(_.write_message("shutdown"))
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   312
            while(server_info.active) { Thread.sleep(50) }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   313
            true
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   314
          case None => false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   315
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   316
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   317
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   318
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   319
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   320
  /* Isabelle tool wrapper */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   321
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   322
  val isabelle_tool =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   323
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   324
    {
67806
bd4c440c8be7 option for console interaction;
wenzelm
parents: 67805
diff changeset
   325
      var console = false
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   326
      var operation_list = false
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   327
      var operation_exit = false
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   328
      var name = default_name
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   329
      var port = 0
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   330
      var existing_server = false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   331
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   332
      val getopts =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   333
        Getopts("""
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   334
Usage: isabelle server [OPTIONS]
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   335
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   336
  Options are:
67806
bd4c440c8be7 option for console interaction;
wenzelm
parents: 67805
diff changeset
   337
    -C           console interaction with specified server
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   338
    -L           list servers (exclusive operation)
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   339
    -X           exit specified server (exclusive operation)
67822
0e2484df2491 clarified default server name;
wenzelm
parents: 67821
diff changeset
   340
    -n NAME      explicit server name (default: """ + default_name + """)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   341
    -p PORT      explicit server port
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   342
    -s           assume existing server, no implicit startup
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   343
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   344
  Manage resident Isabelle servers.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   345
""",
67806
bd4c440c8be7 option for console interaction;
wenzelm
parents: 67805
diff changeset
   346
          "C" -> (_ => console = true),
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   347
          "L" -> (_ => operation_list = true),
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   348
          "X" -> (_ => operation_exit = true),
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   349
          "n:" -> (arg => name = arg),
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   350
          "p:" -> (arg => port = Value.Int.parse(arg)),
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   351
          "s" -> (_ => existing_server = true))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   352
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   353
      val more_args = getopts(args)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   354
      if (more_args.nonEmpty) getopts.usage()
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   355
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   356
      if (operation_list) {
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   357
        for {
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   358
          server_info <- using(SQLite.open_database(Data.database))(list(_))
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   359
          if server_info.active
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   360
        } Output.writeln(server_info.toString, stdout = true)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   361
      }
67823
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   362
      else if (operation_exit) {
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   363
        val ok = Server.exit(name)
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   364
        sys.exit(if (ok) 0 else 1)
92cf045c876b more options;
wenzelm
parents: 67822
diff changeset
   365
      }
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   366
      else {
67811
33199d033505 more options: client without implicit server startup;
wenzelm
parents: 67809
diff changeset
   367
        val (server_info, server) = init(name, port = port, existing_server = existing_server)
67807
331619e6c8b0 clarified signature;
wenzelm
parents: 67806
diff changeset
   368
        Output.writeln(server_info.toString, stdout = true)
67834
wenzelm
parents: 67833
diff changeset
   369
        if (console) {
wenzelm
parents: 67833
diff changeset
   370
          using(server_info.connection())(connection => connection.tty_loop().join)
wenzelm
parents: 67833
diff changeset
   371
        }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   372
        server.foreach(_.join)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   373
      }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   374
    })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   375
}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   376
66352
7ed911242266 clarified signature;
wenzelm
parents: 66351
diff changeset
   377
class Server private(_port: Int)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   378
{
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   379
  server =>
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   380
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   381
  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   382
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   383
  def close() { server_socket.close }
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   384
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   385
  def port: Int = server_socket.getLocalPort
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   386
  val password: String = Library.UUID()
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   387
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   388
  override def toString: String = Server.print(port, password)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   389
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   390
  private def handle(connection: Server.Connection)
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   391
  {
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   392
    val context = new Server.Context(server, connection)
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   393
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   394
    connection.read_message() match {
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   395
      case Some(msg) if msg == password =>
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   396
        connection.reply_ok(())
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   397
        var finished = false
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   398
        while (!finished) {
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   399
          connection.read_message() match {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   400
            case None => finished = true
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   401
            case Some("") => context.writeln("Command 'help' provides list of commands")
67809
a5fa8d854e5e more flexible message formats;
wenzelm
parents: 67807
diff changeset
   402
            case Some(msg) =>
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   403
              val (name, argument) = Server.Argument.split(msg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   404
              name match {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   405
                case Server.Command(cmd) =>
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   406
                  argument match {
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   407
                    case Server.Argument(arg) =>
67839
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   408
                      if (cmd.isDefinedAt((context, arg))) {
0c2ed45ece20 explicit Server.Context with output channels (concurrent write);
wenzelm
parents: 67838
diff changeset
   409
                        Exn.capture { cmd((context, arg)) } match {
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   410
                          case Exn.Res(res) => connection.reply_ok(res)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   411
                          case Exn.Exn(ERROR(msg)) => connection.reply_error(msg)
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   412
                          case Exn.Exn(exn) => throw exn
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   413
                        }
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   414
                      }
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   415
                      else {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   416
                        connection.reply_error_message(
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   417
                          "Bad argument for command " + Library.single_quote(name),
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   418
                          "argument" -> argument)
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   419
                      }
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   420
                    case _ =>
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   421
                      connection.reply_error_message(
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   422
                        "Malformed argument for command " + Library.single_quote(name),
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   423
                        "argument" -> argument)
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   424
                  }
67820
e30d6368c7c8 clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents: 67812
diff changeset
   425
                case _ => connection.reply_error("Bad command " + Library.single_quote(name))
66921
3d3bd0718ef2 clarified command language;
wenzelm
parents: 66857
diff changeset
   426
              }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   427
          }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   428
        }
67796
bb2bbabf3d37 clarified initial protocol;
wenzelm
parents: 67795
diff changeset
   429
      case _ =>
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   430
    }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   431
  }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   432
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   433
  private lazy val server_thread: Thread =
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   434
    Standard_Thread.fork("server") {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   435
      var finished = false
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   436
      while (!finished) {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   437
        Exn.capture(server_socket.accept) match {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   438
          case Exn.Res(socket) =>
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   439
            Standard_Thread.fork("server_connection")
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   440
              { using(Server.Connection(socket))(handle(_)) }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   441
          case Exn.Exn(_) => finished = true
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   442
        }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   443
      }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   444
    }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   445
67790
1babcc248be0 clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents: 67789
diff changeset
   446
  def start { server_thread }
1babcc248be0 clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents: 67789
diff changeset
   447
67791
acecef5fad58 tuned signature;
wenzelm
parents: 67790
diff changeset
   448
  def join { server_thread.join; close() }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   449
}