src/Pure/Tools/server.scala
author wenzelm
Sat Jun 09 21:52:16 2018 +0200 (12 months ago)
changeset 68410 4e27f5c361d2
parent 67941 49a34b2fa788
child 68530 a110dcc9a4c7
permissions -rw-r--r--
clarified signature: more uniform theory_message (see also d7920eb7de54);
wenzelm@66347
     1
/*  Title:      Pure/Tools/server.scala
wenzelm@66347
     2
    Author:     Makarius
wenzelm@66347
     3
wenzelm@66347
     4
Resident Isabelle servers.
wenzelm@67809
     5
wenzelm@67809
     6
Message formats:
wenzelm@67809
     7
  - short message (single line):
wenzelm@67809
     8
      NAME ARGUMENT
wenzelm@67809
     9
  - long message (multiple lines):
wenzelm@67809
    10
      BYTE_LENGTH
wenzelm@67809
    11
      NAME ARGUMENT
wenzelm@67820
    12
wenzelm@67820
    13
Argument formats:
wenzelm@67820
    14
  - Unit as empty string
wenzelm@67820
    15
  - XML.Elem in YXML notation
wenzelm@67820
    16
  - JSON.T in standard notation
wenzelm@66347
    17
*/
wenzelm@66347
    18
wenzelm@66347
    19
package isabelle
wenzelm@66347
    20
wenzelm@66347
    21
wenzelm@67837
    22
import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter,
wenzelm@67837
    23
  IOException}
wenzelm@67797
    24
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress}
wenzelm@66347
    25
wenzelm@66347
    26
wenzelm@66347
    27
object Server
wenzelm@66347
    28
{
wenzelm@67820
    29
  /* message argument */
wenzelm@66927
    30
wenzelm@67820
    31
  object Argument
wenzelm@67794
    32
  {
wenzelm@67903
    33
    def is_name_char(c: Char): Boolean =
wenzelm@67903
    34
      Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.'
wenzelm@67903
    35
wenzelm@67820
    36
    def split(msg: String): (String, String) =
wenzelm@67820
    37
    {
wenzelm@67903
    38
      val name = msg.takeWhile(is_name_char(_))
wenzelm@67820
    39
      val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_))
wenzelm@67820
    40
      (name, argument)
wenzelm@67820
    41
    }
wenzelm@67820
    42
wenzelm@67820
    43
    def print(arg: Any): String =
wenzelm@67820
    44
      arg match {
wenzelm@67820
    45
        case () => ""
wenzelm@67820
    46
        case t: XML.Elem => YXML.string_of_tree(t)
wenzelm@67820
    47
        case t: JSON.T => JSON.Format(t)
wenzelm@67820
    48
      }
wenzelm@67820
    49
wenzelm@67820
    50
    def parse(argument: String): Any =
wenzelm@67820
    51
      if (argument == "") ()
wenzelm@67820
    52
      else if (YXML.detect_elem(argument)) YXML.parse_elem(argument)
wenzelm@67820
    53
      else JSON.parse(argument, strict = false)
wenzelm@67820
    54
wenzelm@67820
    55
    def unapply(argument: String): Option[Any] =
wenzelm@67820
    56
      try { Some(parse(argument)) }
wenzelm@67820
    57
      catch { case ERROR(_) => None }
wenzelm@67794
    58
  }
wenzelm@67794
    59
wenzelm@67820
    60
wenzelm@67820
    61
  /* input command */
wenzelm@67820
    62
wenzelm@67820
    63
  object Command
