src/Pure/Tools/server.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 66353 6e114edae18b
child 66857 f8f42289c4df
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@66347
    17
  /* per-user servers */
wenzelm@66347
    18
wenzelm@66347
    19
  object Data
wenzelm@66347
    20
  {
wenzelm@66349
    21
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
wenzelm@66347
    22
wenzelm@66349
    23
    val name = SQL.Column.string("name", primary_key = true)
wenzelm@66349
    24
    val port = SQL.Column.int("port")
wenzelm@66347
    25
    val password = SQL.Column.string("password")
wenzelm@66349
    26
    val table = SQL.Table("isabelle_servers", List(name, port, password))
wenzelm@66347
    27
wenzelm@66349
    28
    sealed case class Entry(name: String, port: Int, password: String)
wenzelm@66347
    29
    {
wenzelm@66348
    30
      def print: String =
wenzelm@66349
    31
        "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
wenzelm@66353
    32
wenzelm@66353
    33
      def active: Boolean =
wenzelm@66353
    34
        try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
wenzelm@66353
    35
        catch { case _: IOException => false }
wenzelm@66347
    36
    }
wenzelm@66347
    37
  }
wenzelm@66347
    38
wenzelm@66347
    39
  def list(db: SQLite.Database): List[Data.Entry] =
wenzelm@66347
    40
    if (db.tables.contains(Data.table.name)) {
wenzelm@66347
    41
      db.using_statement(Data.table.select())(stmt =>
wenzelm@66347
    42
        stmt.execute_query().iterator(res =>
wenzelm@66347
    43
          Data.Entry(
wenzelm@66349
    44
            res.string(Data.name),
wenzelm@66349
    45
            res.int(Data.port),
wenzelm@66349
    46
            res.string(Data.password))).toList.sortBy(_.name))
wenzelm@66347
    47
    }
wenzelm@66347
    48
    else Nil
wenzelm@66347
    49
wenzelm@66347
    50
  def find(db: SQLite.Database, name: String): Option[Data.Entry] =
wenzelm@66353
    51
    list(db).find(entry => entry.name == name && entry.active)
wenzelm@66347
    52
wenzelm@66352
    53
  def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
wenzelm@66347
    54
  {
wenzelm@66347
    55
    using(SQLite.open_database(Data.database))(db =>
wenzelm@66347
    56
      db.transaction {
wenzelm@66347
    57
        find(db, name) match {
wenzelm@66348
    58
          case Some(entry) => (entry, None)
wenzelm@66347
    59
          case None =>
wenzelm@66352
    60
            val server = new Server(port)
wenzelm@66347
    61
            val entry = Data.Entry(name, server.port, server.password)
wenzelm@66347
    62
wenzelm@66347
    63
            Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
wenzelm@66347
    64
            db.create_table(Data.table)
wenzelm@66353
    65
            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
wenzelm@66347
    66
            db.using_statement(Data.table.insert())(stmt =>
wenzelm@66347
    67
            {
wenzelm@66349
    68
              stmt.string(1) = entry.name
wenzelm@66349
    69
              stmt.int(2) = entry.port
wenzelm@66347
    70
              stmt.string(3) = entry.password
wenzelm@66347
    71
              stmt.execute()
wenzelm@66347
    72
            })
wenzelm@66348
    73
wenzelm@66348
    74
            (entry, Some(server.thread))
wenzelm@66347
    75
        }
wenzelm@66347
    76
      })
wenzelm@66347
    77
  }
wenzelm@66347
    78
wenzelm@66347
    79
  def stop(name: String = ""): Boolean =
wenzelm@66347
    80
  {
wenzelm@66347
    81
    using(SQLite.open_database(Data.database))(db =>
wenzelm@66347
    82
      db.transaction {
wenzelm@66347
    83
        find(db, name) match {
wenzelm@66347
    84
          case Some(entry) =>
wenzelm@66347
    85
            // FIXME shutdown server
wenzelm@66349
    86
            db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
wenzelm@66347
    87
            true
wenzelm@66347
    88
          case None =>
wenzelm@66347
    89
            false
wenzelm@66347
    90
        }
wenzelm@66347
    91
      })
wenzelm@66347
    92
  }
wenzelm@66347
    93
wenzelm@66347
    94
wenzelm@66347
    95
  /* Isabelle tool wrapper */
wenzelm@66347
    96
