src/Pure/Tools/server.scala
author wenzelm
Fri, 09 Mar 2018 12:38:46 +0100
changeset 67787 8335d88195c4
parent 67786 be6d69595ca7
child 67788 34e76587dc94
permissions -rw-r--r--
clarified toString operations;
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.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     5
*/
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     6
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     7
package isabelle
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     8
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
     9
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
    10
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
    11
  IOException}
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
    12
import java.net.{Socket, ServerSocket, InetAddress}
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    13
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    14
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    15
object Server
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    16
{
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    17
  /* protocol */
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    18
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
    19
  val commands: Map[String, PartialFunction[(Server, JSON.T), JSON.T]] =
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
    20
    Map(
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
    21
      "echo" -> { case (_, t) => t },
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
    22
      "help" -> { case (_, JSON.empty) => commands.keySet.toList.sorted },
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
    23
      "shutdown" -> { case (server, JSON.empty) => server.shutdown(); JSON.empty })
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
    24
66927
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    25
  object Reply extends Enumeration
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    26
  {
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    27
    val OK, ERROR = Value
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    28
  }
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    29
153d7b68e8f8 more formal messages;
wenzelm
parents: 66921
diff changeset
    30
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    31
  /* socket connection */
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    32
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    33
  object Connection
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    34
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    35
    def apply(socket: Socket): Connection =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    36
      new Connection(socket)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    37
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    38
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    39
  class Connection private(socket: Socket)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    40
  {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    41
    override def toString: String = socket.toString
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    42
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    43
    def close() { socket.close }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    44
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    45
    val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    46
    val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    47
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    48
    def read_line(): Option[String] =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    49
      reader.readLine() match {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    50
        case null => None
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    51
        case line => Some(line)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    52
      }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    53
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    54
    def write_line(msg: String)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    55
    {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    56
      require(split_lines(msg).length <= 1)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    57
      writer.write(msg)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    58
      writer.newLine()
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    59
      writer.flush()
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    60
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    61
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    62
    def reply(r: Server.Reply.Value, t: JSON.T)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    63
    {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    64
      write_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t))
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    65
    }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    66
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    67
    def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    68
    def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    69
    def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    70
      reply_error(Map("message" -> message) ++ more)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    71
  }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    72
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    73
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    74
  /* per-user servers */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    75
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
    76
  def print(port: Int, password: String): String =
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
    77
    "127.0.0.1:" + port + " (password " + quote(password) + ")"
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
    78
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    79
  object Data
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    80
  {
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
    81
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    82
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66353
diff changeset
    83
    val name = SQL.Column.string("name").make_primary_key
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
    84
    val port = SQL.Column.int("port")
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    85
    val password = SQL.Column.string("password")
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
    86
    val table = SQL.Table("isabelle_servers", List(name, port, password))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    87
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
    88
    sealed case class Entry(name: String, port: Int, password: String)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    89
    {
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
    90
      override def toString: String =
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
    91
        "server " + quote(name) + " = " + print(port, password)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
    92
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    93
      def connection(): Connection =
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    94
        Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
    95
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
    96
      def active(): Boolean =
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
    97
        try { connection().close; true }
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
    98
        catch { case _: IOException => false }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    99
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   100
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   101
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   102
  def list(db: SQLite.Database): List[Data.Entry] =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   103
    if (db.tables.contains(Data.table.name)) {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   104
      db.using_statement(Data.table.select())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   105
        stmt.execute_query().iterator(res =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   106
          Data.Entry(
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   107
            res.string(Data.name),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   108
            res.int(Data.port),
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   109
            res.string(Data.password))).toList.sortBy(_.name))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   110
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   111
    else Nil
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   112
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   113
  def find(db: SQLite.Database, name: String): Option[Data.Entry] =
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   114
    list(db).find(entry => entry.name == name && entry.active)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   115
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   116
  def start(name: String = "", port: Int = 0): (Data.Entry, Option[Server]) =
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   117
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   118
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   119
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   120
        find(db, name) match {
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   121
          case Some(entry) => (entry, None)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   122
          case None =>
66352
7ed911242266 clarified signature;
wenzelm
parents: 66351
diff changeset
   123
            val server = new Server(port)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   124
            val entry = Data.Entry(name, server.port, server.password)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   125
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   126
            Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   127
            db.create_table(Data.table)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   128
            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   129
            db.using_statement(Data.table.insert())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   130
            {
66349
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   131
              stmt.string(1) = entry.name
66b843e4cff5 clarified database names;
wenzelm
parents: 66348
diff changeset
   132
              stmt.int(2) = entry.port
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   133
              stmt.string(3) = entry.password
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   134
              stmt.execute()
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   135
            })
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   136
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   137
            (entry, Some(server))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   138
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   139
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   140
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   141
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   142
  def stop(name: String = ""): Boolean =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   143
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   144
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   145
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   146
        find(db, name) match {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   147
          case Some(entry) =>
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   148
            using(entry.connection())(connection =>
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   149
              {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   150
                connection.write_line(entry.password)
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   151
                connection.write_line("shutdown")
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   152
              })
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   153
            while(entry.active) { Thread.sleep(100) }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   154
            true
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   155
          case None => false
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   156
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   157
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   158
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   159
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   160
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   161
  /* Isabelle tool wrapper */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   162
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   163
  val isabelle_tool =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   164
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   165
    {
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   166
      var operation_list = false
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   167
      var name = ""
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   168
      var port = 0
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   169
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   170
      val getopts =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   171
        Getopts("""
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   172
Usage: isabelle server [OPTIONS]
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   173
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   174
  Options are:
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   175
    -L           list servers
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   176
    -n NAME      explicit server name
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   177
    -p PORT      explicit server port
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   178
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   179
  Manage resident Isabelle servers.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   180
""",
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   181
          "L" -> (_ => operation_list = true),
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   182
          "n:" -> (arg => name = arg),
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   183
          "p:" -> (arg => port = Value.Int.parse(arg)))
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   184
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   185
      val more_args = getopts(args)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   186
      if (more_args.nonEmpty) getopts.usage()
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   187
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   188
      if (operation_list) {
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   189
        for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   190
          Output.writeln(entry.toString, stdout = true)
66353
6e114edae18b proper check for active server;
wenzelm
parents: 66352
diff changeset
   191
      }
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   192
      else {
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   193
        val (entry, server) = start(name, port)
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   194
        Output.writeln(entry.toString, stdout = true)
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   195
        server.foreach(_.join)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   196
      }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   197
    })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   198
}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   199
66352
7ed911242266 clarified signature;
wenzelm
parents: 66351
diff changeset
   200
class Server private(_port: Int)
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   201
{
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   202
  server =>
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   203
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   204
  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   205
  def port: Int = server_socket.getLocalPort
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   206
  val password: String = Library.UUID()
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   207
67787
8335d88195c4 clarified toString operations;
wenzelm
parents: 67786
diff changeset
   208
  override def toString: String = Server.print(port, password)
66348
a426e826e84c more options;
wenzelm
parents: 66347
diff changeset
   209
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   210
  private def handle(connection: Server.Connection)
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   211
  {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   212
    connection.read_line() match {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   213
      case None =>
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   214
      case Some(line) if line != password =>
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   215
        connection.reply_error("Bad password -- connection closed")
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   216
      case _ =>
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   217
        var finished = false
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   218
        while (!finished) {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   219
          connection.read_line() match {
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   220
            case None => finished = true
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   221
            case Some(line) =>
67784
543e36ae489c tuned -- avoid regex matching on potentially large string;
wenzelm
parents: 67178
diff changeset
   222
              val cmd = line.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c))
543e36ae489c tuned -- avoid regex matching on potentially large string;
wenzelm
parents: 67178
diff changeset
   223
              val input = line.substring(cmd.length).dropWhile(Symbol.is_ascii_blank(_))
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   224
              Server.commands.get(cmd) match {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   225
                case None => connection.reply_error("Bad command " + quote(cmd))
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   226
                case Some(body) =>
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   227
                  proper_string(input) getOrElse "{}" match {
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   228
                    case JSON.Format(arg) =>
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   229
                      if (body.isDefinedAt((server, arg))) {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   230
                        try { connection.reply_ok(body(server, arg)) }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   231
                        catch { case ERROR(msg) => connection.reply_error(msg) }
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   232
                      }
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   233
                      else {
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   234
                        connection.reply_error_message(
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   235
                          "Bad argument for command", "command" -> cmd, "argument" -> arg)
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   236
                      }
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   237
                    case _ =>
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   238
                      connection.reply_error_message(
66929
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   239
                        "Malformed command-line", "command" -> cmd, "input" -> input)
c19b17b72777 some concrete commands;
wenzelm
parents: 66927
diff changeset
   240
                  }
66921
3d3bd0718ef2 clarified command language;
wenzelm
parents: 66857
diff changeset
   241
              }
3d3bd0718ef2 clarified command language;
wenzelm
parents: 66857
diff changeset
   242
            case _ =>
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   243
          }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   244
        }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   245
    }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   246
  }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   247
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   248
  private lazy val server_thread: Thread =
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   249
    Standard_Thread.fork("server") {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   250
      var finished = false
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   251
      while (!finished) {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   252
        Exn.capture(server_socket.accept) match {
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   253
          case Exn.Res(socket) =>
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   254
            Standard_Thread.fork("server_connection")
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   255
              { using(Server.Connection(socket))(handle(_)) }
66350
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   256
          case Exn.Exn(_) => finished = true
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   257
        }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   258
      }
66331026a2fc handle server connections;
wenzelm
parents: 66349
diff changeset
   259
    }
67785
ad96390ceb5d server commands may access Server;
wenzelm
parents: 67784
diff changeset
   260
67786
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   261
  def join { server_thread.join; shutdown() }
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   262
be6d69595ca7 clarified socket connection;
wenzelm
parents: 67785
diff changeset
   263
  def shutdown() { server_socket.close }
66347
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   264
}