wenzelm@67820
    64
  {
wenzelm@67839
    65
    type T = PartialFunction[(Context, Any), Any]
wenzelm@67820
    66
wenzelm@67820
    67
    private val table: Map[String, T] =
wenzelm@67820
    68
      Map(
wenzelm@67848
    69
        "help" -> { case (_, ()) => table.keySet.toList.sorted },
wenzelm@67820
    70
        "echo" -> { case (_, t) => t },
wenzelm@67902
    71
        "shutdown" -> { case (context, ()) => context.server.shutdown() },
wenzelm@67920
    72
        "cancel" ->
wenzelm@67920
    73
          { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
wenzelm@67848
    74
        "session_build" ->
wenzelm@67848
    75
          { case (context, Server_Commands.Session_Build(args)) =>
wenzelm@67861
    76
              context.make_task(task =>
wenzelm@67886
    77
                Server_Commands.Session_Build.command(args, progress = task.progress)._1)
wenzelm@67869
    78
          },
wenzelm@67869
    79
        "session_start" ->
wenzelm@67869
    80
          { case (context, Server_Commands.Session_Start(args)) =>
wenzelm@67869
    81
              context.make_task(task =>
wenzelm@67869
    82
                {
wenzelm@67871
    83
                  val (res, entry) =
wenzelm@67878
    84
                    Server_Commands.Session_Start.command(
wenzelm@67886
    85
                      args, progress = task.progress, log = context.server.log)
wenzelm@67878
    86
                  context.server.add_session(entry)
wenzelm@67869
    87
                  res
wenzelm@67869
    88
                })
wenzelm@67871
    89
          },
wenzelm@67871
    90
        "session_stop" ->
wenzelm@67871
    91
          { case (context, Server_Commands.Session_Stop(id)) =>
wenzelm@67871
    92
              context.make_task(_ =>
wenzelm@67871
    93
                {
wenzelm@67878
    94
                  val session = context.server.remove_session(id)
wenzelm@67871
    95
                  Server_Commands.Session_Stop.command(session)._1
wenzelm@67871
    96
                })
wenzelm@67883
    97
          },
wenzelm@67883
    98
        "use_theories" ->
wenzelm@67883
    99
          { case (context, Server_Commands.Use_Theories(args)) =>
wenzelm@67883
   100
              context.make_task(task =>
wenzelm@67883
   101
                {
wenzelm@67883
   102
                  val session = context.server.the_session(args.session_id)
wenzelm@67884
   103
                  Server_Commands.Use_Theories.command(
wenzelm@67884
   104
                    args, session, id = task.id, progress = task.progress)._1
wenzelm@67941
   105
                }),
wenzelm@67941
   106
          },
wenzelm@67941
   107
        "purge_theories" ->
wenzelm@67941
   108
          { case (context, Server_Commands.Purge_Theories(args)) =>
wenzelm@67941
   109
              val session = context.server.the_session(args.session_id)
wenzelm@67941
   110
              Server_Commands.Purge_Theories.command(args, session)._1
wenzelm@67848
   111
          })
wenzelm@67820
   112
wenzelm@67820
   113
    def unapply(name: String): Option[T] = table.get(name)
wenzelm@67820
   114
  }
wenzelm@67820
   115
wenzelm@67820
   116
wenzelm@67820
   117
  /* output reply */
wenzelm@66929
   118
wenzelm@67857
   119
  class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty)
wenzelm@67857
   120
    extends RuntimeException(message)
wenzelm@67857
   121
wenzelm@67891
   122
  def json_error(exn: Throwable): JSON.Object.T =
wenzelm@67891
   123
    exn match {
wenzelm@67913
   124
      case e: Error => Reply.error_message(e.message) ++ e.json
wenzelm@67901
   125
      case ERROR(msg) => Reply.error_message(msg)
wenzelm@67901
   126
      case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
wenzelm@67891
   127
      case _ => JSON.Object.empty
wenzelm@67891
   128
    }
wenzelm@67891
   129
wenzelm@66927
   130
  object Reply extends Enumeration
wenzelm@66927
   131
  {
wenzelm@67860
   132
    val OK, ERROR, FINISHED, FAILED, NOTE = Value
wenzelm@67800
   133
wenzelm@67901
   134
    def message(msg: String, kind: String = ""): JSON.Object.T =
wenzelm@67931
   135
      JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg)
wenzelm@67901
   136
wenzelm@67901
   137
    def error_message(msg: String): JSON.Object.T =
wenzelm@67911
   138
      message(msg, kind = Markup.ERROR)
wenzelm@67857
   139
wenzelm@67820
   140
    def unapply(msg: String): Option[(Reply.Value, Any)] =
wenzelm@67800
   141
    {
wenzelm@67809
   142
      if (msg == "") None
wenzelm@67800
   143
      else {
wenzelm@67820
   144
        val (name, argument) = Argument.split(msg)
wenzelm@67820
   145
        for {
wenzelm@67820
   146
          reply <-
wenzelm@67820
   147
            try { Some(withName(name)) }
wenzelm@67820
   148
            catch { case _: NoSuchElementException => None }
wenzelm@67820
   149
          arg <- Argument.unapply(argument)
wenzelm@67820
   150
        } yield (reply, arg)
wenzelm@67800
   151
      }
wenzelm@67800
   152
    }
