src/Pure/Tools/server.scala
author wenzelm
Sun Dec 10 20:29:00 2017 +0100 (18 months ago)
changeset 67178 70576478bda9
parent 66929 c19b17b72777
child 67784 543e36ae489c
permissions -rw-r--r--
avoid println with its extra CR on Windows;
     1 /*  Title:      Pure/Tools/server.scala
     2     Author:     Makarius
     3 
     4 Resident Isabelle servers.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
    11   IOException}
    12 import java.net.{Socket, ServerSocket, InetAddress}
    13 
    14 
    15 object Server
    16 {
    17   /* protocol */
    18 
    19   val commands: Map[String, PartialFunction[JSON.T, JSON.T]] =
    20     Map(
    21       "help" -> { case JSON.empty => commands.keySet.toList.sorted },
    22       "echo" -> { case t => t })
    23 
    24   object Reply extends Enumeration
    25   {
    26     val OK, ERROR = Value
    27   }
    28 
    29 
    30   /* per-user servers */
    31 
    32   object Data
    33   {
    34     val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
    35 
    36     val name = SQL.Column.string("name").make_primary_key
    37     val port = SQL.Column.int("port")
    38     val password = SQL.Column.string("password")
    39     val table = SQL.Table("isabelle_servers", List(name, port, password))
    40 
    41     sealed case class Entry(name: String, port: Int, password: String)
    42     {
    43       def print: String =
    44         "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
    45 
    46       def active: Boolean =
    47         try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
    48         catch { case _: IOException => false }
    49     }
    50   }
    51 
    52   def list(db: SQLite.Database): List[Data.Entry] =
    53     if (db.tables.contains(Data.table.name)) {
    54       db.using_statement(Data.table.select())(stmt =>
    55         stmt.execute_query().iterator(res =>
    56           Data.Entry(
    57             res.string(Data.name),
    58             res.int(Data.port),
    59             res.string(Data.password))).toList.sortBy(_.name))
    60     }
    61     else Nil
    62 
    63   def find(db: SQLite.Database, name: String): Option[Data.Entry] =
    64     list(db).find(entry => entry.name == name && entry.active)
    65 
    66   def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
    67   {
    68     using(SQLite.open_database(Data.database))(db =>
    69       db.transaction {
    70         find(db, name) match {
    71           case Some(entry) => (entry, None)
    72           case None =>
    73             val server = new Server(port)
    74             val entry = Data.Entry(name, server.port, server.password)
    75 
    76             Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
    77             db.create_table(Data.table)
    78             db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
    79             db.using_statement(Data.table.insert())(stmt =>
    80             {
    81               stmt.string(1) = entry.name
    82               stmt.int(2) = entry.port
    83               stmt.string(3) = entry.password
    84               stmt.execute()
    85             })
    86 
    87             (entry, Some(server.thread))
    88         }
    89       })
    90   }
    91 
    92   def stop(name: String = ""): Boolean =
    93   {
    94     using(SQLite.open_database(Data.database))(db =>
    95       db.transaction {
    96         find(db, name) match {
    97           case Some(entry) =>
    98             // FIXME shutdown server
    99             db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
   100             true
   101           case None =>
   102             false
   103         }
   104       })
   105   }
   106 
   107 
   108   /* Isabelle tool wrapper */
   109 
   110   val isabelle_tool =
   111     Isabelle_Tool("server", "manage resident Isabelle servers", args =>
   112     {
   113       var operation_list = false
   114       var name = ""
   115       var port = 0
   116 
   117       val getopts =
   118         Getopts("""
   119 Usage: isabelle server [OPTIONS]
   120 
   121   Options are:
   122     -L           list servers
   123     -n NAME      explicit server name
   124     -p PORT      explicit server port
   125 
   126   Manage resident Isabelle servers.
   127 """,
   128           "L" -> (_ => operation_list = true),
   129           "n:" -> (arg => name = arg),
   130           "p:" -> (arg => port = Value.Int.parse(arg)))
   131 
   132       val more_args = getopts(args)
   133       if (more_args.nonEmpty) getopts.usage()
   134 
   135       if (operation_list) {
   136         for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
   137           Output.writeln(entry.print, stdout = true)
   138       }
   139       else {
   140         val (entry, thread) = start(name, port)
   141         Output.writeln(entry.print, stdout = true)
   142         thread.foreach(_.join)
   143       }
   144     })
   145 }
   146 
   147 class Server private(_port: Int)
   148 {
   149   private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
   150   def port: Int = server_socket.getLocalPort
   151   def close { server_socket.close }
   152 
   153   val password: String = Library.UUID()
   154 
   155   private def handle_connection(socket: Socket)
   156   {
   157     val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
   158     val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
   159 
   160     def reply_line(msg: String)
   161     {
   162       require(split_lines(msg).length <= 1)
   163       writer.write(msg)
   164       writer.newLine()
   165       writer.flush()
   166     }
   167 
   168     def reply(r: Server.Reply.Value, t: JSON.T)
   169     {
   170       reply_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t))
   171     }
   172 
   173     def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) }
   174     def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) }
   175     def reply_error_message(message: String, more: (String, JSON.T)*): Unit =
   176       reply_error(Map("message" -> message) ++ more)
   177 
   178     val Command_Line = """^(\S+)\s*(.*)$""".r
   179 
   180     reader.readLine() match {
   181       case null =>
   182       case bad if bad != password => reply_error("Bad password -- connection closed")
   183       case _ =>
   184         var finished = false
   185         while (!finished) {
   186           reader.readLine() match {
   187             case null => finished = true
   188             case Command_Line(cmd, input) =>
   189               Server.commands.get(cmd) match {
   190                 case None => reply_error("Unknown command " + quote(cmd))
   191                 case Some(body) =>
   192                   proper_string(input) getOrElse "{}" match {
   193                     case JSON.Format(arg) =>
   194                       if (body.isDefinedAt(arg)) {
   195                         try { reply_ok(body(arg)) }
   196                         catch { case ERROR(msg) => reply_error(msg) }
   197                       }
   198                       else {
   199                         reply_error_message(
   200                           "Bad argument for command", "command" -> cmd, "argument" -> arg)
   201                       }
   202                     case _ =>
   203                       reply_error_message(
   204                         "Malformed command-line", "command" -> cmd, "input" -> input)
   205                   }
   206               }
   207             case _ =>
   208           }
   209         }
   210     }
   211   }
   212 
   213   lazy val thread: Thread =
   214     Standard_Thread.fork("server") {
   215       var finished = false
   216       while (!finished) {
   217         Exn.capture(server_socket.accept) match {
   218           case Exn.Res(socket) =>
   219             Standard_Thread.fork("server_connection")
   220               { try { handle_connection(socket) } finally { socket.close } }
   221           case Exn.Exn(_) => finished = true
   222         }
   223       }
   224     }
   225 }