author | wenzelm |
Tue, 07 Apr 2020 21:49:36 +0200 | |
changeset 71726 | a5fda30edae2 |
parent 71601 | 97ccf48c2f0c |
child 71747 | 1dd514c8c1df |
permissions | -rw-r--r-- |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Tools/server_commands.scala |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
3 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
4 |
Miscellaneous Isabelle server commands. |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
6 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
8 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
9 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
10 |
object Server_Commands |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
11 |
{ |
67863 | 12 |
def default_preferences: String = Options.read_prefs() |
67883 | 13 |
|
67920 | 14 |
object Cancel |
15 |
{ |
|
69458 | 16 |
sealed case class Args(task: UUID.T) |
67920 | 17 |
|
18 |
def unapply(json: JSON.T): Option[Args] = |
|
19 |
for { task <- JSON.uuid(json, "task") } |
|
20 |
yield Args(task) |
|
21 |
} |
|
22 |
||
23 |
||
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
24 |
object Session_Build |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
25 |
{ |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
26 |
sealed case class Args( |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
27 |
session: String, |
67863 | 28 |
preferences: String = default_preferences, |
67862 | 29 |
options: List[String] = Nil, |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
30 |
dirs: List[String] = Nil, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
31 |
include_sessions: List[String] = Nil, |
67853 | 32 |
verbose: Boolean = false) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
33 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
34 |
def unapply(json: JSON.T): Option[Args] = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
35 |
for { |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
36 |
session <- JSON.string(json, "session") |
67863 | 37 |
preferences <- JSON.string_default(json, "preferences", default_preferences) |
68742 | 38 |
options <- JSON.strings_default(json, "options") |
39 |
dirs <- JSON.strings_default(json, "dirs") |
|
40 |
include_sessions <- JSON.strings_default(json, "include_sessions") |
|
67853 | 41 |
verbose <- JSON.bool_default(json, "verbose") |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
42 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
43 |
yield { |
67862 | 44 |
Args(session, preferences = preferences, options = options, dirs = dirs, |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69536
diff
changeset
|
45 |
include_sessions = include_sessions, verbose = verbose) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
46 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
47 |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
48 |
def command(args: Args, progress: Progress = new Progress) |
71599 | 49 |
: (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
50 |
{ |
67862 | 51 |
val options = Options.init(prefs = args.preferences, opts = args.options) |
71601 | 52 |
val dirs = args.dirs.map(Path.explode) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
53 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
54 |
val base_info = |
67919
dd90faed43b2
clarified signature: do not expose somewhat accidental internal options;
wenzelm
parents:
67916
diff
changeset
|
55 |
Sessions.base_info(options, args.session, progress = progress, dirs = dirs, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
56 |
include_sessions = args.include_sessions) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
57 |
val base = base_info.check_base |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
58 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
59 |
val results = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
60 |
Build.build(options, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
61 |
progress = progress, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
62 |
build_heap = true, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
63 |
dirs = dirs, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
64 |
infos = base_info.infos, |
67853 | 65 |
verbose = args.verbose, |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
66 |
sessions = List(args.session)) |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
67 |
|
67858 | 68 |
val sessions_order = |
69 |
base_info.sessions_structure.imports_topological_order.zipWithIndex. |
|
70 |
toMap.withDefaultValue(-1) |
|
71 |
||
72 |
val results_json = |
|
73 |
JSON.Object( |
|
67912 | 74 |
"ok" -> results.ok, |
67858 | 75 |
"return_code" -> results.rc, |
76 |
"sessions" -> |
|
77 |
results.sessions.toList.sortBy(sessions_order).map(session => |
|
67912 | 78 |
{ |
79 |
val result = results(session) |
|
80 |
JSON.Object( |
|
81 |
"session" -> session, |
|
82 |
"ok" -> result.ok, |
|
83 |
"return_code" -> result.rc, |
|
84 |
"timeout" -> result.timeout, |
|
85 |
"timing" -> result.timing.json) |
|
86 |
})) |
|
67858 | 87 |
|
71599 | 88 |
if (results.ok) (results_json, results, options, base_info) |
67858 | 89 |
else throw new Server.Error("Session build failed: return code " + results.rc, results_json) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
90 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
91 |
} |
67869 | 92 |
|
93 |
object Session_Start |
|
94 |
{ |
|
95 |
sealed case class Args( |
|
96 |
build: Session_Build.Args, |
|
97 |
print_mode: List[String] = Nil) |
|
98 |
||
99 |
def unapply(json: JSON.T): Option[Args] = |
|
100 |
for { |
|
101 |
build <- Session_Build.unapply(json) |
|
68742 | 102 |
print_mode <- JSON.strings_default(json, "print_mode") |
67869 | 103 |
} |
104 |
yield Args(build = build, print_mode = print_mode) |
|
105 |
||
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
106 |
def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger) |
69458 | 107 |
: (JSON.Object.T, (UUID.T, Headless.Session)) = |
67869 | 108 |
{ |
71599 | 109 |
val (_, _, options, base_info) = |
110 |
try { Session_Build.command(args.build, progress = progress) } |
|
67914
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
111 |
catch { case exn: Server.Error => error(exn.message) } |
67869 | 112 |
|
71599 | 113 |
val resources = Headless.Resources(options, base_info, log = log) |
69536 | 114 |
|
115 |
val session = resources.start_session(print_mode = args.print_mode, progress = progress) |
|
67869 | 116 |
|
69458 | 117 |
val id = UUID.random() |
67869 | 118 |
|
67925 | 119 |
val res = |
120 |
JSON.Object( |
|
121 |
"session_id" -> id.toString, |
|
122 |
"tmp_dir" -> File.path(session.tmp_dir).implode) |
|
123 |
||
124 |
(res, id -> session) |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
125 |
} |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
126 |
} |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
127 |
|
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
128 |
object Session_Stop |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
129 |
{ |
69458 | 130 |
def unapply(json: JSON.T): Option[UUID.T] = |
67885 | 131 |
JSON.uuid(json, "session_id") |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
132 |
|
69012 | 133 |
def command(session: Headless.Session): (JSON.Object.T, Process_Result) = |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
134 |
{ |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
135 |
val result = session.stop() |
67916 | 136 |
val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
137 |
|
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
138 |
if (result.ok) (result_json, result) |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
139 |
else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json) |
67869 | 140 |
} |
141 |
} |
|
67883 | 142 |
|
143 |
object Use_Theories |
|
144 |
{ |
|
145 |
sealed case class Args( |
|
69458 | 146 |
session_id: UUID.T, |
67940
b4e80f062fbf
clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents:
67937
diff
changeset
|
147 |
theories: List[String], |
67897 | 148 |
master_dir: String = "", |
149 |
pretty_margin: Double = Pretty.default_margin, |
|
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
150 |
unicode_symbols: Boolean = false, |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
151 |
export_pattern: String = "", |
69520 | 152 |
check_delay: Option[Time] = None, |
153 |
check_limit: Option[Int] = None, |
|
154 |
watchdog_timeout: Option[Time] = None, |
|
155 |
nodes_status_delay: Option[Time] = None, |
|
156 |
commit_cleanup_delay: Option[Time] = None) |
|
67883 | 157 |
|
158 |
def unapply(json: JSON.T): Option[Args] = |
|
159 |
for { |
|
67885 | 160 |
session_id <- JSON.uuid(json, "session_id") |
68742 | 161 |
theories <- JSON.strings(json, "theories") |
67883 | 162 |
master_dir <- JSON.string_default(json, "master_dir") |
67897 | 163 |
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
164 |
unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
|
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
165 |
export_pattern <- JSON.string_default(json, "export_pattern") |
69520 | 166 |
check_delay = JSON.seconds(json, "check_delay") |
167 |
check_limit = JSON.int(json, "check_limit") |
|
168 |
watchdog_timeout = JSON.seconds(json, "watchdog_timeout") |
|
169 |
nodes_status_delay = JSON.seconds(json, "nodes_status_delay") |
|
170 |
commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") |
|
67883 | 171 |
} |
67897 | 172 |
yield { |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
173 |
Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
174 |
unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
68908 | 175 |
check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, |
69520 | 176 |
nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) |
67897 | 177 |
} |
67883 | 178 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
179 |
def command(args: Args, |
69012 | 180 |
session: Headless.Session, |
69458 | 181 |
id: UUID.T = UUID.random(), |
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71601
diff
changeset
|
182 |
progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) = |
67883 | 183 |
{ |
184 |
val result = |
|
67937 | 185 |
session.use_theories(args.theories, master_dir = args.master_dir, |
69520 | 186 |
check_delay = args.check_delay.getOrElse(session.default_check_delay), |
187 |
check_limit = args.check_limit.getOrElse(session.default_check_limit), |
|
188 |
watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), |
|
189 |
nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), |
|
190 |
commit_cleanup_delay = |
|
191 |
args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), |
|
67937 | 192 |
id = id, progress = progress) |
67883 | 193 |
|
67901 | 194 |
def output_text(s: String): String = |
195 |
if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
|
67897 | 196 |
|
197 |
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = |
|
198 |
{ |
|
199 |
val position = "pos" -> Position.JSON(pos) |
|
200 |
tree match { |
|
67901 | 201 |
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position |
67897 | 202 |
case elem: XML.Elem => |
203 |
val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) |
|
67923
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67922
diff
changeset
|
204 |
val kind = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67922
diff
changeset
|
205 |
Markup.messages.collectFirst({ case (a, b) if b == elem.name => |
67931
f7917c15b566
field "kind" is always present, with default "writeln";
wenzelm
parents:
67925
diff
changeset
|
206 |
if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" |
f7917c15b566
field "kind" is always present, with default "writeln";
wenzelm
parents:
67925
diff
changeset
|
207 |
Server.Reply.message(output_text(msg), kind = kind) + position |
67897 | 208 |
} |
209 |
} |
|
210 |
||
67883 | 211 |
val result_json = |
212 |
JSON.Object( |
|
213 |
"ok" -> result.ok, |
|
67900 | 214 |
"errors" -> |
215 |
(for { |
|
216 |
(name, status) <- result.nodes if !status.ok |
|
68365 | 217 |
(tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) |
67900 | 218 |
} yield output_message(tree, pos)), |
67883 | 219 |
"nodes" -> |
68365 | 220 |
(for ((name, status) <- result.nodes) yield { |
221 |
val snapshot = result.snapshot(name) |
|
67943 | 222 |
name.json + |
223 |
("status" -> status.json) + |
|
224 |
("messages" -> |
|
67947 | 225 |
(for { |
68365 | 226 |
(tree, pos) <- snapshot.messages if Protocol.is_exported(tree) |
68106 | 227 |
} yield output_message(tree, pos))) + |
228 |
("exports" -> |
|
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
229 |
(if (args.export_pattern == "") Nil else { |
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
230 |
val matcher = Export.make_matcher(args.export_pattern) |
68365 | 231 |
for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
232 |
yield { |
68167 | 233 |
val (base64, body) = entry.uncompressed().maybe_base64 |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
234 |
JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) |
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
235 |
} |
68365 | 236 |
})) |
237 |
})) |
|
67883 | 238 |
|
239 |
(result_json, result) |
|
240 |
} |
|
241 |
} |
|
67941 | 242 |
|
243 |
object Purge_Theories |
|
244 |
{ |
|
245 |
sealed case class Args( |
|
69458 | 246 |
session_id: UUID.T, |
67941 | 247 |
theories: List[String] = Nil, |
248 |
master_dir: String = "", |
|
249 |
all: Boolean = false) |
|
250 |
||
251 |
def unapply(json: JSON.T): Option[Args] = |
|
252 |
for { |
|
253 |
session_id <- JSON.uuid(json, "session_id") |
|
68742 | 254 |
theories <- JSON.strings_default(json, "theories") |
67941 | 255 |
master_dir <- JSON.string_default(json, "master_dir") |
256 |
all <- JSON.bool_default(json, "all") |
|
257 |
} |
|
258 |
yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } |
|
259 |
||
69012 | 260 |
def command(args: Args, session: Headless.Session) |
67943 | 261 |
: (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = |
67941 | 262 |
{ |
67943 | 263 |
val (purged, retained) = |
67941 | 264 |
session.purge_theories( |
265 |
theories = args.theories, master_dir = args.master_dir, all = args.all) |
|
67943 | 266 |
|
267 |
val result_json = |
|
268 |
JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) |
|
269 |
||
270 |
(result_json, (purged, retained)) |
|
67941 | 271 |
} |
272 |
} |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
273 |
} |