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