author | wenzelm |
Sat, 08 Sep 2018 12:01:37 +0200 | |
changeset 68943 | e564605d4cac |
parent 68908 | abc338d25640 |
child 68947 | ea804c814693 |
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 |
{ |
|
16 |
sealed case class Args(task: UUID) |
|
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 |
system_mode: Boolean = false, |
33 |
verbose: Boolean = false) |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
34 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
35 |
def unapply(json: JSON.T): Option[Args] = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
36 |
for { |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
37 |
session <- JSON.string(json, "session") |
67863 | 38 |
preferences <- JSON.string_default(json, "preferences", default_preferences) |
68742 | 39 |
options <- JSON.strings_default(json, "options") |
40 |
dirs <- JSON.strings_default(json, "dirs") |
|
41 |
include_sessions <- JSON.strings_default(json, "include_sessions") |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
42 |
system_mode <- JSON.bool_default(json, "system_mode") |
67853 | 43 |
verbose <- JSON.bool_default(json, "verbose") |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
44 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
45 |
yield { |
67862 | 46 |
Args(session, preferences = preferences, options = options, dirs = dirs, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
47 |
include_sessions = include_sessions, system_mode = system_mode, verbose = verbose) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
48 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
49 |
|
67886 | 50 |
def command(args: Args, progress: Progress = No_Progress) |
67861 | 51 |
: (JSON.Object.T, Build.Results, Sessions.Base_Info) = |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
52 |
{ |
67862 | 53 |
val options = Options.init(prefs = args.preferences, opts = args.options) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
54 |
val dirs = args.dirs.map(Path.explode(_)) |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
55 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
56 |
val base_info = |
67919
dd90faed43b2
clarified signature: do not expose somewhat accidental internal options;
wenzelm
parents:
67916
diff
changeset
|
57 |
Sessions.base_info(options, args.session, progress = progress, dirs = dirs, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
58 |
include_sessions = args.include_sessions) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
59 |
val base = base_info.check_base |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
60 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
61 |
val results = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
62 |
Build.build(options, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
63 |
progress = progress, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
64 |
build_heap = true, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
65 |
system_mode = args.system_mode, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
66 |
dirs = dirs, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
67 |
infos = base_info.infos, |
67853 | 68 |
verbose = args.verbose, |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
69 |
sessions = List(args.session)) |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
70 |
|
67858 | 71 |
val sessions_order = |
72 |
base_info.sessions_structure.imports_topological_order.zipWithIndex. |
|
73 |
toMap.withDefaultValue(-1) |
|
74 |
||
75 |
val results_json = |
|
76 |
JSON.Object( |
|
67912 | 77 |
"ok" -> results.ok, |
67858 | 78 |
"return_code" -> results.rc, |
79 |
"sessions" -> |
|
80 |
results.sessions.toList.sortBy(sessions_order).map(session => |
|
67912 | 81 |
{ |
82 |
val result = results(session) |
|
83 |
JSON.Object( |
|
84 |
"session" -> session, |
|
85 |
"ok" -> result.ok, |
|
86 |
"return_code" -> result.rc, |
|
87 |
"timeout" -> result.timeout, |
|
88 |
"timing" -> result.timing.json) |
|
89 |
})) |
|
67858 | 90 |
|
91 |
if (results.ok) (results_json, results, base_info) |
|
92 |
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
|
93 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
94 |
} |
67869 | 95 |
|
96 |
object Session_Start |
|
97 |
{ |
|
98 |
sealed case class Args( |
|
99 |
build: Session_Build.Args, |
|
100 |
print_mode: List[String] = Nil) |
|
101 |
||
102 |
def unapply(json: JSON.T): Option[Args] = |
|
103 |
for { |
|
104 |
build <- Session_Build.unapply(json) |
|
68742 | 105 |
print_mode <- JSON.strings_default(json, "print_mode") |
67869 | 106 |
} |
107 |
yield Args(build = build, print_mode = print_mode) |
|
108 |
||
67886 | 109 |
def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) |
67885 | 110 |
: (JSON.Object.T, (UUID, Thy_Resources.Session)) = |
67869 | 111 |
{ |
67914
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
112 |
val base_info = |
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
113 |
try { Session_Build.command(args.build, progress = progress)._3 } |
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
114 |
catch { case exn: Server.Error => error(exn.message) } |
67869 | 115 |
|
116 |
val session = |
|
117 |
Thy_Resources.start_session( |
|
118 |
base_info.options, |
|
119 |
base_info.session, |
|
120 |
session_dirs = base_info.dirs, |
|
121 |
session_base = Some(base_info.check_base), |
|
122 |
print_mode = args.print_mode, |
|
123 |
progress = progress, |
|
124 |
log = log) |
|
125 |
||
67885 | 126 |
val id = UUID() |
67869 | 127 |
|
67925 | 128 |
val res = |
129 |
JSON.Object( |
|
130 |
"session_id" -> id.toString, |
|
131 |
"tmp_dir" -> File.path(session.tmp_dir).implode) |
|
132 |
||
133 |
(res, id -> session) |
|
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 |
} |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
136 |
|
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
137 |
object Session_Stop |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
138 |
{ |
67885 | 139 |
def unapply(json: JSON.T): Option[UUID] = |
140 |
JSON.uuid(json, "session_id") |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
141 |
|
67878 | 142 |
def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) = |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
143 |
{ |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
144 |
val result = session.stop() |
67916 | 145 |
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
|
146 |
|
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
147 |
if (result.ok) (result_json, result) |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
148 |
else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json) |
67869 | 149 |
} |
150 |
} |
|
67883 | 151 |
|
152 |
object Use_Theories |
|
153 |
{ |
|
154 |
sealed case class Args( |
|
67885 | 155 |
session_id: UUID, |
67940
b4e80f062fbf
clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents:
67937
diff
changeset
|
156 |
theories: List[String], |
67897 | 157 |
master_dir: String = "", |
158 |
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
|
159 |
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
|
160 |
export_pattern: String = "", |
68943 | 161 |
check_delay: Time = Thy_Resources.default_check_delay, |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68742
diff
changeset
|
162 |
check_limit: Int = 0, |
68943 | 163 |
watchdog_timeout: Time = Time.zero, |
164 |
nodes_status_delay: Time = Thy_Resources.default_nodes_status_delay) |
|
67883 | 165 |
|
166 |
def unapply(json: JSON.T): Option[Args] = |
|
167 |
for { |
|
67885 | 168 |
session_id <- JSON.uuid(json, "session_id") |
68742 | 169 |
theories <- JSON.strings(json, "theories") |
67883 | 170 |
master_dir <- JSON.string_default(json, "master_dir") |
67897 | 171 |
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
172 |
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
|
173 |
export_pattern <- JSON.string_default(json, "export_pattern") |
68943 | 174 |
check_delay <- JSON.seconds_default(json, "check_delay", Thy_Resources.default_check_delay) |
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
|
175 |
check_limit <- JSON.int_default(json, "check_limit") |
68943 | 176 |
watchdog_timeout <- JSON.seconds_default(json, "watchdog_timeout") |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68742
diff
changeset
|
177 |
nodes_status_delay <- |
68943 | 178 |
JSON.seconds_default(json, "nodes_status_delay", Thy_Resources.default_nodes_status_delay) |
67883 | 179 |
} |
67897 | 180 |
yield { |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
181 |
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
|
182 |
unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
68908 | 183 |
check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68742
diff
changeset
|
184 |
nodes_status_delay = nodes_status_delay) |
67897 | 185 |
} |
67883 | 186 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
187 |
def command(args: Args, |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
188 |
session: Thy_Resources.Session, |
67885 | 189 |
id: UUID = UUID(), |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
190 |
progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) = |
67883 | 191 |
{ |
192 |
val result = |
|
67937 | 193 |
session.use_theories(args.theories, master_dir = args.master_dir, |
68943 | 194 |
check_delay = args.check_delay, check_limit = args.check_limit, |
195 |
watchdog_timeout = args.watchdog_timeout, |
|
196 |
nodes_status_delay = args.nodes_status_delay, |
|
67937 | 197 |
id = id, progress = progress) |
67883 | 198 |
|
67901 | 199 |
def output_text(s: String): String = |
200 |
if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
|
67897 | 201 |
|
202 |
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = |
|
203 |
{ |
|
204 |
val position = "pos" -> Position.JSON(pos) |
|
205 |
tree match { |
|
67901 | 206 |
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position |
67897 | 207 |
case elem: XML.Elem => |
208 |
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
|
209 |
val kind = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67922
diff
changeset
|
210 |
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
|
211 |
if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" |
f7917c15b566
field "kind" is always present, with default "writeln";
wenzelm
parents:
67925
diff
changeset
|
212 |
Server.Reply.message(output_text(msg), kind = kind) + position |
67897 | 213 |
} |
214 |
} |
|
215 |
||
67883 | 216 |
val result_json = |
217 |
JSON.Object( |
|
218 |
"ok" -> result.ok, |
|
67900 | 219 |
"errors" -> |
220 |
(for { |
|
221 |
(name, status) <- result.nodes if !status.ok |
|
68365 | 222 |
(tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) |
67900 | 223 |
} yield output_message(tree, pos)), |
67883 | 224 |
"nodes" -> |
68365 | 225 |
(for ((name, status) <- result.nodes) yield { |
226 |
val snapshot = result.snapshot(name) |
|
67943 | 227 |
name.json + |
228 |
("status" -> status.json) + |
|
229 |
("messages" -> |
|
67947 | 230 |
(for { |
68365 | 231 |
(tree, pos) <- snapshot.messages if Protocol.is_exported(tree) |
68106 | 232 |
} yield output_message(tree, pos))) + |
233 |
("exports" -> |
|
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
234 |
(if (args.export_pattern == "") Nil else { |
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
235 |
val matcher = Export.make_matcher(args.export_pattern) |
68365 | 236 |
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
|
237 |
yield { |
68167 | 238 |
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
|
239 |
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
|
240 |
} |
68365 | 241 |
})) |
242 |
})) |
|
67883 | 243 |
|
244 |
(result_json, result) |
|
245 |
} |
|
246 |
} |
|
67941 | 247 |
|
248 |
object Purge_Theories |
|
249 |
{ |
|
250 |
sealed case class Args( |
|
251 |
session_id: UUID, |
|
252 |
theories: List[String] = Nil, |
|
253 |
master_dir: String = "", |
|
254 |
all: Boolean = false) |
|
255 |
||
256 |
def unapply(json: JSON.T): Option[Args] = |
|
257 |
for { |
|
258 |
session_id <- JSON.uuid(json, "session_id") |
|
68742 | 259 |
theories <- JSON.strings_default(json, "theories") |
67941 | 260 |
master_dir <- JSON.string_default(json, "master_dir") |
261 |
all <- JSON.bool_default(json, "all") |
|
262 |
} |
|
263 |
yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } |
|
264 |
||
265 |
def command(args: Args, session: Thy_Resources.Session) |
|
67943 | 266 |
: (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = |
67941 | 267 |
{ |
67943 | 268 |
val (purged, retained) = |
67941 | 269 |
session.purge_theories( |
270 |
theories = args.theories, master_dir = args.master_dir, all = args.all) |
|
67943 | 271 |
|
272 |
val result_json = |
|
273 |
JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) |
|
274 |
||
275 |
(result_json, (purged, retained)) |
|
67941 | 276 |
} |
277 |
} |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
278 |
} |