src/Pure/Tools/server.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 66929 c19b17b72777
child 67178 70576478bda9
permissions -rw-r--r--
tuned signature;
wenzelm@66347
     1
/*  Title:      Pure/Tools/server.scala
wenzelm@66347
     2
    Author:     Makarius
wenzelm@66347
     3
wenzelm@66347
     4
Resident Isabelle servers.
wenzelm@66347
     5
*/
wenzelm@66347
     6
wenzelm@66347
     7
package isabelle
wenzelm@66347
     8
wenzelm@66347
     9
wenzelm@66353
    10
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
wenzelm@66353
    11
  IOException}
wenzelm@66350
    12
import java.net.{Socket, ServerSocket, InetAddress}
wenzelm@66347
    13
wenzelm@66347
    14
wenzelm@66347
    15
object Server
wenzelm@66347
    16
{
wenzelm@66927
    17
  /* protocol */
wenzelm@66927
    18
wenzelm@66929
    19
  val commands: Map[String, PartialFunction[JSON.T, JSON.T]] =
wenzelm@66929
    20
    Map(
wenzelm@66929
    21
      "help" -> { case JSON.empty => commands.keySet.toList.sorted },
wenzelm@66929
    22
      "echo" -> { case t => t })
wenzelm@66929
    23
wenzelm@66927
    24
  object Reply extends Enumeration
wenzelm@66927
    25
  {
wenzelm@66927
    26
    val OK, ERROR = Value
wenzelm@66927
    27
  }
wenzelm@66927
    28
wenzelm@66927
    29
wenzelm@66347
    30
  /* per-user servers */
wenzelm@66347
    31
wenzelm@66347
    32
  object Data
wenzelm@66347
    33
  {
wenzelm@66349
    34
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
wenzelm@66347
    35
wenzelm@66857
    36
    val name = SQL.Column.string("name").make_primary_key
wenzelm@66349
    37
    val port = SQL.Column.int("port")
wenzelm@66347
    38
    val password = SQL.Column.string("password")
wenzelm@66349
    39
    val table = SQL.Table("isabelle_servers", List(name, port, password))
wenzelm@66347
    40
wenzelm@66349
    41
    sealed case class Entry(name: String, port: Int, password: String)
wenzelm@66347
    42
    {
wenzelm@66348
    43
      def print: String =
wenzelm@66349
    44
        "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
wenzelm@66353
    45
wenzelm@66353
    46
      def active: Boolean =
wenzelm@66353
    47
        try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
wenzelm@66353
    48
        catch { case _: IOException => false }
wenzelm@66347
    49
    }
wenzelm@66347
    50
  }
wenzelm@66347
    51
wenzelm@66347
    52
  def list(db: SQLite.Database): List[Data.Entry] =
wenzelm@66347
    53
    if (db.tables.contains(Data.table.name)) {
wenzelm@66347
    54
      db.using_statement(Data.table.select())(stmt =>
wenzelm@66347
    55
        stmt.execute_query().iterator(res =>
wenzelm@66347
    56
          Data.Entry(
wenzelm@66349
    57
            res.string(Data.name),
wenzelm@66349
    58
            res.int(Data.port),
wenzelm@66349
    59
            res.string(Data.password))).toList.sortBy(_.name))
wenzelm@66347
    60
    }
wenzelm@66347
    61
    else Nil
wenzelm@66347
    62
wenzelm@66347
    63
  def find(db: SQLite.Database, name: String): Option[Data.Entry] =
wenzelm@66353
    64
    list(db).find(entry => entry.name == name && entry.active)
wenzelm@66347
    65
wenzelm@66352
    66
  def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
wenzelm@66347
    67
  {
wenzelm@66347
    68
    using(SQLite.open_database(Data.database))(db =>
wenzelm@66347
    69
      db.transaction {
wenzelm@66347
    70
        find(db, name) match {
wenzelm@66348
    71
          case Some(entry) => (entry, None)
wenzelm@66347
    72
          case None =>
wenzelm@66352
    73
            val server = new Server(port)
wenzelm@66347
    74
            val entry = Data.Entry(name, server.port, server.password)
wenzelm@66347
    75
wenzelm@66347
    76
            Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
wenzelm@66347
    77
            db.create_table(Data.table)
wenzelm@66353
    78
            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
wenzelm@66347
    79
            db.using_statement(Data.table.insert())(stmt =>
wenzelm@66347
    80
            {
wenzelm@66349
    81
              stmt.string(1) = entry.name
wenzelm@66349
    82
              stmt.int(2) = entry.port
wenzelm@66347
    83
              stmt.string(3) = entry.password
wenzelm@66347
    84
              stmt.execute()
wenzelm@66347
    85
            })
wenzelm@66348
    86
wenzelm@66348
    87
            (entry, Some(server.thread))
wenzelm@66347
    88
        }
wenzelm@66347
    89
      })
wenzelm@66347
    90
  }
wenzelm@66347
    91
wenzelm@66347
    92
  def stop(name: String = ""): Boolean =
wenzelm@66347
    93
  {
wenzelm@66347
    94
    using(SQLite.open_database(Data.database))(db =>
wenzelm@66347
    95
      db.transaction {
wenzelm@66347
    96
        find(db, name) match {
wenzelm@66347
    97
          case Some(entry) =>
wenzelm@66347
    98
            // FIXME shutdown server
wenzelm@66349
    99
            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
wenzelm@66347
   100
            true
wenzelm@66347
   101
          case None =>
wenzelm@66347
   102
            false
wenzelm@66347
   103
        }
wenzelm@66347
   104
      })
wenzelm@66347
   105
  }
wenzelm@66347
   106
wenzelm@66347
   107
wenzelm@66347
   108
  /* Isabelle tool wrapper */
wenzelm@66347
   109
wenzelm@66347
   110
  val isabelle_tool =
wenzelm@66347
   111
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
wenzelm@66347
   112
    {
wenzelm@66348
   113
      var operation_list = false
wenzelm@66348
   114
      var name = ""
wenzelm@66348
   115
      var port = 0
wenzelm@66347
   116
wenzelm@66347
   117
      val getopts =
wenzelm@66347
   118
        Getopts("""
wenzelm@66347
   119
Usage: isabelle server [OPTIONS]
wenzelm@66347
   120
wenzelm@66347
   121
  Options are:
wenzelm@66348
   122
    -L           list servers
wenzelm@66348
   123
    -n NAME      explicit server name
wenzelm@66348
   124
    -p PORT      explicit server port
wenzelm@66347
   125
wenzelm@66347
   126
  Manage resident Isabelle servers.
wenzelm@66347
   127
""",
wenzelm@66348
   128
          "L" -> (_ => operation_list = true),
wenzelm@66348
   129
          "n:" -> (arg => name = arg),
wenzelm@66348
   130
          "p:" -> (arg => port = Value.Int.parse(arg)))
wenzelm@66347
   131
wenzelm@66347
   132
      val more_args = getopts(args)
wenzelm@66348
   133
      if (more_args.nonEmpty) getopts.usage()
wenzelm@66347
   134
wenzelm@66353
   135
      if (operation_list) {
wenzelm@66353
   136
        for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
wenzelm@66353
   137
          Console.println(entry.print)
wenzelm@66353
   138
      }
wenzelm@66348
   139
      else {
wenzelm@66348
   140
        val (entry, thread) = start(name, port)
wenzelm@66348
   141
        Console.println(entry.print)
wenzelm@66348
   142
        thread.foreach(_.join)
wenzelm@66348
   143
      }
wenzelm@66347
   144
    })