wenzelm@66927
   153
  }
wenzelm@66927
   154
wenzelm@66927
   155
wenzelm@67786
   156
  /* socket connection */
wenzelm@67786
   157
wenzelm@67786
   158
  object Connection
wenzelm@67786
   159
  {
wenzelm@67786
   160
    def apply(socket: Socket): Connection =
wenzelm@67786
   161
      new Connection(socket)
wenzelm@67786
   162
  }
wenzelm@67786
   163
wenzelm@67832
   164
  class Connection private(socket: Socket)
wenzelm@67786
   165
  {
wenzelm@67786
   166
    override def toString: String = socket.toString
wenzelm@67786
   167
wenzelm@67786
   168
    def close() { socket.close }
wenzelm@67786
   169
wenzelm@67832
   170
    def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) }
wenzelm@67832
   171
wenzelm@67832
   172
    private val in = new BufferedInputStream(socket.getInputStream)
wenzelm@67832
   173
    private val out = new BufferedOutputStream(socket.getOutputStream)
wenzelm@67839
   174
    private val out_lock: AnyRef = new Object
wenzelm@67786
   175
wenzelm@67837
   176
    def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop =
wenzelm@67839
   177
      new TTY_Loop(
wenzelm@67839
   178
        new OutputStreamWriter(out),
wenzelm@67839
   179
        new InputStreamReader(in),
wenzelm@67839
   180
        writer_lock = out_lock,
wenzelm@67839
   181
        interrupt = interrupt)
wenzelm@67837
   182
wenzelm@67809
   183
    def read_message(): Option[String] =
wenzelm@67809
   184
      try {
wenzelm@67809
   185
        Bytes.read_line(in).map(_.text) match {
wenzelm@67809
   186
          case Some(Value.Int(n)) =>
wenzelm@67809
   187
            Bytes.read_block(in, n).map(bytes => Library.trim_line(bytes.text))
wenzelm@67809
   188
          case res => res
wenzelm@67809
   189
        }
wenzelm@67809
   190
      }
wenzelm@67805
   191
      catch { case _: SocketException => None }
wenzelm@67786
   192
wenzelm@67839
   193
    def write_message(msg: String): Unit = out_lock.synchronized
wenzelm@67786
   194
    {
wenzelm@67809
   195
      val b = UTF8.bytes(msg)
wenzelm@67809
   196
      if (b.length > 100 || b.contains(10)) {
wenzelm@67809
   197
        out.write(UTF8.bytes((b.length + 1).toString))
wenzelm@67809
   198
        out.write(10)
wenzelm@67809
   199
      }
wenzelm@67809
   200
      out.write(b)
wenzelm@67805
   201
      out.write(10)
wenzelm@67805
   202
      try { out.flush() } catch { case _: SocketException => }
wenzelm@67786
   203
    }
wenzelm@67786
   204
wenzelm@67859
   205
    def reply(r: Reply.Value, arg: Any)
wenzelm@67786
   206
    {
wenzelm@67820
   207
      val argument = Argument.print(arg)
wenzelm@67820
   208
      write_message(if (argument == "") r.toString else r.toString + " " + argument)
wenzelm@67786
   209
    }
wenzelm@67786
   210
wenzelm@67859
   211
    def reply_ok(arg: Any) { reply(Reply.OK, arg) }
wenzelm@67859
   212
    def reply_error(arg: Any) { reply(Reply.ERROR, arg) }
wenzelm@67857
   213
    def reply_error_message(message: String, more: JSON.Object.Entry*): Unit =
wenzelm@67901
   214
      reply_error(Reply.error_message(message) ++ more)
wenzelm@67801
   215
wenzelm@67859
   216
    def notify(arg: Any) { reply(Reply.NOTE, arg) }
wenzelm@67839
   217
  }
wenzelm@67839
   218
wenzelm@67839
   219
wenzelm@67839
   220
  /* context with output channels */
wenzelm@67839
   221
wenzelm@67878
   222
  class Context private[Server](val server: Server, connection: Connection)
