support for resident Isabelle servers;
authorwenzelm
Sat Aug 05 20:08:41 2017 +0200 (2017-08-05)
changeset 6634723eaab37e4a8
parent 66346 30663525e057
child 66348 a426e826e84c
support for resident Isabelle servers;
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/server.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/System/isabelle_tool.scala	Sat Aug 05 15:48:02 2017 +0200
     1.2 +++ b/src/Pure/System/isabelle_tool.scala	Sat Aug 05 20:08:41 2017 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4        Options.isabelle_tool,
     1.5        Profiling_Report.isabelle_tool,
     1.6        Remote_DMG.isabelle_tool,
     1.7 +      Server.isabelle_tool,
     1.8        Update_Cartouches.isabelle_tool,
     1.9        Update_Header.isabelle_tool,
    1.10        Update_Then.isabelle_tool,
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/server.scala	Sat Aug 05 20:08:41 2017 +0200
     2.3 @@ -0,0 +1,122 @@
     2.4 +/*  Title:      Pure/Tools/server.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Resident Isabelle servers.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +import java.util.UUID
    2.14 +import java.net.{ServerSocket, InetAddress}
    2.15 +
    2.16 +
    2.17 +object Server
    2.18 +{
    2.19 +  /* per-user servers */
    2.20 +
    2.21 +  object Data
    2.22 +  {
    2.23 +    val database = Path.explode("$ISABELLE_HOME_USER/server.db")
    2.24 +
    2.25 +    val server_name = SQL.Column.string("server_name", primary_key = true)
    2.26 +    val server_port = SQL.Column.int("server_port")
    2.27 +    val password = SQL.Column.string("password")
    2.28 +    val table = SQL.Table("isabelle_servers", List(server_name, server_port, password))
    2.29 +
    2.30 +    sealed case class Entry(server_name: String, server_port: Int, password: String)
    2.31 +    {
    2.32 +      def address: String = "127.0.0.1:" + server_port
    2.33 +    }
    2.34 +  }
    2.35 +
    2.36 +  def list(): List[Data.Entry] =
    2.37 +    using(SQLite.open_database(Data.database))(list(_))
    2.38 +
    2.39 +  def list(db: SQLite.Database): List[Data.Entry] =
    2.40 +    if (db.tables.contains(Data.table.name)) {
    2.41 +      db.using_statement(Data.table.select())(stmt =>
    2.42 +        stmt.execute_query().iterator(res =>
    2.43 +          Data.Entry(
    2.44 +            res.string(Data.server_name),
    2.45 +            res.int(Data.server_port),
    2.46 +            res.string(Data.password))).toList.sortBy(_.server_name))
    2.47 +    }
    2.48 +    else Nil
    2.49 +
    2.50 +  def find(db: SQLite.Database, name: String): Option[Data.Entry] =
    2.51 +    list(db).find(entry => entry.server_name == name)
    2.52 +
    2.53 +  def start(name: String = "", port: Int = 0): (Data.Entry, Boolean) =
    2.54 +  {
    2.55 +    using(SQLite.open_database(Data.database))(db =>
    2.56 +      db.transaction {
    2.57 +        find(db, name) match {
    2.58 +          case Some(entry) => (entry, false)
    2.59 +          case None =>
    2.60 +            val socket = new ServerSocket(port, 50, InetAddress.getByName("127.0.0.1"))
    2.61 +            val server = new Server(socket)
    2.62 +            val entry = Data.Entry(name, server.port, server.password)
    2.63 +
    2.64 +            Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
    2.65 +            db.create_table(Data.table)
    2.66 +            db.using_statement(Data.table.insert())(stmt =>
    2.67 +            {
    2.68 +              stmt.string(1) = entry.server_name
    2.69 +              stmt.int(2) = entry.server_port
    2.70 +              stmt.string(3) = entry.password
    2.71 +              stmt.execute()
    2.72 +            })
    2.73 +            (entry, true)
    2.74 +        }
    2.75 +      })
    2.76 +  }
    2.77 +
    2.78 +  def stop(name: String = ""): Boolean =
    2.79 +  {
    2.80 +    using(SQLite.open_database(Data.database))(db =>
    2.81 +      db.transaction {
    2.82 +        find(db, name) match {
    2.83 +          case Some(entry) =>
    2.84 +            // FIXME shutdown server
    2.85 +            db.using_statement(Data.table.delete(Data.server_name.where_equal(name)))(_.execute)
    2.86 +            true
    2.87 +          case None =>
    2.88 +            false
    2.89 +        }
    2.90 +      })
    2.91 +  }
    2.92 +
    2.93 +
    2.94 +  /* Isabelle tool wrapper */
    2.95 +
    2.96 +  val isabelle_tool =
    2.97 +    Isabelle_Tool("server", "manage resident Isabelle servers", args =>
    2.98 +    {
    2.99 +      var list_servers = false
   2.100 +
   2.101 +      val getopts =
   2.102 +        Getopts("""
   2.103 +Usage: isabelle server [OPTIONS]
   2.104 +
   2.105 +  Options are:
   2.106 +    -l           list servers
   2.107 +
   2.108 +  Manage resident Isabelle servers.
   2.109 +""",
   2.110 +          "l" -> (_ => list_servers = true))
   2.111 +
   2.112 +      val more_args = getopts(args)
   2.113 +      if (more_args.nonEmpty || !list_servers) getopts.usage()
   2.114 +
   2.115 +      if (list_servers) list().foreach(entry =>
   2.116 +        Console.println("server " + quote(entry.server_name) + " = " + entry.address +
   2.117 +          " (password " + quote(entry.password) + ")"))
   2.118 +    })
   2.119 +}
   2.120 +
   2.121 +class Server private(val socket: ServerSocket)
   2.122 +{
   2.123 +  def port: Int = socket.getLocalPort
   2.124 +  val password = UUID.randomUUID().toString
   2.125 +}
     3.1 --- a/src/Pure/build-jars	Sat Aug 05 15:48:02 2017 +0200
     3.2 +++ b/src/Pure/build-jars	Sat Aug 05 20:08:41 2017 +0200
     3.3 @@ -140,6 +140,7 @@
     3.4    Tools/main.scala
     3.5    Tools/print_operation.scala
     3.6    Tools/profiling_report.scala
     3.7 +  Tools/server.scala
     3.8    Tools/simplifier_trace.scala
     3.9    Tools/spell_checker.scala
    3.10    Tools/task_statistics.scala