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