wenzelm@67839
   223
  {
wenzelm@67839
   224
    context =>
wenzelm@67839
   225
wenzelm@67859
   226
    def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) }
wenzelm@67840
   227
    def notify(arg: Any) { connection.notify(arg) }
wenzelm@67857
   228
    def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit =
wenzelm@67901
   229
      notify(Reply.message(msg, kind = kind) ++ more)
wenzelm@67857
   230
    def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
wenzelm@67857
   231
    def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
wenzelm@67857
   232
    def error_message(msg: String, more: JSON.Object.Entry*): Unit =
wenzelm@67911
   233
      message(Markup.ERROR, msg, more:_*)
wenzelm@67839
   234
wenzelm@67860
   235
    def progress(more: JSON.Object.Entry*): Connection_Progress =
wenzelm@67860
   236
      new Connection_Progress(context, more:_*)
wenzelm@67839
   237
wenzelm@67839
   238
    override def toString: String = connection.toString
wenzelm@67860
   239
wenzelm@67860
   240
wenzelm@67860
   241
    /* asynchronous tasks */
wenzelm@67860
   242
wenzelm@67860
   243
    private val _tasks = Synchronized(Set.empty[Task])
wenzelm@67860
   244
wenzelm@67860
   245
    def make_task(body: Task => JSON.Object.T): Task =
wenzelm@67860
   246
    {
wenzelm@67860
   247
      val task = new Task(context, body)
wenzelm@67860
   248
      _tasks.change(_ + task)
wenzelm@67860
   249
      task
wenzelm@67860
   250
    }
wenzelm@67860
   251
wenzelm@67860
   252
    def remove_task(task: Task): Unit =
wenzelm@67860
   253
      _tasks.change(_ - task)
wenzelm@67860
   254
wenzelm@67885
   255
    def cancel_task(id: UUID): Unit =
wenzelm@67860
   256
      _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
wenzelm@67860
   257
wenzelm@67860
   258
    def close()
wenzelm@67860
   259
    {
wenzelm@67860
   260
      while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) }))
wenzelm@67860
   261
      { _tasks.value.foreach(_.join) }
wenzelm@67860
   262
    }
wenzelm@67839
   263
  }
wenzelm@67839
   264
wenzelm@67860
   265
  class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*)
wenzelm@67860
   266
    extends Progress
wenzelm@67839
   267
  {
wenzelm@67860
   268
    override def echo(msg: String): Unit = context.writeln(msg, more:_*)
wenzelm@67860
   269
    override def echo_warning(msg: String): Unit = context.warning(msg, more:_*)
wenzelm@67860
   270
    override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*)
wenzelm@67839
   271
    override def theory(session: String, theory: String): Unit =
wenzelm@68410
   272
      context.writeln(Progress.theory_message(session, theory),
wenzelm@67860
   273
        (List("session" -> session, "theory" -> theory) ::: more.toList):_*)
wenzelm@67839
   274
wenzelm@67839
   275
    @volatile private var is_stopped = false
wenzelm@67839
   276
    override def stopped: Boolean = is_stopped
wenzelm@67839
   277
    def stop { is_stopped = true }
wenzelm@67839
   278
wenzelm@67839
   279
    override def toString: String = context.toString
wenzelm@67786
   280
  }
wenzelm@67786
   281
wenzelm@67860
   282
  class Task private[Server](val context: Context, body: Task => JSON.Object.T)
wenzelm@67860
   283
  {
wenzelm@67860
   284
    task =>
wenzelm@67860
   285
wenzelm@67885
   286
    val id: UUID = UUID()
wenzelm@67885
   287
    val ident: JSON.Object.Entry = ("task" -> id.toString)
wenzelm@67860
   288
wenzelm@67860
   289
    val progress: Connection_Progress = context.progress(ident)
wenzelm@67860
   290
    def cancel { progress.stop }
wenzelm@67860
   291
wenzelm@67860
   292
    private lazy val thread = Standard_Thread.fork("server_task")
wenzelm@67860
   293
    {
wenzelm@67860
   294
      Exn.capture { body(task) } match {
wenzelm@67860
   295
        case Exn.Res(res) =>
wenzelm@67860
   296
          context.reply(Reply.FINISHED, res + ident)
wenzelm@67891
   297
        case Exn.Exn(exn) =>
wenzelm@67891
   298
          val err = json_error(exn)
wenzelm@67891
   299
          if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident)
wenzelm@67860
   300
      }
wenzelm@67860
   301
      progress.stop
wenzelm@67860
   302
      context.remove_task(task)
wenzelm@67860
   303
    }