wenzelm@66347
   145
}
wenzelm@66347
   146
wenzelm@66352
   147
class Server private(_port: Int)
wenzelm@66347
   148
{
wenzelm@66350
   149
  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
wenzelm@66350
   150
  def port: Int = server_socket.getLocalPort
wenzelm@66350
   151
  def close { server_socket.close }
wenzelm@66350
   152
wenzelm@66352
   153
  val password: String = Library.UUID()
wenzelm@66348
   154
wenzelm@66350
   155
  private def handle_connection(socket: Socket)
wenzelm@66350
   156
  {
wenzelm@66350
   157
    val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
wenzelm@66350
   158
    val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
wenzelm@66350
   159
wenzelm@66927
   160
    def reply_line(msg: String)
wenzelm@66350
   161
    {
wenzelm@66927
   162
      require(split_lines(msg).length <= 1)
wenzelm@66927
   163
      writer.write(msg)
wenzelm@66350
   164
      writer.newLine()
wenzelm@66350
   165
      writer.flush()
wenzelm@66350
   166
    }
wenzelm@66350
   167
wenzelm@66927
   168
    def reply(r: Server.Reply.Value, t: JSON.T)
wenzelm@66927
   169
    {
wenzelm@66927
   170
      reply_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t))
wenzelm@66927
   171
    }
