author | wenzelm |
Sun, 11 Mar 2018 15:08:14 +0100 | |
changeset 67820 | e30d6368c7c8 |
parent 67812 | b123c9a007d0 |
child 67821 | 82fb12061069 |
permissions | -rw-r--r-- |
66347 | 1 |
/* Title: Pure/Tools/server.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Resident Isabelle servers. |
|
67809 | 5 |
|
6 |
Message formats: |
|
7 |
- short message (single line): |
|
8 |
NAME ARGUMENT |
|
9 |
- long message (multiple lines): |
|
10 |
BYTE_LENGTH |
|
11 |
NAME ARGUMENT |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
12 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
13 |
Argument formats: |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
14 |
- Unit as empty string |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
15 |
- XML.Elem in YXML notation |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
16 |
- JSON.T in standard notation |
66347 | 17 |
*/ |
18 |
||
19 |
package isabelle |
|
20 |
||
21 |
||
67806 | 22 |
import java.io.{BufferedInputStream, BufferedOutputStream, BufferedReader, BufferedWriter, |
23 |
InputStreamReader, OutputStreamWriter, IOException} |
|
67797 | 24 |
import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} |
66347 | 25 |
|
26 |
||
27 |
object Server |
|
28 |
{ |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
29 |
/* message argument */ |
66927 | 30 |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
31 |
object Argument |
67794 | 32 |
{ |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
33 |
def split(msg: String): (String, String) = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
34 |
{ |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
35 |
val name = msg.takeWhile(c => Symbol.is_ascii_letter(c) || Symbol.is_ascii_letdig(c)) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
36 |
val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank(_)) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
37 |
(name, argument) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
38 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
39 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
40 |
def print(arg: Any): String = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
41 |
arg match { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
42 |
case () => "" |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
43 |
case t: XML.Elem => YXML.string_of_tree(t) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
44 |
case t: JSON.T => JSON.Format(t) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
45 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
46 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
47 |
def parse(argument: String): Any = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
48 |
if (argument == "") () |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
49 |
else if (YXML.detect_elem(argument)) YXML.parse_elem(argument) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
50 |
else JSON.parse(argument, strict = false) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
51 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
52 |
def unapply(argument: String): Option[Any] = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
53 |
try { Some(parse(argument)) } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
54 |
catch { case ERROR(_) => None } |
67794 | 55 |
} |
56 |
||
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
57 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
58 |
/* input command */ |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
59 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
60 |
object Command |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
61 |
{ |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
62 |
type T = PartialFunction[(Server, Any), Any] |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
63 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
64 |
private val table: Map[String, T] = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
65 |
Map( |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
66 |
"echo" -> { case (_, t) => t }, |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
67 |
"help" -> { case (_, ()) => table.keySet.toList.sorted }, |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
68 |
"shutdown" -> { case (server, ()) => server.close(); () }) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
69 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
70 |
def unapply(name: String): Option[T] = table.get(name) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
71 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
72 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
73 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
74 |
/* output reply */ |
66929 | 75 |
|
66927 | 76 |
object Reply extends Enumeration |
77 |
{ |
|
67801 | 78 |
val OK, ERROR, NOTE = Value |
67800 | 79 |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
80 |
def unapply(msg: String): Option[(Reply.Value, Any)] = |
67800 | 81 |
{ |
67809 | 82 |
if (msg == "") None |
67800 | 83 |
else { |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
84 |
val (name, argument) = Argument.split(msg) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
85 |
for { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
86 |
reply <- |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
87 |
try { Some(withName(name)) } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
88 |
catch { case _: NoSuchElementException => None } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
89 |
arg <- Argument.unapply(argument) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
90 |
} yield (reply, arg) |
67800 | 91 |
} |
92 |
} |
|
66927 | 93 |
} |
94 |
||
95 |
||
67786 | 96 |
/* socket connection */ |
97 |
||
98 |
object Connection |
|
99 |
{ |
|
100 |
def apply(socket: Socket): Connection = |
|
101 |
new Connection(socket) |
|
102 |
} |
|
103 |
||
67788 | 104 |
class Connection private(val socket: Socket) |
67786 | 105 |
{ |
106 |
override def toString: String = socket.toString |
|
107 |
||
108 |
def close() { socket.close } |
|
109 |
||
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
110 |
val in = new BufferedInputStream(socket.getInputStream) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
111 |
val out = new BufferedOutputStream(socket.getOutputStream) |
67786 | 112 |
|
67809 | 113 |
def read_message(): Option[String] = |
114 |
try { |
|
115 |
Bytes.read_line(in).map(_.text) match { |
|
116 |
case Some(Value.Int(n)) => |
|
117 |
Bytes.read_block(in, n).map(bytes => Library.trim_line(bytes.text)) |
|
118 |
case res => res |
|
119 |
} |
|
120 |
} |
|
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
121 |
catch { case _: SocketException => None } |
67786 | 122 |
|
67809 | 123 |
def write_message(msg: String) |
67786 | 124 |
{ |
67809 | 125 |
val b = UTF8.bytes(msg) |
126 |
if (b.length > 100 || b.contains(10)) { |
|
127 |
out.write(UTF8.bytes((b.length + 1).toString)) |
|
128 |
out.write(10) |
|
129 |
} |
|
130 |
out.write(b) |
|
67805
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
131 |
out.write(10) |
2d9a265b294e
more uniform Bytes.read_line/read_block operations;
wenzelm
parents:
67801
diff
changeset
|
132 |
try { out.flush() } catch { case _: SocketException => } |
67786 | 133 |
} |
134 |
||
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
135 |
def reply(r: Server.Reply.Value, arg: Any) |
67786 | 136 |
{ |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
137 |
val argument = Argument.print(arg) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
138 |
write_message(if (argument == "") r.toString else r.toString + " " + argument) |
67786 | 139 |
} |
140 |
||
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
141 |
def reply_ok(arg: Any) { reply(Server.Reply.OK, arg) } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
142 |
def reply_error(arg: Any) { reply(Server.Reply.ERROR, arg) } |
67786 | 143 |
def reply_error_message(message: String, more: (String, JSON.T)*): Unit = |
144 |
reply_error(Map("message" -> message) ++ more) |
|
67801 | 145 |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
146 |
def notify(arg: Any) { reply(Server.Reply.NOTE, arg) } |
67801 | 147 |
def notify_message(message: String, more: (String, JSON.T)*): Unit = |
148 |
notify(Map("message" -> message) ++ more) |
|
67786 | 149 |
} |
150 |
||
151 |
||
67807 | 152 |
/* server info */ |
153 |
||
154 |
sealed case class Info(name: String, port: Int, password: String) |
|
155 |
{ |
|
156 |
override def toString: String = |
|
67812 | 157 |
"server " + print_name_space(name) + "= " + print(port, password) |
67807 | 158 |
|
159 |
def connection(): Connection = |
|
160 |
{ |
|
161 |
val connection = Connection(new Socket(InetAddress.getByName("127.0.0.1"), port)) |
|
67809 | 162 |
connection.write_message(password) |
67807 | 163 |
connection |
164 |
} |
|
165 |
||
166 |
def active(): Boolean = |
|
167 |
try { |
|
168 |
using(connection())(connection => |
|
169 |
{ |
|
170 |
connection.socket.setSoTimeout(2000) |
|
67809 | 171 |
connection.read_message() == Some(Reply.OK.toString) |
67807 | 172 |
}) |
173 |
} |
|
174 |
catch { |
|
175 |
case _: IOException => false |
|
176 |
case _: SocketException => false |
|
177 |
case _: SocketTimeoutException => false |
|
178 |
} |
|
179 |
||
180 |
def console() |
|
181 |
{ |
|
182 |
using(connection())(connection => |
|
183 |
{ |
|
184 |
val tty_loop = |
|
185 |
new TTY_Loop( |
|
186 |
new BufferedWriter(new OutputStreamWriter(connection.socket.getOutputStream)), |
|
187 |
new BufferedReader(new InputStreamReader(connection.socket.getInputStream))) |
|
188 |
tty_loop.join |
|
189 |
}) |
|
190 |
} |
|
191 |
} |
|
192 |
||
193 |
||
66347 | 194 |
/* per-user servers */ |
195 |
||
67812 | 196 |
def print_name_space(name: String): String = |
197 |
if (name == "") "" else quote(name) + " " |
|
198 |
||
67787 | 199 |
def print(port: Int, password: String): String = |
200 |
"127.0.0.1:" + port + " (password " + quote(password) + ")" |
|
201 |
||
66347 | 202 |
object Data |
203 |
{ |
|
66349 | 204 |
val database = Path.explode("$ISABELLE_HOME_USER/servers.db") |
66347 | 205 |
|
66857 | 206 |
val name = SQL.Column.string("name").make_primary_key |
66349 | 207 |
val port = SQL.Column.int("port") |
66347 | 208 |
val password = SQL.Column.string("password") |
66349 | 209 |
val table = SQL.Table("isabelle_servers", List(name, port, password)) |
66347 | 210 |
} |
211 |
||
67807 | 212 |
def list(db: SQLite.Database): List[Info] = |
66347 | 213 |
if (db.tables.contains(Data.table.name)) { |
214 |
db.using_statement(Data.table.select())(stmt => |
|
215 |
stmt.execute_query().iterator(res => |
|
67807 | 216 |
Info( |
66349 | 217 |
res.string(Data.name), |
218 |
res.int(Data.port), |
|
219 |
res.string(Data.password))).toList.sortBy(_.name)) |
|
66347 | 220 |
} |
221 |
else Nil |
|
222 |
||
67807 | 223 |
def find(db: SQLite.Database, name: String): Option[Info] = |
224 |
list(db).find(server_info => server_info.name == name && server_info.active) |
|
66347 | 225 |
|
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
226 |
def init(name: String = "", port: Int = 0, existing_server: Boolean = false) |
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
227 |
: (Info, Option[Server]) = |
66347 | 228 |
{ |
229 |
using(SQLite.open_database(Data.database))(db => |
|
67799 | 230 |
{ |
231 |
db.transaction { |
|
232 |
Isabelle_System.bash("chmod 600 " + File.bash_path(Data.database)).check |
|
233 |
db.create_table(Data.table) |
|
67807 | 234 |
list(db).filterNot(_.active).foreach(server_info => |
235 |
db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))( |
|
236 |
_.execute)) |
|
67799 | 237 |
} |
238 |
db.transaction { |
|
239 |
find(db, name) match { |
|
67807 | 240 |
case Some(server_info) => (server_info, None) |
67799 | 241 |
case None => |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
242 |
if (existing_server) { |
67812 | 243 |
error("Isabelle server " + print_name_space(name) + "not running") |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
244 |
} |
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
245 |
|
67799 | 246 |
val server = new Server(port) |
67807 | 247 |
val server_info = Info(name, server.port, server.password) |
66347 | 248 |
|
67799 | 249 |
db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) |
250 |
db.using_statement(Data.table.insert())(stmt => |
|
251 |
{ |
|
67807 | 252 |
stmt.string(1) = server_info.name |
253 |
stmt.int(2) = server_info.port |
|
254 |
stmt.string(3) = server_info.password |
|
67799 | 255 |
stmt.execute() |
256 |
}) |
|
66348 | 257 |
|
67799 | 258 |
server.start |
67807 | 259 |
(server_info, Some(server)) |
67799 | 260 |
} |
66347 | 261 |
} |
262 |
}) |
|
263 |
} |
|
264 |
||
67789 | 265 |
def exit(name: String = ""): Boolean = |
66347 | 266 |
{ |
267 |
using(SQLite.open_database(Data.database))(db => |
|
268 |
db.transaction { |
|
269 |
find(db, name) match { |
|
67807 | 270 |
case Some(server_info) => |
67809 | 271 |
using(server_info.connection())(_.write_message("shutdown")) |
67807 | 272 |
while(server_info.active) { Thread.sleep(50) } |
66347 | 273 |
true |
67785 | 274 |
case None => false |
66347 | 275 |
} |
276 |
}) |
|
277 |
} |
|
278 |
||
279 |
||
280 |
/* Isabelle tool wrapper */ |
|
281 |
||
282 |
val isabelle_tool = |
|
283 |
Isabelle_Tool("server", "manage resident Isabelle servers", args => |
|
284 |
{ |
|
67806 | 285 |
var console = false |
66348 | 286 |
var operation_list = false |
287 |
var name = "" |
|
288 |
var port = 0 |
|
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
289 |
var existing_server = false |
66347 | 290 |
|
291 |
val getopts = |
|
292 |
Getopts(""" |
|
293 |
Usage: isabelle server [OPTIONS] |
|
294 |
||
295 |
Options are: |
|
67806 | 296 |
-C console interaction with specified server |
297 |
-L list servers only |
|
66348 | 298 |
-n NAME explicit server name |
299 |
-p PORT explicit server port |
|
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
300 |
-s assume existing server, no implicit startup |
66347 | 301 |
|
302 |
Manage resident Isabelle servers. |
|
303 |
""", |
|
67806 | 304 |
"C" -> (_ => console = true), |
66348 | 305 |
"L" -> (_ => operation_list = true), |
306 |
"n:" -> (arg => name = arg), |
|
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
307 |
"p:" -> (arg => port = Value.Int.parse(arg)), |
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
308 |
"s" -> (_ => existing_server = true)) |
66347 | 309 |
|
310 |
val more_args = getopts(args) |
|
66348 | 311 |
if (more_args.nonEmpty) getopts.usage() |
66347 | 312 |
|
66353 | 313 |
if (operation_list) { |
67807 | 314 |
for { |
315 |
server_info <- using(SQLite.open_database(Data.database))(list(_)) |
|
316 |
if server_info.active |
|
317 |
} Output.writeln(server_info.toString, stdout = true) |
|
66353 | 318 |
} |
66348 | 319 |
else { |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
320 |
val (server_info, server) = init(name, port = port, existing_server = existing_server) |
67807 | 321 |
Output.writeln(server_info.toString, stdout = true) |
322 |
if (console) server_info.console() |
|
67785 | 323 |
server.foreach(_.join) |
66348 | 324 |
} |
66347 | 325 |
}) |
326 |
} |
|
327 |
||
66352 | 328 |
class Server private(_port: Int) |
66347 | 329 |
{ |
67785 | 330 |
server => |
331 |
||
66350 | 332 |
private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1")) |
67791 | 333 |
|
334 |
def close() { server_socket.close } |
|
335 |
||
66350 | 336 |
def port: Int = server_socket.getLocalPort |
67787 | 337 |
val password: String = Library.UUID() |
66350 | 338 |
|
67787 | 339 |
override def toString: String = Server.print(port, password) |
66348 | 340 |
|
67786 | 341 |
private def handle(connection: Server.Connection) |
66350 | 342 |
{ |
67809 | 343 |
connection.read_message() match { |
344 |
case Some(msg) if msg == password => |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
345 |
connection.reply_ok(()) |
66350 | 346 |
var finished = false |
347 |
while (!finished) { |
|
67809 | 348 |
connection.read_message() match { |
67786 | 349 |
case None => finished = true |
67801 | 350 |
case Some("") => |
351 |
connection.notify_message("Command 'help' provides list of commands") |
|
67809 | 352 |
case Some(msg) => |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
353 |
val (name, argument) = Server.Argument.split(msg) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
354 |
name match { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
355 |
case Server.Command(cmd) => |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
356 |
argument match { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
357 |
case Server.Argument(arg) => |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
358 |
if (cmd.isDefinedAt((server, arg))) { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
359 |
Exn.capture { cmd((server, arg)) } match { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
360 |
case Exn.Res(res) => connection.reply_ok(res) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
361 |
case Exn.Exn(ERROR(msg)) => connection.reply_error(msg) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
362 |
case Exn.Exn(exn) => throw exn |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
363 |
} |
66929 | 364 |
} |
365 |
else { |
|
67786 | 366 |
connection.reply_error_message( |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
367 |
"Bad argument for command " + Library.single_quote(name), |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
368 |
"argument" -> argument) |
66929 | 369 |
} |
370 |
case _ => |
|
67786 | 371 |
connection.reply_error_message( |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
372 |
"Malformed argument for command " + Library.single_quote(name), |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
373 |
"argument" -> argument) |
66929 | 374 |
} |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
375 |
case _ => connection.reply_error("Bad command " + Library.single_quote(name)) |
66921 | 376 |
} |
66350 | 377 |
} |
378 |
} |
|
67796 | 379 |
case _ => |
66350 | 380 |
} |
381 |
} |
|
382 |
||
67786 | 383 |
private lazy val server_thread: Thread = |
66350 | 384 |
Standard_Thread.fork("server") { |
385 |
var finished = false |
|
386 |
while (!finished) { |
|
387 |
Exn.capture(server_socket.accept) match { |
|
388 |
case Exn.Res(socket) => |
|
389 |
Standard_Thread.fork("server_connection") |
|
67786 | 390 |
{ using(Server.Connection(socket))(handle(_)) } |
66350 | 391 |
case Exn.Exn(_) => finished = true |
392 |
} |
|
393 |
} |
|
394 |
} |
|
67785 | 395 |
|
67790
1babcc248be0
clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents:
67789
diff
changeset
|
396 |
def start { server_thread } |
1babcc248be0
clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents:
67789
diff
changeset
|
397 |
|
67791 | 398 |
def join { server_thread.join; close() } |
66347 | 399 |
} |