wenzelm@67860
   304
    def start { thread }
wenzelm@67860
   305
    def join { thread.join }
wenzelm@67860
   306
  }
wenzelm@67860
   307
wenzelm@67786
   308
wenzelm@67807
   309
  /* server info */
wenzelm@67807
   310
wenzelm@67807
   311
  sealed case class Info(name: String, port: Int, password: String)
wenzelm@67807
   312
  {
wenzelm@67807
   313
    override def toString: String =
wenzelm@67821
   314
      "server " + quote(name) + " = " + print(port, password)
wenzelm@67807
   315
wenzelm@67807
   316
    def connection(): Connection =
wenzelm@67807
   317
    {
wenzelm@67807
   318
      val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port))
wenzelm@67809
   319
      connection.write_message(password)
wenzelm@67807
   320
      connection
wenzelm@67807
   321
    }
wenzelm@67807
   322
wenzelm@67807
   323
    def active(): Boolean =
wenzelm@67807
   324
      try {
wenzelm@67807
   325
        using(connection())(connection =>
wenzelm@67807
   326
          {
wenzelm@67832
   327
            connection.set_timeout(Time.seconds(2.0))
wenzelm@67867
   328
            connection.read_message() match {
wenzelm@67867
   329
              case Some(Reply(Reply.OK, _)) => true
wenzelm@67867
   330
              case _ => false
wenzelm@67867
   331
            }
wenzelm@67807
   332
          })
wenzelm@67807
   333
      }
wenzelm@67807
   334
      catch {
wenzelm@67807
   335
        case _: IOException => false
wenzelm@67807
   336
        case _: SocketException => false
wenzelm@67807
   337
        case _: SocketTimeoutException => false
wenzelm@67807
   338
      }
wenzelm@67807
   339
  }
wenzelm@67807
   340
wenzelm@67807
   341
wenzelm@66347
   342
  /* per-user servers */
wenzelm@66347
   343
wenzelm@67822
   344
  val default_name = "isabelle"
wenzelm@67822
   345
wenzelm@67787
   346
  def print(port: Int, password: String): String =
wenzelm@67787
   347
    "127.0.0.1:" + port + " (password " + quote(password) + ")"
wenzelm@67787
   348
wenzelm@66347
   349
  object Data
wenzelm@66347
   350
  {
wenzelm@66349
   351
    val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
wenzelm@66347
   352
wenzelm@66857
   353
    val name = SQL.Column.string("name").make_primary_key
wenzelm@66349
   354
    val port = SQL.Column.int("port")
wenzelm@66347
   355
    val password = SQL.Column.string("password")
wenzelm@66349
   356
    val table = SQL.Table("isabelle_servers", List(name, port, password))
wenzelm@66347
   357
  }
wenzelm@66347
   358
wenzelm@67807
   359
  def list(db: SQLite.Database): List[Info] =
wenzelm@66347
   360
    if (db.tables.contains(Data.table.name)) {
wenzelm@66347
   361
      db.using_statement(Data.table.select())(stmt =>
wenzelm@66347
   362
        stmt.execute_query().iterator(res =>
wenzelm@67807
   363
          Info(
wenzelm@66349
   364
            res.string(Data.name),
wenzelm@66349
   365
            res.int(Data.port),
wenzelm@66349
   366
            res.string(Data.password))).toList.sortBy(_.name))
wenzelm@66347
   367
    }
wenzelm@66347
   368
    else Nil
wenzelm@66347
   369
wenzelm@67807
   370
  def find(db: SQLite.Database, name: String): Option[Info] =
wenzelm@67807
   371
    list(db).find(server_info => server_info.name == name && server_info.active)
wenzelm@66347
   372
wenzelm@67870
   373
  def init(
wenzelm@67870
   374
    name: String = default_name,
wenzelm@67870
   375
    port: Int = 0,
wenzelm@67870
   376
    existing_server: Boolean = false,
wenzelm@67870
   377
    log: Logger = No_Logger): (Info, Option[Server]) =