wenzelm@66347
    97
  val isabelle_tool =
wenzelm@66347
    98
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
wenzelm@66347
    99
    {
wenzelm@66348
   100
      var operation_list = false
wenzelm@66348
   101
      var name = ""
wenzelm@66348
   102
      var port = 0
wenzelm@66347
   103
wenzelm@66347
   104
      val getopts =
wenzelm@66347
   105
        Getopts("""
wenzelm@66347
   106
Usage: isabelle server [OPTIONS]
wenzelm@66347
   107
wenzelm@66347
   108
  Options are:
wenzelm@66348
   109
    -L           list servers
wenzelm@66348
   110
    -n NAME      explicit server name
wenzelm@66348
   111
    -p PORT      explicit server port
wenzelm@66347
   112
wenzelm@66347
   113
  Manage resident Isabelle servers.
wenzelm@66347
   114
""",
wenzelm@66348
   115
          "L" -> (_ => operation_list = true),
wenzelm@66348
   116
          "n:" -> (arg => name = arg),
wenzelm@66348
   117
          "p:" -> (arg => port = Value.Int.parse(arg)))
wenzelm@66347
   118
wenzelm@66347
   119
      val more_args = getopts(args)
wenzelm@66348
   120
      if (more_args.nonEmpty) getopts.usage()
wenzelm@66347
   121
wenzelm@66353
   122
      if (operation_list) {
wenzelm@66353
   123
        for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
wenzelm@66353
   124
          Console.println(entry.print)
wenzelm@66353
   125
      }
wenzelm@66348
   126
      else {
wenzelm@66348
   127
        val (entry, thread) = start(name, port)
wenzelm@66348
   128
        Console.println(entry.print)
wenzelm@66348
   129
        thread.foreach(_.join)
wenzelm@66348
   130
      }
wenzelm@66347
   131
    })
wenzelm@66347
   132
}
wenzelm@66347
   133
wenzelm@66352
   134
class Server private(_port: Int)
wenzelm@66347
   135
{
wenzelm@66350
   136
  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
wenzelm@66350
   137
  def port: Int = server_socket.getLocalPort
wenzelm@66350
   138
  def close { server_socket.close }
wenzelm@66350
   139
wenzelm@66352
   140
  val password: String = Library.UUID()
wenzelm@66348
   141
wenzelm@66350
   142
  private def handle_connection(socket: Socket)
wenzelm@66350
   143
  {
wenzelm@66350
   144
    val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
wenzelm@66350
   145
    val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
wenzelm@66350
   146
wenzelm@66350
   147
    def println(s: String)
wenzelm@66350
   148
    {
wenzelm@66350
   149
      writer.write(s)
wenzelm@66350
   150
      writer.newLine()
wenzelm@66350
   151
      writer.flush()
wenzelm@66350
   152
    }
wenzelm@66350
   153
wenzelm@66350
   154
    reader.readLine() match {
wenzelm@66350
   155
      case null =>
wenzelm@66350
   156
      case bad if bad != password => println("BAD PASSWORD")
wenzelm@66350
   157
      case _ =>
wenzelm@66350
   158
        var finished = false
wenzelm@66350
   159
        while (!finished) {
wenzelm@66350
   160
          reader.readLine() match {
wenzelm@66350
   161
            case null => println("FINISHED"); finished = true
wenzelm@66350
   162
            case line => println("ECHO " + line)
wenzelm@66350
   163
          }
wenzelm@66350
   164
        }
wenzelm@66350
   165
    }
wenzelm@66350
   166
  }
wenzelm@66350
   167
wenzelm@66350
   168
  lazy val thread: Thread =
wenzelm@66350
   169
    Standard_Thread.fork("server") {
wenzelm@66350
   170
      var finished = false
wenzelm@66350
   171
      while (!finished) {
wenzelm@66350
   172
        Exn.capture(server_socket.accept) match {
wenzelm@66350
   173
          case Exn.Res(socket) =>
wenzelm@66350
   174
            Standard_Thread.fork("server_connection")
wenzelm@66350
   175
              { try { handle_connection(socket) } finally { socket.close } }
wenzelm@66350
   176
          case Exn.Exn(_) => finished = true
wenzelm@66350
   177
        }
wenzelm@66350
   178
      }
wenzelm@66350
   179
    }
wenzelm@66347
   180
}