author | wenzelm |
Mon, 13 Apr 2020 16:16:22 +0200 | |
changeset 71747 | 1dd514c8c1df |
parent 71726 | a5fda30edae2 |
child 72163 | f5722290a4d0 |
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 |
||
67837 | 22 |
import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter, |
23 |
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 |
{ |
67903 | 33 |
def is_name_char(c: Char): Boolean = |
34 |
Symbol.is_ascii_letter(c) || Symbol.is_ascii_digit(c) || c == '_' || c == '.' |
|
35 |
||
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
36 |
def split(msg: String): (String, String) = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
37 |
{ |
71601 | 38 |
val name = msg.takeWhile(is_name_char) |
39 |
val argument = msg.substring(name.length).dropWhile(Symbol.is_ascii_blank) |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
40 |
(name, argument) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
41 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
42 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
43 |
def print(arg: Any): String = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
44 |
arg match { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
45 |
case () => "" |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
46 |
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
|
47 |
case t: JSON.T => JSON.Format(t) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
48 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
49 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
50 |
def parse(argument: String): Any = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
51 |
if (argument == "") () |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
52 |
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
|
53 |
else JSON.parse(argument, strict = false) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
54 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
55 |
def unapply(argument: String): Option[Any] = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
56 |
try { Some(parse(argument)) } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
57 |
catch { case ERROR(_) => None } |
67794 | 58 |
} |
59 |
||
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
60 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
61 |
/* input command */ |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
62 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
63 |
object Command |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
64 |
{ |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
65 |
type T = PartialFunction[(Context, Any), Any] |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
66 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
67 |
private val table: Map[String, T] = |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
68 |
Map( |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
67840
diff
changeset
|
69 |
"help" -> { case (_, ()) => table.keySet.toList.sorted }, |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
70 |
"echo" -> { case (_, t) => t }, |
67902 | 71 |
"shutdown" -> { case (context, ()) => context.server.shutdown() }, |
67920 | 72 |
"cancel" -> |
73 |
{ case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) }, |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
67840
diff
changeset
|
74 |
"session_build" -> |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
67840
diff
changeset
|
75 |
{ case (context, Server_Commands.Session_Build(args)) => |
67861 | 76 |
context.make_task(task => |
67886 | 77 |
Server_Commands.Session_Build.command(args, progress = task.progress)._1) |
67869 | 78 |
}, |
79 |
"session_start" -> |
|
80 |
{ case (context, Server_Commands.Session_Start(args)) => |
|
81 |
context.make_task(task => |
|
82 |
{ |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
83 |
val (res, entry) = |
67878 | 84 |
Server_Commands.Session_Start.command( |
67886 | 85 |
args, progress = task.progress, log = context.server.log) |
67878 | 86 |
context.server.add_session(entry) |
67869 | 87 |
res |
88 |
}) |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
89 |
}, |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
90 |
"session_stop" -> |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
91 |
{ case (context, Server_Commands.Session_Stop(id)) => |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
92 |
context.make_task(_ => |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
93 |
{ |
67878 | 94 |
val session = context.server.remove_session(id) |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
95 |
Server_Commands.Session_Stop.command(session)._1 |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
96 |
}) |
67883 | 97 |
}, |
98 |
"use_theories" -> |
|
99 |
{ case (context, Server_Commands.Use_Theories(args)) => |
|
100 |
context.make_task(task => |
|
101 |
{ |
|
102 |
val session = context.server.the_session(args.session_id) |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
103 |
Server_Commands.Use_Theories.command( |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
104 |
args, session, id = task.id, progress = task.progress)._1 |
68530 | 105 |
}) |
67941 | 106 |
}, |
107 |
"purge_theories" -> |
|
108 |
{ case (context, Server_Commands.Purge_Theories(args)) => |
|
109 |
val session = context.server.the_session(args.session_id) |
|
110 |
Server_Commands.Purge_Theories.command(args, session)._1 |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
67840
diff
changeset
|
111 |
}) |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
112 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
113 |
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
|
114 |
} |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
115 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
116 |
|
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
117 |
/* output reply */ |
66929 | 118 |
|
67857 | 119 |
class Error(val message: String, val json: JSON.Object.T = JSON.Object.empty) |
120 |
extends RuntimeException(message) |
|
121 |
||
67891
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
122 |
def json_error(exn: Throwable): JSON.Object.T = |
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
123 |
exn match { |
67913
d58fa3ed236f
proper order of matches: Server.Error is an instance of Exn.ERROR;
wenzelm
parents:
67911
diff
changeset
|
124 |
case e: Error => Reply.error_message(e.message) ++ e.json |
67901 | 125 |
case ERROR(msg) => Reply.error_message(msg) |
126 |
case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn)) |
|
67891
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
127 |
case _ => JSON.Object.empty |
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
128 |
} |
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
129 |
|
66927 | 130 |
object Reply extends Enumeration |
131 |
{ |
|
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
132 |
val OK, ERROR, FINISHED, FAILED, NOTE = Value |
67800 | 133 |
|
67901 | 134 |
def message(msg: String, kind: String = ""): JSON.Object.T = |
67931
f7917c15b566
field "kind" is always present, with default "writeln";
wenzelm
parents:
67920
diff
changeset
|
135 |
JSON.Object(Markup.KIND -> proper_string(kind).getOrElse(Markup.WRITELN), "message" -> msg) |
67901 | 136 |
|
137 |
def error_message(msg: String): JSON.Object.T = |
|
67911
3cda747493d8
clarified markup according to common Command.Results;
wenzelm
parents:
67904
diff
changeset
|
138 |
message(msg, kind = Markup.ERROR) |
67857 | 139 |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
140 |
def unapply(msg: String): Option[(Reply.Value, Any)] = |
67800 | 141 |
{ |
67809 | 142 |
if (msg == "") None |
67800 | 143 |
else { |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
144 |
val (name, argument) = Argument.split(msg) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
145 |
for { |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
146 |
reply <- |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
147 |
try { Some(withName(name)) } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
148 |
catch { case _: NoSuchElementException => None } |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
149 |
arg <- Argument.unapply(argument) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
150 |
} yield (reply, arg) |
67800 | 151 |
} |
152 |
} |
|
66927 | 153 |
} |
154 |
||
155 |
||
67786 | 156 |
/* socket connection */ |
157 |
||
158 |
object Connection |
|
159 |
{ |
|
160 |
def apply(socket: Socket): Connection = |
|
161 |
new Connection(socket) |
|
162 |
} |
|
163 |
||
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69033
diff
changeset
|
164 |
class Connection private(socket: Socket) extends AutoCloseable |
67786 | 165 |
{ |
166 |
override def toString: String = socket.toString |
|
167 |
||
168 |
def close() { socket.close } |
|
169 |
||
67832 | 170 |
def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) } |
171 |
||
172 |
private val in = new BufferedInputStream(socket.getInputStream) |
|
173 |
private val out = new BufferedOutputStream(socket.getOutputStream) |
|
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
174 |
private val out_lock: AnyRef = new Object |
67786 | 175 |
|
71713 | 176 |
def tty_loop(): TTY_Loop = |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
177 |
new TTY_Loop( |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
178 |
new OutputStreamWriter(out), |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
179 |
new InputStreamReader(in), |
71713 | 180 |
writer_lock = out_lock) |
67837 | 181 |
|
69464 | 182 |
def read_password(password: String): Boolean = |
183 |
try { Byte_Message.read_line(in).map(_.text) == Some(password) } |
|
184 |
catch { case _: IOException => false } |
|
185 |
||
67809 | 186 |
def read_message(): Option[String] = |
69451 | 187 |
try { Byte_Message.read_line_message(in).map(_.text) } |
188 |
catch { case _: IOException => None } |
|
67786 | 189 |
|
69448 | 190 |
def write_message(msg: String): Unit = |
191 |
out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } |
|
67786 | 192 |
|
67859 | 193 |
def reply(r: Reply.Value, arg: Any) |
67786 | 194 |
{ |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
195 |
val argument = Argument.print(arg) |
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
196 |
write_message(if (argument == "") r.toString else r.toString + " " + argument) |
67786 | 197 |
} |
198 |
||
67859 | 199 |
def reply_ok(arg: Any) { reply(Reply.OK, arg) } |
200 |
def reply_error(arg: Any) { reply(Reply.ERROR, arg) } |
|
67857 | 201 |
def reply_error_message(message: String, more: JSON.Object.Entry*): Unit = |
67901 | 202 |
reply_error(Reply.error_message(message) ++ more) |
67801 | 203 |
|
67859 | 204 |
def notify(arg: Any) { reply(Reply.NOTE, arg) } |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
205 |
} |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
206 |
|
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
207 |
|
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
208 |
/* context with output channels */ |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
209 |
|
67878 | 210 |
class Context private[Server](val server: Server, connection: Connection) |
69393
ed0824ef337e
static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
wenzelm
parents:
69033
diff
changeset
|
211 |
extends AutoCloseable |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
212 |
{ |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
213 |
context => |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
214 |
|
67859 | 215 |
def reply(r: Reply.Value, arg: Any) { connection.reply(r, arg) } |
67840 | 216 |
def notify(arg: Any) { connection.notify(arg) } |
67857 | 217 |
def message(kind: String, msg: String, more: JSON.Object.Entry*): Unit = |
67901 | 218 |
notify(Reply.message(msg, kind = kind) ++ more) |
67857 | 219 |
def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*) |
220 |
def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*) |
|
221 |
def error_message(msg: String, more: JSON.Object.Entry*): Unit = |
|
67911
3cda747493d8
clarified markup according to common Command.Results;
wenzelm
parents:
67904
diff
changeset
|
222 |
message(Markup.ERROR, msg, more:_*) |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
223 |
|
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
224 |
def progress(more: JSON.Object.Entry*): Connection_Progress = |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
225 |
new Connection_Progress(context, more:_*) |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
226 |
|
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
227 |
override def toString: String = connection.toString |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
228 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
229 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
230 |
/* asynchronous tasks */ |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
231 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
232 |
private val _tasks = Synchronized(Set.empty[Task]) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
233 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
234 |
def make_task(body: Task => JSON.Object.T): Task = |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
235 |
{ |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
236 |
val task = new Task(context, body) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
237 |
_tasks.change(_ + task) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
238 |
task |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
239 |
} |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
240 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
241 |
def remove_task(task: Task): Unit = |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
242 |
_tasks.change(_ - task) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
243 |
|
69458 | 244 |
def cancel_task(id: UUID.T): Unit = |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
245 |
_tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks }) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
246 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
247 |
def close() |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
248 |
{ |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
249 |
while(_tasks.change_result(tasks => { tasks.foreach(_.cancel); (tasks.nonEmpty, tasks) })) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
250 |
{ _tasks.value.foreach(_.join) } |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
251 |
} |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
252 |
} |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
253 |
|
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
254 |
class Connection_Progress private[Server](context: Context, more: JSON.Object.Entry*) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
255 |
extends Progress |
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
256 |
{ |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
257 |
override def echo(msg: String): Unit = context.writeln(msg, more:_*) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
258 |
override def echo_warning(msg: String): Unit = context.warning(msg, more:_*) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
259 |
override def echo_error_message(msg: String): Unit = context.error_message(msg, more:_*) |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68530
diff
changeset
|
260 |
|
68957 | 261 |
override def theory(theory: Progress.Theory) |
262 |
{ |
|
263 |
val entries: List[JSON.Object.Entry] = |
|
264 |
List("theory" -> theory.theory, "session" -> theory.session) ::: |
|
265 |
(theory.percentage match { case None => Nil case Some(p) => List("percentage" -> p) }) |
|
266 |
context.writeln(theory.message, entries ::: more.toList:_*) |
|
267 |
} |
|
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
268 |
|
69818
60d0ee8f2ddb
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents:
69817
diff
changeset
|
269 |
override def nodes_status(nodes_status: Document_Status.Nodes_Status) |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68530
diff
changeset
|
270 |
{ |
68903 | 271 |
val json = |
69818
60d0ee8f2ddb
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents:
69817
diff
changeset
|
272 |
for ((name, node_status) <- nodes_status.present) |
68903 | 273 |
yield name.json + ("status" -> nodes_status(name).json) |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68530
diff
changeset
|
274 |
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json)) |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68530
diff
changeset
|
275 |
} |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68530
diff
changeset
|
276 |
|
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67838
diff
changeset
|
277 |
override def toString: String = context.toString |
67786 | 278 |
} |
279 |
||
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
280 |
class Task private[Server](val context: Context, body: Task => JSON.Object.T) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
281 |
{ |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
282 |
task => |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
283 |
|
69458 | 284 |
val id: UUID.T = UUID.random() |
67885 | 285 |
val ident: JSON.Object.Entry = ("task" -> id.toString) |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
286 |
|
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
287 |
val progress: Connection_Progress = context.progress(ident) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
288 |
def cancel { progress.stop } |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
289 |
|
71692 | 290 |
private lazy val thread = Isabelle_Thread.fork(name = "server_task") |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
291 |
{ |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
292 |
Exn.capture { body(task) } match { |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
293 |
case Exn.Res(res) => |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
294 |
context.reply(Reply.FINISHED, res + ident) |
67891
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
295 |
case Exn.Exn(exn) => |
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
296 |
val err = json_error(exn) |
4f383cd54f69
clarified exception handling: include interrupts;
wenzelm
parents:
67886
diff
changeset
|
297 |
if (err.isEmpty) throw exn else context.reply(Reply.FAILED, err + ident) |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
298 |
} |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
299 |
progress.stop |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
300 |
context.remove_task(task) |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
301 |
} |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
302 |
def start { thread } |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
303 |
def join { thread.join } |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
304 |
} |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
305 |
|
67786 | 306 |
|
67807 | 307 |
/* server info */ |
308 |
||
69463 | 309 |
val localhost_name: String = "127.0.0.1" |
310 |
def localhost: InetAddress = InetAddress.getByName(localhost_name) |
|
311 |
||
312 |
def print_address(port: Int): String = localhost_name + ":" + port |
|
69460
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
313 |
|
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
314 |
def print(port: Int, password: String): String = |
69461 | 315 |
print_address(port) + " (password " + quote(password) + ")" |
69460
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
316 |
|
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
317 |
object Info |
67807 | 318 |
{ |
69463 | 319 |
private val Pattern = |
320 |
("""server "([^"]*)" = \Q""" + localhost_name + """\E:(\d+) \(password "([^"]*)"\)""").r |
|
69460
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
321 |
|
69463 | 322 |
def parse(s: String): Option[Info] = |
69460
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
323 |
s match { |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
324 |
case Pattern(name, Value.Int(port), password) => Some(Info(name, port, password)) |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
325 |
case _ => None |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
326 |
} |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
327 |
|
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
328 |
def apply(name: String, port: Int, password: String): Info = |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
329 |
new Info(name, port, password) |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
330 |
} |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
331 |
|
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
332 |
class Info private(val name: String, val port: Int, val password: String) |
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
333 |
{ |
69461 | 334 |
def address: String = print_address(port) |
69460
5ffe7e17f770
clarified signature, e.g. for re-use by other servers;
wenzelm
parents:
69458
diff
changeset
|
335 |
|
67807 | 336 |
override def toString: String = |
67821
82fb12061069
more uniform output: this may be parsed by another program;
wenzelm
parents:
67820
diff
changeset
|
337 |
"server " + quote(name) + " = " + print(port, password) |
67807 | 338 |
|
339 |
def connection(): Connection = |
|
340 |
{ |
|
69463 | 341 |
val connection = Connection(new Socket(localhost, port)) |
67809 | 342 |
connection.write_message(password) |
67807 | 343 |
connection |
344 |
} |
|
345 |
||
346 |
def active(): Boolean = |
|
347 |
try { |
|
348 |
using(connection())(connection => |
|
349 |
{ |
|
67832 | 350 |
connection.set_timeout(Time.seconds(2.0)) |
67867 | 351 |
connection.read_message() match { |
352 |
case Some(Reply(Reply.OK, _)) => true |
|
353 |
case _ => false |
|
354 |
} |
|
67807 | 355 |
}) |
356 |
} |
|
357 |
catch { |
|
358 |
case _: IOException => false |
|
359 |
case _: SocketException => false |
|
360 |
case _: SocketTimeoutException => false |
|
361 |
} |
|
362 |
} |
|
363 |
||
364 |
||
66347 | 365 |
/* per-user servers */ |
366 |
||
67822 | 367 |
val default_name = "isabelle" |
368 |
||
66347 | 369 |
object Data |
370 |
{ |
|
66349 | 371 |
val database = Path.explode("$ISABELLE_HOME_USER/servers.db") |
66347 | 372 |
|
66857 | 373 |
val name = SQL.Column.string("name").make_primary_key |
66349 | 374 |
val port = SQL.Column.int("port") |
66347 | 375 |
val password = SQL.Column.string("password") |
66349 | 376 |
val table = SQL.Table("isabelle_servers", List(name, port, password)) |
66347 | 377 |
} |
378 |
||
67807 | 379 |
def list(db: SQLite.Database): List[Info] = |
66347 | 380 |
if (db.tables.contains(Data.table.name)) { |
381 |
db.using_statement(Data.table.select())(stmt => |
|
382 |
stmt.execute_query().iterator(res => |
|
67807 | 383 |
Info( |
66349 | 384 |
res.string(Data.name), |
385 |
res.int(Data.port), |
|
386 |
res.string(Data.password))).toList.sortBy(_.name)) |
|
66347 | 387 |
} |
388 |
else Nil |
|
389 |
||
67807 | 390 |
def find(db: SQLite.Database, name: String): Option[Info] = |
391 |
list(db).find(server_info => server_info.name == name && server_info.active) |
|
66347 | 392 |
|
67870 | 393 |
def init( |
394 |
name: String = default_name, |
|
395 |
port: Int = 0, |
|
396 |
existing_server: Boolean = false, |
|
397 |
log: Logger = No_Logger): (Info, Option[Server]) = |
|
66347 | 398 |
{ |
399 |
using(SQLite.open_database(Data.database))(db => |
|
67799 | 400 |
{ |
401 |
db.transaction { |
|
71114 | 402 |
Isabelle_System.chmod("600", Data.database) |
67799 | 403 |
db.create_table(Data.table) |
67807 | 404 |
list(db).filterNot(_.active).foreach(server_info => |
405 |
db.using_statement(Data.table.delete(Data.name.where_equal(server_info.name)))( |
|
406 |
_.execute)) |
|
67799 | 407 |
} |
408 |
db.transaction { |
|
409 |
find(db, name) match { |
|
67807 | 410 |
case Some(server_info) => (server_info, None) |
67799 | 411 |
case None => |
67821
82fb12061069
more uniform output: this may be parsed by another program;
wenzelm
parents:
67820
diff
changeset
|
412 |
if (existing_server) error("Isabelle server " + quote(name) + " not running") |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
413 |
|
67870 | 414 |
val server = new Server(port, log) |
67807 | 415 |
val server_info = Info(name, server.port, server.password) |
66347 | 416 |
|
67799 | 417 |
db.using_statement(Data.table.delete(Data.name.where_equal(name)))(_.execute) |
418 |
db.using_statement(Data.table.insert())(stmt => |
|
419 |
{ |
|
67807 | 420 |
stmt.string(1) = server_info.name |
421 |
stmt.int(2) = server_info.port |
|
422 |
stmt.string(3) = server_info.password |
|
67799 | 423 |
stmt.execute() |
424 |
}) |
|
66348 | 425 |
|
67799 | 426 |
server.start |
67807 | 427 |
(server_info, Some(server)) |
67799 | 428 |
} |
66347 | 429 |
} |
430 |
}) |
|
431 |
} |
|
432 |
||
67822 | 433 |
def exit(name: String = default_name): Boolean = |
66347 | 434 |
{ |
435 |
using(SQLite.open_database(Data.database))(db => |
|
436 |
db.transaction { |
|
437 |
find(db, name) match { |
|
67807 | 438 |
case Some(server_info) => |
67809 | 439 |
using(server_info.connection())(_.write_message("shutdown")) |
71684 | 440 |
while(server_info.active) { Time.seconds(0.05).sleep } |
66347 | 441 |
true |
67785 | 442 |
case None => false |
66347 | 443 |
} |
444 |
}) |
|
445 |
} |
|
446 |
||
447 |
||
448 |
/* Isabelle tool wrapper */ |
|
449 |
||
450 |
val isabelle_tool = |
|
451 |
Isabelle_Tool("server", "manage resident Isabelle servers", args => |
|
452 |
{ |
|
67806 | 453 |
var console = false |
67870 | 454 |
var log_file: Option[Path] = None |
66348 | 455 |
var operation_list = false |
67823 | 456 |
var operation_exit = false |
67822 | 457 |
var name = default_name |
66348 | 458 |
var port = 0 |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
459 |
var existing_server = false |
66347 | 460 |
|
461 |
val getopts = |
|
462 |
Getopts(""" |
|
463 |
Usage: isabelle server [OPTIONS] |
|
464 |
||
465 |
Options are: |
|
67870 | 466 |
-L FILE logging on FILE |
67875 | 467 |
-c console interaction with specified server |
67904 | 468 |
-l list servers (alternative operation) |
67822 | 469 |
-n NAME explicit server name (default: """ + default_name + """) |
66348 | 470 |
-p PORT explicit server port |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
471 |
-s assume existing server, no implicit startup |
67904 | 472 |
-x exit specified server (alternative operation) |
66347 | 473 |
|
474 |
Manage resident Isabelle servers. |
|
475 |
""", |
|
67870 | 476 |
"L:" -> (arg => log_file = Some(Path.explode(File.standard_path(arg)))), |
67875 | 477 |
"c" -> (_ => console = true), |
67870 | 478 |
"l" -> (_ => operation_list = true), |
66348 | 479 |
"n:" -> (arg => name = arg), |
67811
33199d033505
more options: client without implicit server startup;
wenzelm
parents:
67809
diff
changeset
|
480 |
"p:" -> (arg => port = Value.Int.parse(arg)), |
67870 | 481 |
"s" -> (_ => existing_server = true), |
67876 | 482 |
"x" -> (_ => operation_exit = true)) |
66347 | 483 |
|
484 |
val more_args = getopts(args) |
|
66348 | 485 |
if (more_args.nonEmpty) getopts.usage() |
66347 | 486 |
|
66353 | 487 |
if (operation_list) { |
67807 | 488 |
for { |
71714 | 489 |
server_info <- using(SQLite.open_database(Data.database))(list) |
67807 | 490 |
if server_info.active |
491 |
} Output.writeln(server_info.toString, stdout = true) |
|
66353 | 492 |
} |
67823 | 493 |
else if (operation_exit) { |
494 |
val ok = Server.exit(name) |
|
69033 | 495 |
sys.exit(if (ok) 0 else 2) |
67823 | 496 |
} |
66348 | 497 |
else { |
67870 | 498 |
val log = Logger.make(log_file) |
499 |
val (server_info, server) = |
|
500 |
init(name, port = port, existing_server = existing_server, log = log) |
|
67807 | 501 |
Output.writeln(server_info.toString, stdout = true) |
67834 | 502 |
if (console) { |
503 |
using(server_info.connection())(connection => connection.tty_loop().join) |
|
504 |
} |
|
67785 | 505 |
server.foreach(_.join) |
66348 | 506 |
} |
66347 | 507 |
}) |
508 |
} |
|
509 |
||
67870 | 510 |
class Server private(_port: Int, val log: Logger) |
66347 | 511 |
{ |
67785 | 512 |
server => |
513 |
||
69463 | 514 |
private val server_socket = new ServerSocket(_port, 50, Server.localhost) |
67902 | 515 |
|
69458 | 516 |
private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session]) |
517 |
def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString)) |
|
71383 | 518 |
def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id)) |
69458 | 519 |
def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) } |
520 |
def remove_session(id: UUID.T): Headless.Session = |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
521 |
{ |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
522 |
_sessions.change_result(sessions => |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
523 |
sessions.get(id) match { |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
524 |
case Some(session) => (session, sessions - id) |
67883 | 525 |
case None => err_session(id) |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
526 |
}) |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
527 |
} |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67870
diff
changeset
|
528 |
|
67902 | 529 |
def shutdown() |
530 |
{ |
|
531 |
server_socket.close |
|
67791 | 532 |
|
67902 | 533 |
val sessions = _sessions.change_result(sessions => (sessions, Map.empty)) |
534 |
for ((_, session) <- sessions) { |
|
535 |
try { |
|
536 |
val result = session.stop() |
|
71747 | 537 |
if (!result.ok) log("Session shutdown failed: " + result.print_rc) |
67902 | 538 |
} |
539 |
catch { case ERROR(msg) => log("Session shutdown failed: " + msg) } |
|
540 |
} |
|
541 |
} |
|
67791 | 542 |
|
66350 | 543 |
def port: Int = server_socket.getLocalPort |
69458 | 544 |
val password: String = UUID.random_string() |
66350 | 545 |
|
67787 | 546 |
override def toString: String = Server.print(port, password) |
66348 | 547 |
|
67786 | 548 |
private def handle(connection: Server.Connection) |
66350 | 549 |
{ |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
550 |
using(new Server.Context(server, connection))(context => |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
551 |
{ |
69464 | 552 |
if (connection.read_password(password)) { |
553 |
connection.reply_ok( |
|
554 |
JSON.Object( |
|
555 |
"isabelle_id" -> Isabelle_System.isabelle_id(), |
|
556 |
"isabelle_version" -> Distribution.version)) |
|
67867 | 557 |
|
69464 | 558 |
var finished = false |
559 |
while (!finished) { |
|
560 |
connection.read_message() match { |
|
561 |
case None => finished = true |
|
562 |
case Some("") => context.notify("Command 'help' provides list of commands") |
|
563 |
case Some(msg) => |
|
564 |
val (name, argument) = Server.Argument.split(msg) |
|
565 |
name match { |
|
566 |
case Server.Command(cmd) => |
|
567 |
argument match { |
|
568 |
case Server.Argument(arg) => |
|
569 |
if (cmd.isDefinedAt((context, arg))) { |
|
570 |
Exn.capture { cmd((context, arg)) } match { |
|
571 |
case Exn.Res(task: Server.Task) => |
|
572 |
connection.reply_ok(JSON.Object(task.ident)) |
|
573 |
task.start |
|
574 |
case Exn.Res(res) => connection.reply_ok(res) |
|
575 |
case Exn.Exn(exn) => |
|
576 |
val err = Server.json_error(exn) |
|
577 |
if (err.isEmpty) throw exn else connection.reply_error(err) |
|
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
578 |
} |
69464 | 579 |
} |
580 |
else { |
|
67786 | 581 |
connection.reply_error_message( |
69464 | 582 |
"Bad argument for command " + Library.single_quote(name), |
67820
e30d6368c7c8
clarified argument formats: explicit Unit, allow XML.Elem as well;
wenzelm
parents:
67812
diff
changeset
|
583 |
"argument" -> argument) |
69464 | 584 |
} |
585 |
case _ => |
|
586 |
connection.reply_error_message( |
|
587 |
"Malformed argument for command " + Library.single_quote(name), |
|
588 |
"argument" -> argument) |
|
589 |
} |
|
590 |
case _ => connection.reply_error("Bad command " + Library.single_quote(name)) |
|
591 |
} |
|
66350 | 592 |
} |
69464 | 593 |
} |
67860
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
594 |
} |
5a6c483269f3
support for asynchronous tasks, with "cancel" command;
wenzelm
parents:
67859
diff
changeset
|
595 |
}) |
66350 | 596 |
} |
597 |
||
67786 | 598 |
private lazy val server_thread: Thread = |
71692 | 599 |
Isabelle_Thread.fork(name = "server") { |
66350 | 600 |
var finished = false |
601 |
while (!finished) { |
|
602 |
Exn.capture(server_socket.accept) match { |
|
603 |
case Exn.Res(socket) => |
|
71692 | 604 |
Isabelle_Thread.fork(name = "server_connection") |
71601 | 605 |
{ using(Server.Connection(socket))(handle) } |
66350 | 606 |
case Exn.Exn(_) => finished = true |
607 |
} |
|
608 |
} |
|
609 |
} |
|
67785 | 610 |
|
67790
1babcc248be0
clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents:
67789
diff
changeset
|
611 |
def start { server_thread } |
1babcc248be0
clarified server start, notably for invocation within regular Isabelle/Scala process;
wenzelm
parents:
67789
diff
changeset
|
612 |
|
67902 | 613 |
def join { server_thread.join; shutdown() } |
66347 | 614 |
} |