wenzelm@66347
   378
  {
wenzelm@66347
   379
    using(SQLite.open_database(Data.database))(db =>
wenzelm@67799
   380
      {
wenzelm@67799
   381
        db.transaction {
wenzelm@67799
   382
          Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
wenzelm@67799
   383
          db.create_table(Data.table)
wenzelm@67807
   384
          list(db).filterNot(_.active).foreach(server_info =>
wenzelm@67807
   385
            db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))(
wenzelm@67807
   386
              _.execute))
wenzelm@67799
   387
        }
wenzelm@67799
   388
        db.transaction {
wenzelm@67799
   389
          find(db, name) match {
wenzelm@67807
   390
            case Some(server_info) => (server_info, None)
wenzelm@67799
   391
            case None =>
wenzelm@67821
   392
              if (existing_server) error("Isabelle server " + quote(name) + " not running")
wenzelm@67811
   393
wenzelm@67870
   394
              val server = new Server(port, log)
wenzelm@67807
   395
              val server_info = Info(name, server.port, server.password)
wenzelm@66347
   396
wenzelm@67799
   397
              db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
wenzelm@67799
   398
              db.using_statement(Data.table.insert())(stmt =>
wenzelm@67799
   399
              {
wenzelm@67807
   400
                stmt.string(1) = server_info.name
wenzelm@67807
   401
                stmt.int(2) = server_info.port
wenzelm@67807
   402
                stmt.string(3) = server_info.password
wenzelm@67799
   403
                stmt.execute()
wenzelm@67799
   404
              })
wenzelm@66348
   405
wenzelm@67799
   406
              server.start
wenzelm@67807
   407
              (server_info, Some(server))
wenzelm@67799
   408
          }
wenzelm@66347
   409
        }
wenzelm@66347
   410
      })
wenzelm@66347
   411
  }
wenzelm@66347
   412
wenzelm@67822
   413
  def exit(name: String = default_name): Boolean =
wenzelm@66347
   414
  {
wenzelm@66347
   415
    using(SQLite.open_database(Data.database))(db =>
wenzelm@66347
   416
      db.transaction {
wenzelm@66347
   417
        find(db, name) match {
wenzelm@67807
   418
          case Some(server_info) =>
wenzelm@67809
   419
            using(server_info.connection())(_.write_message("shutdown"))
wenzelm@67807
   420
            while(server_info.active) { Thread.sleep(50) }
wenzelm@66347
   421
            true
wenzelm@67785
   422
          case None => false
wenzelm@66347
   423
        }
wenzelm@66347
   424
      })
wenzelm@66347
   425
  }
wenzelm@66347
   426
wenzelm@66347
   427
wenzelm@66347
   428
  /* Isabelle tool wrapper */
wenzelm@66347
   429
wenzelm@66347
   430
  val isabelle_tool =
wenzelm@66347
   431
    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
