--- a/src/Pure/System/isabelle_tool.scala Sun Aug 06 15:02:54 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sun Aug 06 18:56:47 2017 +0200
@@ -115,6 +115,7 @@
Options.isabelle_tool,
Profiling_Report.isabelle_tool,
Remote_DMG.isabelle_tool,
+ Server.isabelle_tool,
Update_Cartouches.isabelle_tool,
Update_Header.isabelle_tool,
Update_Then.isabelle_tool,
--- a/src/Pure/System/system_channel.scala Sun Aug 06 15:02:54 2017 +0200
+++ b/src/Pure/System/system_channel.scala Sun Aug 06 18:56:47 2017 +0200
@@ -18,7 +18,7 @@
class System_Channel private
{
- private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1"))
+ private val server = new ServerSocket(0, 50, InetAddress.getByName("127.0.0.1"))
val server_name: String = "127.0.0.1:" + server.getLocalPort
override def toString: String = server_name
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/server.scala Sun Aug 06 18:56:47 2017 +0200
@@ -0,0 +1,180 @@
+/* Title: Pure/Tools/server.scala
+ Author: Makarius
+
+Resident Isabelle servers.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
+ IOException}
+import java.net.{Socket, ServerSocket, InetAddress}
+
+
+object Server
+{
+ /* per-user servers */
+
+ object Data
+ {
+ val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
+
+ val name = SQL.Column.string("name", primary_key = true)
+ val port = SQL.Column.int("port")
+ val password = SQL.Column.string("password")
+ val table = SQL.Table("isabelle_servers", List(name, port, password))
+
+ sealed case class Entry(name: String, port: Int, password: String)
+ {
+ def print: String =
+ "server " + quote(name) + " = 127.0.0.1:" + port + " (password " + quote(password) + ")"
+
+ def active: Boolean =
+ try { (new Socket(InetAddress.getByName("127.0.0.1"), port)).close; true }
+ catch { case _: IOException => false }
+ }
+ }
+
+ def list(db: SQLite.Database): List[Data.Entry] =
+ if (db.tables.contains(Data.table.name)) {
+ db.using_statement(Data.table.select())(stmt =>
+ stmt.execute_query().iterator(res =>
+ Data.Entry(
+ res.string(Data.name),
+ res.int(Data.port),
+ res.string(Data.password))).toList.sortBy(_.name))
+ }
+ else Nil
+
+ def find(db: SQLite.Database, name: String): Option[Data.Entry] =
+ list(db).find(entry => entry.name == name && entry.active)
+
+ def start(name: String = "", port: Int = 0): (Data.Entry, Option[Thread]) =
+ {
+ using(SQLite.open_database(Data.database))(db =>
+ db.transaction {
+ find(db, name) match {
+ case Some(entry) => (entry, None)
+ case None =>
+ val server = new Server(port)
+ val entry = Data.Entry(name, server.port, server.password)
+
+ Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check
+ db.create_table(Data.table)
+ db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+ db.using_statement(Data.table.insert())(stmt =>
+ {
+ stmt.string(1) = entry.name
+ stmt.int(2) = entry.port
+ stmt.string(3) = entry.password
+ stmt.execute()
+ })
+
+ (entry, Some(server.thread))
+ }
+ })
+ }
+
+ def stop(name: String = ""): Boolean =
+ {
+ using(SQLite.open_database(Data.database))(db =>
+ db.transaction {
+ find(db, name) match {
+ case Some(entry) =>
+ // FIXME shutdown server
+ db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute)
+ true
+ case None =>
+ false
+ }
+ })
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("server", "manage resident Isabelle servers", args =>
+ {
+ var operation_list = false
+ var name = ""
+ var port = 0
+
+ val getopts =
+ Getopts("""
+Usage: isabelle server [OPTIONS]
+
+ Options are:
+ -L list servers
+ -n NAME explicit server name
+ -p PORT explicit server port
+
+ Manage resident Isabelle servers.
+""",
+ "L" -> (_ => operation_list = true),
+ "n:" -> (arg => name = arg),
+ "p:" -> (arg => port = Value.Int.parse(arg)))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ if (operation_list) {
+ for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active)
+ Console.println(entry.print)
+ }
+ else {
+ val (entry, thread) = start(name, port)
+ Console.println(entry.print)
+ thread.foreach(_.join)
+ }
+ })
+}
+
+class Server private(_port: Int)
+{
+ private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
+ def port: Int = server_socket.getLocalPort
+ def close { server_socket.close }
+
+ val password: String = Library.UUID()
+
+ private def handle_connection(socket: Socket)
+ {
+ val reader = new BufferedReader(new InputStreamReader(socket.getInputStream, UTF8.charset))
+ val writer = new BufferedWriter(new OutputStreamWriter(socket.getOutputStream, UTF8.charset))
+
+ def println(s: String)
+ {
+ writer.write(s)
+ writer.newLine()
+ writer.flush()
+ }
+
+ reader.readLine() match {
+ case null =>
+ case bad if bad != password => println("BAD PASSWORD")
+ case _ =>
+ var finished = false
+ while (!finished) {
+ reader.readLine() match {
+ case null => println("FINISHED"); finished = true
+ case line => println("ECHO " + line)
+ }
+ }
+ }
+ }
+
+ lazy val thread: Thread =
+ Standard_Thread.fork("server") {
+ var finished = false
+ while (!finished) {
+ Exn.capture(server_socket.accept) match {
+ case Exn.Res(socket) =>
+ Standard_Thread.fork("server_connection")
+ { try { handle_connection(socket) } finally { socket.close } }
+ case Exn.Exn(_) => finished = true
+ }
+ }
+ }
+}
--- a/src/Pure/build-jars Sun Aug 06 15:02:54 2017 +0200
+++ b/src/Pure/build-jars Sun Aug 06 18:56:47 2017 +0200
@@ -140,6 +140,7 @@
Tools/main.scala
Tools/print_operation.scala
Tools/profiling_report.scala
+ Tools/server.scala
Tools/simplifier_trace.scala
Tools/spell_checker.scala
Tools/task_statistics.scala
--- a/src/Pure/library.scala Sun Aug 06 15:02:54 2017 +0200
+++ b/src/Pure/library.scala Sun Aug 06 18:56:47 2017 +0200
@@ -259,4 +259,9 @@
def proper_list[A](list: List[A]): Option[List[A]] =
if (list == null || list.isEmpty) None else Some(list)
+
+
+ /* UUID */
+
+ def UUID(): String = java.util.UUID.randomUUID().toString
}
--- a/src/Tools/VSCode/src/grammar.scala Sun Aug 06 15:02:54 2017 +0200
+++ b/src/Tools/VSCode/src/grammar.scala Sun Aug 06 18:56:47 2017 +0200
@@ -9,8 +9,6 @@
import isabelle._
-import java.util.UUID
-
object Grammar
{
@@ -47,7 +45,7 @@
"name": "Isabelle",
"scopeName": "source.isabelle",
"fileTypes": ["thy"],
- "uuid": """ + JSON.Format(UUID.randomUUID().toString) + """,
+ "uuid": """ + JSON.Format(Library.UUID()) + """,
"repository": {
"comment": {
"patterns": [
--- a/src/Tools/jEdit/src/plugin.scala Sun Aug 06 15:02:54 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sun Aug 06 18:56:47 2017 +0200
@@ -12,7 +12,6 @@
import javax.swing.JOptionPane
import java.io.{File => JFile}
-import java.util.UUID
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
import org.gjt.sp.jedit.textarea.JEditTextArea
@@ -398,7 +397,7 @@
/* HTTP server */
- val http_root: String = "/" + UUID.randomUUID().toString
+ val http_root: String = "/" + Library.UUID()
val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))