src/Pure/Tools/server.scala
author wenzelm
Sat, 05 Aug 2017 20:08:41 +0200
changeset 66347 23eaab37e4a8
child 66348 a426e826e84c
permissions -rw-r--r--
support for resident Isabelle servers;
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
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    10
import java.util.UUID
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    11
import java.net.{ServerSocket, InetAddress}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    12
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    13
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    14
object Server
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    15
{
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    16
  /* per-user servers */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    17
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    18
  object Data
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    19
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    20
    val database = Path.explode("$ISABELLE_HOME_USER/server.db")
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    21
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    22
    val server_name = SQL.Column.string("server_name", primary_key = true)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    23
    val server_port = SQL.Column.int("server_port")
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    24
    val password = SQL.Column.string("password")
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    25
    val table = SQL.Table("isabelle_servers", List(server_name, server_port, password))
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    26
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    27
    sealed case class Entry(server_name: String, server_port: Int, password: String)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    28
    {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    29
      def address: String = "127.0.0.1:" + server_port
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    30
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    31
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    32
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    33
  def list(): List[Data.Entry] =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    34
    using(SQLite.open_database(Data.database))(list(_))
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    35
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    36
  def list(db: SQLite.Database): List[Data.Entry] =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    37
    if (db.tables.contains(Data.table.name)) {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    38
      db.using_statement(Data.table.select())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    39
        stmt.execute_query().iterator(res =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    40
          Data.Entry(
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    41
            res.string(Data.server_name),
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    42
            res.int(Data.server_port),
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    43
            res.string(Data.password))).toList.sortBy(_.server_name))
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    44
    }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    45
    else Nil
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    46
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    47
  def find(db: SQLite.Database, name: String): Option[Data.Entry] =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    48
    list(db).find(entry => entry.server_name == name)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    49
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    50
  def start(name: String = "", port: Int = 0): (Data.Entry, Boolean) =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    51
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    52
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    53
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    54
        find(db, name) match {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    55
          case Some(entry) => (entry, false)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    56
          case None =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    57
            val socket = new ServerSocket(port, 50, InetAddress.getByName("127.0.0.1"))
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    58
            val server = new Server(socket)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    59
            val entry = Data.Entry(name, server.port, server.password)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    60
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    61
            Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    62
            db.create_table(Data.table)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    63
            db.using_statement(Data.table.insert())(stmt =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    64
            {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    65
              stmt.string(1) = entry.server_name
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    66
              stmt.int(2) = entry.server_port
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    67
              stmt.string(3) = entry.password
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    68
              stmt.execute()
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    69
            })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    70
            (entry, true)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    71
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    72
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    73
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    74
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    75
  def stop(name: String = ""): Boolean =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    76
  {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    77
    using(SQLite.open_database(Data.database))(db =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    78
      db.transaction {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    79
        find(db, name) match {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    80
          case Some(entry) =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    81
            // FIXME shutdown server
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    82
            db.using_statement(Data.table.delete(Data.server_name.where_equal(name)))(_.execute)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    83
            true
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    84
          case None =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    85
            false
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    86
        }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    87
      })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    88
  }
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    89
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    90
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    91
  /* Isabelle tool wrapper */
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    92
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    93
  val isabelle_tool =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    94
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    95
    {
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    96
      var list_servers = false
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    97
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    98
      val getopts =
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
    99
        Getopts("""
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   100
Usage: isabelle server [OPTIONS]
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   101
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   102
  Options are:
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   103
    -l           list servers
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   104
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   105
  Manage resident Isabelle servers.
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   106
""",
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   107
          "l" -> (_ => list_servers = true))
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   108
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   109
      val more_args = getopts(args)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   110
      if (more_args.nonEmpty || !list_servers) getopts.usage()
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   111
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   112
      if (list_servers) list().foreach(entry =>
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   113
        Console.println("server " + quote(entry.server_name) + " = " + entry.address +
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   114
          " (password " + quote(entry.password) + ")"))
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   115
    })
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   116
}
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   117
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   118
class Server private(val socket: ServerSocket)
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   119
{
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   120
  def port: Int = socket.getLocalPort
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   121
  val password = UUID.randomUUID().toString
23eaab37e4a8 support for resident Isabelle servers;
wenzelm
parents:
diff changeset
   122
}