wenzelm@66347
   432
    {
wenzelm@67806
   433
      var console = false
wenzelm@67870
   434
      var log_file: Option[Path] = None
wenzelm@66348
   435
      var operation_list = false
wenzelm@67823
   436
      var operation_exit = false
wenzelm@67822
   437
      var name = default_name
wenzelm@66348
   438
      var port = 0
wenzelm@67811
   439
      var existing_server = false
wenzelm@66347
   440
wenzelm@66347
   441
      val getopts =
wenzelm@66347
   442
        Getopts("""
wenzelm@66347
   443
Usage: isabelle server [OPTIONS]
wenzelm@66347
   444
wenzelm@66347
   445
  Options are:
wenzelm@67870
   446
    -L FILE      logging on FILE
wenzelm@67875
   447
    -c           console interaction with specified server
wenzelm@67904
   448
    -l           list servers (alternative operation)
wenzelm@67822
   449
    -n NAME      explicit server name (default: """ + default_name + """)
wenzelm@66348
   450
    -p PORT      explicit server port
wenzelm@67811
   451
    -s           assume existing server, no implicit startup
wenzelm@67904
   452
    -x           exit specified server (alternative operation)
wenzelm@66347
   453
wenzelm@66347
   454
  Manage resident Isabelle servers.
wenzelm@66347
   455
""",
wenzelm@67870
   456
          "L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))),
wenzelm@67875
   457
          "c" -> (_ => console = true),
wenzelm@67870
   458
          "l" -> (_ => operation_list = true),
wenzelm@66348
   459
          "n:" -> (arg => name = arg),
wenzelm@67811
   460
          "p:" -> (arg => port = Value.Int.parse(arg)),
wenzelm@67870
   461
          "s" -> (_ => existing_server = true),
wenzelm@67876
   462
          "x" -> (_ => operation_exit = true))
wenzelm@66347
   463
wenzelm@66347
   464
      val more_args = getopts(args)
wenzelm@66348
   465
      if (more_args.nonEmpty) getopts.usage()
wenzelm@66347
   466
wenzelm@66353
   467
      if (operation_list) {
wenzelm@67807
   468
        for {
wenzelm@67807
   469
          server_info <- using(SQLite.open_database(Data.database))(list(_))
wenzelm@67807
   470
          if server_info.active
wenzelm@67807
   471
        } Output.writeln(server_info.toString, stdout = true)
wenzelm@66353
   472
      }
wenzelm@67823
   473
      else if (operation_exit) {
wenzelm@67823
   474
        val ok = Server.exit(name)
wenzelm@67823
   475
        sys.exit(if (ok) 0 else 1)
wenzelm@67823
   476
      }
wenzelm@66348
   477
      else {
wenzelm@67870
   478
        val log = Logger.make(log_file)
wenzelm@67870
   479
        val (server_info, server) =
wenzelm@67870
   480
          init(name, port = port, existing_server = existing_server, log = log)
wenzelm@67807
   481
        Output.writeln(server_info.toString, stdout = true)
wenzelm@67834
   482
        if (console) {
wenzelm@67834
   483
          using(server_info.connection())(connection => connection.tty_loop().join)
wenzelm@67834
   484
        }
wenzelm@67785
   485
        server.foreach(_.join)
wenzelm@66348
   486
      }
wenzelm@66347
   487
    })
wenzelm@66347
   488
}
wenzelm@66347
   489
wenzelm@67870
   490
