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