author | wenzelm |
Sat, 10 Mar 2018 11:55:54 +0100 | |
changeset 67805 | 2d9a265b294e |
parent 67801 | 8f5f5fbe291b |
child 67806 | bd4c440c8be7 |
permissions | -rw-r--r-- |
66347 | 1 |
/* Title: Pure/Tools/server.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Resident Isabelle servers. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
10 |
import java.io.{BufferedInputStream, BufferedOutputStream, IOException} |
67797 | 11 |
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} |
66347 | 12 |
|
13 |
||
14 |
object Server |
|
15 |
{ |
|
66927 | 16 |
/* protocol */ |
17 |
||
67794 | 18 |
def split_line(line: String): (String, String) = |
19 |
{ |
|
20 |
val head = line.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c)) |
|
21 |
val rest = line.substring(head.length).dropWhile(Symbol.is_ascii_blank(_)) |
|
22 |
(head, proper_string(rest) getOrElse "{}") |
|
23 |
} |
|
24 |
||
67785 | 25 |
val commands: Map[String, PartialFunction[(Server, JSON.T), JSON.T]] = |
66929 | 26 |
Map( |
67785 | 27 |
"echo" -> { case (_, t) => t }, |
28 |
"help" -> { case (_, JSON.empty) => commands.keySet.toList.sorted }, |
|
67791 | 29 |
"shutdown" -> { case (server, JSON.empty) => server.close(); JSON.empty }) |
66929 | 30 |
|
66927 | 31 |
object Reply extends Enumeration |
32 |
{ |
|
67801 | 33 |
val OK, ERROR, NOTE = Value |
67800 | 34 |
|
35 |
def unapply(line: String): Option[(Reply.Value, JSON.T)] = |
|
36 |
{ |
|
37 |
if (line == "") None |
|
38 |
else { |
|
39 |
val (reply, output) = split_line(line) |
|
40 |
try { Some((withName(reply), JSON.parse(output, strict = false))) } |
|
41 |
catch { |
|
42 |
case _: NoSuchElementException => None |
|
43 |
case Exn.ERROR(_) => None |
|
44 |
} |
|
45 |
} |
|
46 |
} |
|
66927 | 47 |
} |
48 |
||
49 |
||
67786 | 50 |
/* socket connection */ |
51 |
||
52 |
object Connection |
|
53 |
{ |
|
54 |
def apply(socket: Socket): Connection = |
|
55 |
new Connection(socket) |
|
56 |
} |
|
57 |
||
67788 | 58 |
class Connection private(val socket: Socket) |
67786 | 59 |
{ |
60 |
override def toString: String = socket.toString |
|
61 |
||
62 |
def close() { socket.close } |
|
63 |
||
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
64 |
val in = new BufferedInputStream(socket.getInputStream) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
65 |
val out = new BufferedOutputStream(socket.getOutputStream) |
67786 | 66 |
|
67 |
def read_line(): Option[String] = |
|
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
68 |
try { Bytes.read_line(in).map(_.text) } |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
69 |
catch { case _: SocketException => None } |
67786 | 70 |
|
71 |
def write_line(msg: String) |
|
72 |
{ |
|
73 |
require(split_lines(msg).length <= 1) |
|
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
74 |
out.write(UTF8.bytes(msg)) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
75 |
out.write(10) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
76 |
try { out.flush() } catch { case _: SocketException => } |
67786 | 77 |
} |
78 |
||
79 |
def reply(r: Server.Reply.Value, t: JSON.T) |
|
80 |
{ |
|
81 |
write_line(if (t == JSON.empty) r.toString else r.toString + " " + JSON.Format(t)) |
|
82 |
} |
|
83 |
||
84 |
def reply_ok(t: JSON.T) { reply(Server.Reply.OK, t) } |
|
85 |
def reply_error(t: JSON.T) { reply(Server.Reply.ERROR, t) } |
|
86 |
def reply_error_message(message: String, more: (String, JSON.T)*): Unit = |
|
87 |
reply_error(Map("message" -> message) ++ more) |
|
67801 | 88 |
|
89 |
def notify(t: JSON.T) { reply(Server.Reply.NOTE, t) } |
|
90 |
def notify_message(message: String, more: (String, JSON.T)*): Unit = |
|
91 |
notify(Map("message" -> message) ++ more) |
|
67786 | 92 |
} |
93 |
||
94 |
||
66347 | 95 |
/* per-user servers */ |
96 |
||
67787 | 97 |
def print(port: Int, password: String): String = |
98 |
"127.0.0.1:" + port + " (password " + quote(password) + ")" |
|
99 |
||
66347 | 100 |
object Data |
101 |
{ |
|
66349 | 102 |
val database = Path.explode("$ISABELLE_HOME_USER/servers.db") |
66347 | 103 |
|
66857 | 104 |
val name = SQL.Column.string("name").make_primary_key |
66349 | 105 |
val port = SQL.Column.int("port") |
66347 | 106 |
val password = SQL.Column.string("password") |
66349 | 107 |
val table = SQL.Table("isabelle_servers", List(name, port, password)) |
66347 | 108 |
|
66349 | 109 |
sealed case class Entry(name: String, port: Int, password: String) |
66347 | 110 |
{ |
67787 | 111 |
override def toString: String = |
112 |
"server " + quote(name) + " = " + print(port, password) |
|
66353 | 113 |
|
67786 | 114 |
def connection(): Connection = |
67797 | 115 |
{ |
116 |
val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) |
|
117 |
connection.write_line(password) |
|
118 |
connection |
|
119 |
} |
|
67785 | 120 |
|
121 |
def active(): Boolean = |
|
67797 | 122 |
try { |
123 |
using(connection())(connection => |
|
124 |
{ |
|
67798 | 125 |
connection.socket.setSoTimeout(2000) |
67797 | 126 |
connection.read_line() == Some(Reply.OK.toString) |
127 |
}) |
|
128 |
} |
|
129 |
catch { |
|
130 |
case _: IOException => false |
|
131 |
case _: SocketException => false |
|
132 |
case _: SocketTimeoutException => false |
|
133 |
} |
|
66347 | 134 |
} |
135 |
} |
|
136 |
||
137 |
def list(db: SQLite.Database): List[Data.Entry] = |
|
138 |
if (db.tables.contains(Data.table.name)) { |
|
139 |
db.using_statement(Data.table.select())(stmt => |
|
140 |
stmt.execute_query().iterator(res => |
|
141 |
Data.Entry( |
|
66349 | 142 |
res.string(Data.name), |
143 |
res.int(Data.port), |
|
144 |
res.string(Data.password))).toList.sortBy(_.name)) |
|
66347 | 145 |
} |
146 |
else Nil |
|
147 |
||
148 |
def find(db: SQLite.Database, name: String): Option[Data.Entry] = |
|
66353 | 149 |
list(db).find(entry => entry.name == name && entry.active) |
66347 | 150 |
|
67789 | 151 |
def init(name: String = "", port: Int = 0): (Data.Entry, Option[Server]) = |
66347 | 152 |
{ |
153 |
using(SQLite.open_database(Data.database))(db => |
|
67799 | 154 |
{ |
155 |
db.transaction { |
|
156 |
Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check |
|
157 |
db.create_table(Data.table) |
|
158 |
list(db).filterNot(_.active).foreach(entry => |
|
159 |
db.using_statement(Data.table.delete(Data.name.where_equal(entry.name)))(_.execute)) |
|
160 |
} |
|
161 |
db.transaction { |
|
162 |
find(db, name) match { |
|
163 |
case Some(entry) => (entry, None) |
|
164 |
case None => |
|
165 |
val server = new Server(port) |
|
166 |
val entry = Data.Entry(name, server.port, server.password) |
|
66347 | 167 |
|
67799 | 168 |
db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) |
169 |
db.using_statement(Data.table.insert())(stmt => |
|
170 |
{ |
|
171 |
stmt.string(1) = entry.name |
|
172 |
stmt.int(2) = entry.port |
|
173 |
stmt.string(3) = entry.password |
|
174 |
stmt.execute() |
|
175 |
}) |
|
66348 | 176 |
|
67799 | 177 |
server.start |
178 |
(entry, Some(server)) |
|
179 |
} |
|
66347 | 180 |
} |
181 |
}) |
|
182 |
} |
|
183 |
||
67789 | 184 |
def exit(name: String = ""): Boolean = |
66347 | 185 |
{ |
186 |
using(SQLite.open_database(Data.database))(db => |
|
187 |
db.transaction { |
|
188 |
find(db, name) match { |
|
189 |
case Some(entry) => |
|
67797 | 190 |
using(entry.connection())(_.write_line("shutdown")) |
191 |
while(entry.active) { Thread.sleep(50) } |
|
66347 | 192 |
true |
67785 | 193 |
case None => false |
66347 | 194 |
} |
195 |
}) |
|
196 |
} |
|
197 |
||
198 |
||
199 |
/* Isabelle tool wrapper */ |
|
200 |
||
201 |
val isabelle_tool = |
|
202 |
Isabelle_Tool("server", "manage resident Isabelle servers", args => |
|
203 |
{ |
|
66348 | 204 |
var operation_list = false |
205 |
var name = "" |
|
206 |
var port = 0 |
|
66347 | 207 |
|
208 |
val getopts = |
|
209 |
Getopts(""" |
|
210 |
Usage: isabelle server [OPTIONS] |
|
211 |
||
212 |
Options are: |
|
66348 | 213 |
-L list servers |
214 |
-n NAME explicit server name |
|
215 |
-p PORT explicit server port |
|
66347 | 216 |
|
217 |
Manage resident Isabelle servers. |
|
218 |
""", |
|
66348 | 219 |
"L" -> (_ => operation_list = true), |
220 |
"n:" -> (arg => name = arg), |
|
221 |
"p:" -> (arg => port = Value.Int.parse(arg))) |
|
66347 | 222 |
|
223 |
val more_args = getopts(args) |
|
66348 | 224 |
if (more_args.nonEmpty) getopts.usage() |
66347 | 225 |
|
66353 | 226 |
if (operation_list) { |
227 |
for (entry <- using(SQLite.open_database(Data.database))(list(_)) if entry.active) |
|
67787 | 228 |
Output.writeln(entry.toString, stdout = true) |
66353 | 229 |
} |
66348 | 230 |
else { |
67789 | 231 |
val (entry, server) = init(name, port) |
67787 | 232 |
Output.writeln(entry.toString, stdout = true) |
67785 | 233 |
server.foreach(_.join) |
66348 | 234 |
} |
66347 | 235 |
}) |
236 |
} |
|
237 |
||
66352 | 238 |
class Server private(_port: Int) |
66347 | 239 |
{ |
67785 | 240 |
server => |
241 |
||
66350 | 242 |
private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1")) |
67791 | 243 |
|
244 |
def close() { server_socket.close } |
|
245 |
||
66350 | 246 |
def port: Int = server_socket.getLocalPort |
67787 | 247 |
val password: String = Library.UUID() |
66350 | 248 |
|
67787 | 249 |
override def toString: String = Server.print(port, password) |
66348 | 250 |
|
67786 | 251 |
private def handle(connection: Server.Connection) |
66350 | 252 |
{ |
67786 | 253 |
connection.read_line() match { |
67796 | 254 |
case Some(line) if line == password => |
255 |
connection.reply_ok(JSON.empty) |
|
66350 | 256 |
var finished = false |
257 |
while (!finished) { |
|
67786 | 258 |
connection.read_line() match { |
259 |
case None => finished = true |
|
67801 | 260 |
case Some("") => |
261 |
connection.notify_message("Command 'help' provides list of commands") |
|
262 |
case Some(line) => |
|
67794 | 263 |
val (cmd, input) = Server.split_line(line) |
66929 | 264 |
Server.commands.get(cmd) match { |
67786 | 265 |
case None => connection.reply_error("Bad command " + quote(cmd)) |
66929 | 266 |
case Some(body) => |
67794 | 267 |
input match { |
66929 | 268 |
case JSON.Format(arg) => |
67785 | 269 |
if (body.isDefinedAt((server, arg))) { |
67786 | 270 |
try { connection.reply_ok(body(server, arg)) } |
271 |
catch { case ERROR(msg) => connection.reply_error(msg) } |
|
66929 | 272 |
} |
273 |
else { |
|
67786 | 274 |
connection.reply_error_message( |
66929 | 275 |
"Bad argument for command", "command" -> cmd, "argument" -> arg) |
276 |
} |
|
277 |
case _ => |
|
67786 | 278 |
connection.reply_error_message( |
66929 | 279 |
"Malformed command-line", "command" -> cmd, "input" -> input) |
280 |
} |
|
66921 | 281 |
} |
66350 | 282 |
} |
283 |
} |
|
67796 | 284 |
case _ => |
66350 | 285 |
} |
286 |
} |
|
287 |
||
67786 | 288 |
private lazy val server_thread: Thread = |
66350 | 289 |
Standard_Thread.fork("server") { |
290 |
var finished = false |
|
291 |
while (!finished) { |
|
292 |
Exn.capture(server_socket.accept) match { |
|
293 |
case Exn.Res(socket) => |
|
294 |
Standard_Thread.fork("server_connection") |
|
67786 | 295 |
{ using(Server.Connection(socket))(handle(_)) } |
66350 | 296 |
case Exn.Exn(_) => finished = true |
297 |
} |
|
298 |
} |
|
299 |
} |
|
67785 | 300 |
|
67790
1babcc248be0
clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents:
67789
diff
changeset
|
301 |
def start { server_thread } |
1babcc248be0
clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents:
67789
diff
changeset
|
302 |
|
67791 | 303 |
def join { server_thread.join; close() } |
66347 | 304 |
} |