class Server private(_port: Int, val log: Logger)
wenzelm@66347
   491
{
wenzelm@67785
   492
  server =>
wenzelm@67785
   493
wenzelm@67902
   494
  private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
wenzelm@67902
   495
wenzelm@67885
   496
  private val _sessions = Synchronized(Map.empty[UUID, Thy_Resources.Session])
wenzelm@67885
   497
  def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
wenzelm@67885
   498
  def the_session(id: UUID): Thy_Resources.Session =
wenzelm@67883
   499
    _sessions.value.get(id) getOrElse err_session(id)
wenzelm@67885
   500
  def add_session(entry: (UUID, Thy_Resources.Session)) { _sessions.change(_ + entry) }
wenzelm@67885
   501
  def remove_session(id: UUID): Thy_Resources.Session =
wenzelm@67871
   502
  {
wenzelm@67871
   503
    _sessions.change_result(sessions =>
wenzelm@67871
   504
      sessions.get(id) match {
wenzelm@67871
   505
        case Some(session) => (session, sessions - id)
wenzelm@67883
   506
        case None => err_session(id)
wenzelm@67871
   507
      })
wenzelm@67871
   508
  }
wenzelm@67871
   509
wenzelm@67902
   510
  def shutdown()
wenzelm@67902
   511
  {
wenzelm@67902
   512
    server_socket.close
wenzelm@67791
   513
wenzelm@67902
   514
    val sessions = _sessions.change_result(sessions => (sessions, Map.empty))
wenzelm@67902
   515
    for ((_, session) <- sessions) {
wenzelm@67902
   516
      try {
wenzelm@67902
   517
        val result = session.stop()
wenzelm@67902
   518
        if (!result.ok) log("Session shutdown failed: return code " + result.rc)
wenzelm@67902
   519
      }
wenzelm@67902
   520
      catch { case ERROR(msg) => log("Session shutdown failed: " + msg) }
wenzelm@67902
   521
    }
wenzelm@67902
   522
  }
wenzelm@67791
   523
wenzelm@66350
   524
  def port: Int = server_socket.getLocalPort
wenzelm@67885
   525
  val password: String = UUID().toString
wenzelm@66350
   526
wenzelm@67787
   527
  override def toString: String = Server.print(port, password)
wenzelm@66348
   528
wenzelm@67786
   529
  private def handle(connection: Server.Connection)
wenzelm@66350
   530
  {
wenzelm@67860
   531
    using(new Server.Context(server, connection))(context =>
wenzelm@67860
   532
    {
wenzelm@67860
   533
      connection.read_message() match {
wenzelm@67860
   534
        case Some(msg) if msg == password =>
wenzelm@67867
   535
          connection.reply_ok(
wenzelm@67867
   536
            JSON.Object(
wenzelm@67867
   537
              "isabelle_id" -> Isabelle_System.isabelle_id(),
wenzelm@67867
   538
              "isabelle_version" -> Distribution.version))
wenzelm@67867
   539
wenzelm@67860
   540
          var finished = false
wenzelm@67860
   541
          while (!finished) {
wenzelm@67860
   542
            connection.read_message() match {
wenzelm@67860
   543
              case None => finished = true
wenzelm@67860
   544
              case Some("") => context.notify("Command 'help' provides list of commands")
wenzelm@67860
   545
              case Some(msg) =>
wenzelm@67860
   546
                val (name, argument) = Server.Argument.split(msg)
wenzelm@67860
   547
                name match {
wenzelm@67860
   548
                  case Server.Command(cmd) =>
wenzelm@67860
   549
                    argument match {
wenzelm@67860
   550
                      case Server.Argument(arg) =>
wenzelm@67860
   551
                        if (cmd.isDefinedAt((context, arg))) {
wenzelm@67860
   552
                          Exn.capture { cmd((context, arg)) } match {
wenzelm@67860
   553
                            case Exn.Res(task: Server.Task) =>
wenzelm@67860
   554
                              connection.reply_ok(JSON.Object(task.ident))
wenzelm@67860
   555
                              task.start
wenzelm@67860
   556
                            case Exn.Res(res) => connection.reply_ok(res)
wenzelm@67891
   557
                            case Exn.Exn(exn) =>
wenzelm@67891
   558
                              val err = Server.json_error(exn)
wenzelm@67891
   559
                              if (err.isEmpty) throw exn else connection.reply_error(err)
wenzelm@67860
   560
                          }
wenzelm@67820
   561
                        }
wenzelm@67860
   562
                        else {
wenzelm@67860
   563
                          connection.reply_error_message(
wenzelm@67860
   564
                            "Bad argument for command " + Library.single_quote(name),
wenzelm@67860
   565
                            "argument" -> argument)
wenzelm@67860
   566
                        }
wenzelm@67860
   567
                      case _ =>
wenzelm@67786
   568
                        connection.reply_error_message(
wenzelm@67860
   569
                          "Malformed argument for command " + Library.single_quote(name),
wenzelm@67820
   570
                          "argument" -> argument)
wenzelm@67860
   571
                    }
wenzelm@67860
   572
                  case _ => connection.reply_error("Bad command " + Library.single_quote(name))
wenzelm@67860
   573
                }
wenzelm@67860
   574
            }
wenzelm@66350
   575
          }
wenzelm@67860
   576
        case _ =>
wenzelm@67860
   577
      }
wenzelm@67860
   578
    })
wenzelm@66350
   579
  }
wenzelm@66350
   580
wenzelm@67786
   581
  private lazy val server_thread: Thread =
wenzelm@66350
   582
    Standard_Thread.fork("server") {
wenzelm@66350
   583
      var finished = false
wenzelm@66350
   584
      while (!finished) {
wenzelm@66350
   585
        Exn.capture(server_socket.accept) match {
wenzelm@66350
   586
          case Exn.Res(socket) =>
wenzelm@66350
   587
            Standard_Thread.fork("server_connection")
wenzelm@67786
   588
              { using(Server.Connection(socket))(handle(_)) }
wenzelm@66350
   589
          case Exn.Exn(_) => finished = true
wenzelm@66350
   590
        }
wenzelm@66350
   591
      }
wenzelm@66350
   592
    }
wenzelm@67785
   593
wenzelm@67790
   594
  def start { server_thread }
wenzelm@67790
   595
wenzelm@67902
   596
  def join { server_thread.join; shutdown() }
wenzelm@66347
   597
}