wenzelm@66927
   172
wenzelm@66927
   173
    def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
wenzelm@66927
   174
    def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
wenzelm@66929
   175
    def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
wenzelm@66929
   176
      reply_error(Map("message" -> message) ++ more)
wenzelm@66929
   177
wenzelm@66929
   178
    val Command_Line = """^(\S+)\s*(.*)$""".r
wenzelm@66921
   179
wenzelm@66350
   180
    reader.readLine() match {
wenzelm@66350
   181
      case null =>
wenzelm@66927
   182
      case bad if bad != password => reply_error("Bad password -- connection closed")
wenzelm@66350
   183
      case _ =>
wenzelm@66350
   184
        var finished = false
wenzelm@66350
   185
        while (!finished) {
wenzelm@66350
   186
          reader.readLine() match {
wenzelm@66921
   187
            case null => finished = true
wenzelm@66929
   188
            case Command_Line(cmd, input) =>
wenzelm@66929
   189
              Server.commands.get(cmd) match {
wenzelm@66929
   190
                case None => reply_error("Unknown command " + quote(cmd))
wenzelm@66929
   191
                case Some(body) =>
wenzelm@66929
   192
                  proper_string(input) getOrElse "{}" match {
wenzelm@66929
   193
                    case JSON.Format(arg) =>
wenzelm@66929
   194
                      if (body.isDefinedAt(arg)) {
wenzelm@66929
   195
                        try { reply_ok(body(arg)) }
wenzelm@66929
   196
                        catch { case ERROR(msg) => reply_error(msg) }
wenzelm@66929
   197
                      }
wenzelm@66929
   198
                      else {
wenzelm@66929
   199
                        reply_error_message(
wenzelm@66929
   200
                          "Bad argument for command", "command" -> cmd, "argument" -> arg)
wenzelm@66929
   201
                      }
wenzelm@66929
   202
                    case _ =>
wenzelm@66929
   203
                      reply_error_message(
wenzelm@66929
   204
                        "Malformed command-line", "command" -> cmd, "input" -> input)
wenzelm@66929
   205
                  }
wenzelm@66921
   206
              }
wenzelm@66921
   207
            case _ =>
wenzelm@66350
   208
          }
wenzelm@66350
   209
        }
wenzelm@66350
   210
    }
wenzelm@66350
   211
  }
wenzelm@66350
   212
wenzelm@66350
   213
  lazy val thread: Thread =
wenzelm@66350
   214
    Standard_Thread.fork("server") {
wenzelm@66350
   215
      var finished = false
wenzelm@66350
   216
      while (!finished) {
wenzelm@66350
   217
        Exn.capture(server_socket.accept) match {
wenzelm@66350
   218
          case Exn.Res(socket) =>
wenzelm@66350
   219
            Standard_Thread.fork("server_connection")
wenzelm@66350
   220
              { try { handle_connection(socket) } finally { socket.close } }
wenzelm@66350
   221
          case Exn.Exn(_) => finished = true
wenzelm@66350
   222
        }
wenzelm@66350
   223
      }
wenzelm@66350
   224
    }
wenzelm@66347
   225
}