src/Pure/Tools/server.scala
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 66353 6e114edae18b
child 66857 f8f42289c4df
permissions -rw-r--r--
tuned signature;
     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   /* per-user servers */
    18 
    19   object Data
    20   {
    21     val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
    22 
    23     val name = SQL.Column.string("name", primary_key = true)
    24     val port = SQL.Column.int("port")
    25     val password = SQL.Column.string("password")
    26     val table = SQL.Table("isabelle_servers", List(name, port, password))
    27 
    28     sealed case class Entry(name: String, port: Int, password: String)
    29     {
    30       def print: String =
    31         "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
    32 
    33       def active: Boolean =
    34         try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
    35         catch { case _: IOException => false }
    36     }
    37   }
    38 
    39   def list(db: SQLite.Database): List[Data.Entry] =
    40     if (db.tables.contains(Data.table.name)) {
    41       db.using_statement(Data.table.select())(stmt =>
    42         stmt.execute_query().iterator(res =>
    43           Data.Entry(
    44             res.string(Data.name),
    45             res.int(Data.port),
    46             res.string(Data.password))).toList.sortBy(_.name))
    47     }
    48     else Nil
    49 
    50   def find(db: SQLite.Database, name: String): Option[Data.Entry] =
    51     list(db).find(entry => entry.name == name && entry.active)
    52 
    53   def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
    54   {
    55     using(SQLite.open_database(Data.database))(db =>
    56       db.transaction {
    57         find(db, name) match {
    58           case Some(entry) => (entry, None)
    59           case None =>
    60             val server = new Server(port)
    61             val entry = Data.Entry(name, server.port, server.password)
    62 
    63             Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
    64             db.create_table(Data.table)
    65             db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
    66             db.using_statement(Data.table.insert())(stmt =>
    67             {
    68               stmt.string(1) = entry.name
    69               stmt.int(2) = entry.port
    70               stmt.string(3) = entry.password
    71               stmt.execute()
    72             })
    73 
    74             (entry, Some(server.thread))
    75         }
    76       })
    77   }
    78 
    79   def stop(name: String = ""): Boolean =
    80   {
    81     using(SQLite.open_database(Data.database))(db =>
    82       db.transaction {
    83         find(db, name) match {
    84           case Some(entry) =>
    85             // FIXME shutdown server
    86             db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
    87             true
    88           case None =>
    89             false
    90         }
    91       })
    92   }
    93 
    94 
    95   /* Isabelle tool wrapper */
    96 
    97   val isabelle_tool =
    98     Isabelle_Tool("server", "manage resident Isabelle servers", args =>
    99     {
   100       var operation_list = false
   101       var name = ""
   102       var port = 0
   103 
   104       val getopts =
   105         Getopts("""
   106 Usage: isabelle server [OPTIONS]
   107 
   108   Options are:
   109     -L           list servers
   110     -n NAME      explicit server name
   111     -p PORT      explicit server port
   112 
   113   Manage resident Isabelle servers.
   114 """,
   115           "L" -> (_ => operation_list = true),
   116           "n:" -> (arg => name = arg),
   117           "p:" -> (arg => port = Value.Int.parse(arg)))
   118 
   119       val more_args = getopts(args)
   120       if (more_args.nonEmpty) getopts.usage()
   121 
   122       if (operation_list) {
   123         for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
   124           Console.println(entry.print)
   125       }
   126       else {
   127         val (entry, thread) = start(name, port)
   128         Console.println(entry.print)
   129         thread.foreach(_.join)
   130       }
   131     })
   132 }
   133 
   134 class Server private(_port: Int)
   135 {
   136   private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
   137   def port: Int = server_socket.getLocalPort
   138   def close { server_socket.close }
   139 
   140   val password: String = Library.UUID()
   141 
   142   private def handle_connection(socket: Socket)
   143   {
   144     val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
   145     val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
   146 
   147     def println(s: String)
   148     {
   149       writer.write(s)
   150       writer.newLine()
   151       writer.flush()
   152     }
   153 
   154     reader.readLine() match {
   155       case null =>
   156       case bad if bad != password => println("BAD PASSWORD")
   157       case _ =>
   158         var finished = false
   159         while (!finished) {
   160           reader.readLine() match {
   161             case null => println("FINISHED"); finished = true
   162             case line => println("ECHO " + line)
   163           }
   164         }
   165     }
   166   }
   167 
   168   lazy val thread: Thread =
   169     Standard_Thread.fork("server") {
   170       var finished = false
   171       while (!finished) {
   172         Exn.capture(server_socket.accept) match {
   173           case Exn.Res(socket) =>
   174             Standard_Thread.fork("server_connection")
   175               { try { handle_connection(socket) } finally { socket.close } }
   176           case Exn.Exn(_) => finished = true
   177         }
   178       }
   179     }
   180 }