# HG changeset patch # User wenzelm # Date 1502038607 -7200 # Node ID 8bf96de5019366491b1b2785f25fbc0bb060924c # Parent 882abe912da90969a000e7631f4fdbd59756e004# Parent 6e114edae18b5015988d85b2ddcf782387950616 merged diff -r 882abe912da9 -r 8bf96de50193 src/Pure/System/isabelle_tool.scala --- 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, diff -r 882abe912da9 -r 8bf96de50193 src/Pure/System/system_channel.scala --- 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 diff -r 882abe912da9 -r 8bf96de50193 src/Pure/Tools/server.scala --- /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 + } + } + } +} diff -r 882abe912da9 -r 8bf96de50193 src/Pure/build-jars --- 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 diff -r 882abe912da9 -r 8bf96de50193 src/Pure/library.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 } diff -r 882abe912da9 -r 8bf96de50193 src/Tools/VSCode/src/grammar.scala --- 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": [ diff -r 882abe912da9 -r 8bf96de50193 src/Tools/jEdit/src/plugin.scala --- 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))