author | wenzelm |
Wed, 12 Oct 2022 19:52:03 +0200 | |
changeset 76278 | 6aeb18e8a557 |
parent 75920 | 27bf2533f4a4 |
child 76308 | fdf823f5b56f |
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 |
|
75393 | 10 |
object Server_Commands { |
67863 | 11 |
def default_preferences: String = Options.read_prefs() |
67883 | 12 |
|
75393 | 13 |
object Help extends Server.Command("help") { |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
14 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
15 |
{ case (context, ()) => context.command_list } |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
16 |
} |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
17 |
|
75393 | 18 |
object Echo extends Server.Command("echo") { |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
19 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
20 |
{ case (_, t) => t } |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
21 |
} |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
22 |
|
75393 | 23 |
object Cancel extends Server.Command("cancel") { |
69458 | 24 |
sealed case class Args(task: UUID.T) |
67920 | 25 |
|
26 |
def unapply(json: JSON.T): Option[Args] = |
|
27 |
for { task <- JSON.uuid(json, "task") } |
|
28 |
yield Args(task) |
|
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
29 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
30 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
31 |
{ case (context, Cancel(args)) => context.cancel_task(args.task) } |
67920 | 32 |
} |
33 |
||
75393 | 34 |
object Shutdown extends Server.Command("shutdown") { |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
35 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
36 |
{ case (context, ()) => context.server.shutdown() } |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
37 |
} |
67920 | 38 |
|
75393 | 39 |
object Session_Build extends Server.Command("session_build") { |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
40 |
sealed case class Args( |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
41 |
session: String, |
67863 | 42 |
preferences: String = default_preferences, |
67862 | 43 |
options: List[String] = Nil, |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
44 |
dirs: List[String] = Nil, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
45 |
include_sessions: List[String] = Nil, |
67853 | 46 |
verbose: Boolean = false) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
47 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
48 |
def unapply(json: JSON.T): Option[Args] = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
49 |
for { |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
50 |
session <- JSON.string(json, "session") |
67863 | 51 |
preferences <- JSON.string_default(json, "preferences", default_preferences) |
68742 | 52 |
options <- JSON.strings_default(json, "options") |
53 |
dirs <- JSON.strings_default(json, "dirs") |
|
54 |
include_sessions <- JSON.strings_default(json, "include_sessions") |
|
67853 | 55 |
verbose <- JSON.bool_default(json, "verbose") |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
56 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
57 |
yield { |
67862 | 58 |
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
|
59 |
include_sessions = include_sessions, verbose = verbose) |
67848
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 |
|
75393 | 62 |
def command( |
63 |
args: Args, |
|
64 |
progress: Progress = new Progress |
|
65 |
) : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) = { |
|
67862 | 66 |
val options = Options.init(prefs = args.preferences, opts = args.options) |
71601 | 67 |
val dirs = args.dirs.map(Path.explode) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
68 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
69 |
val base_info = |
67919
dd90faed43b2
clarified signature: do not expose somewhat accidental internal options;
wenzelm
parents:
67916
diff
changeset
|
70 |
Sessions.base_info(options, args.session, progress = progress, dirs = dirs, |
75920
27bf2533f4a4
clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);
wenzelm
parents:
75674
diff
changeset
|
71 |
include_sessions = args.include_sessions).check_errors |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
72 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
73 |
val results = |
71981 | 74 |
Build.build(options, |
75 |
selection = Sessions.Selection.session(args.session), |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
76 |
progress = progress, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
77 |
build_heap = true, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
78 |
dirs = dirs, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
79 |
infos = base_info.infos, |
71896
ce06d6456cc8
clarified signature --- fit within limit of 22 arguments;
wenzelm
parents:
71747
diff
changeset
|
80 |
verbose = args.verbose) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
81 |
|
67858 | 82 |
val sessions_order = |
83 |
base_info.sessions_structure.imports_topological_order.zipWithIndex. |
|
84 |
toMap.withDefaultValue(-1) |
|
85 |
||
86 |
val results_json = |
|
87 |
JSON.Object( |
|
67912 | 88 |
"ok" -> results.ok, |
67858 | 89 |
"return_code" -> results.rc, |
90 |
"sessions" -> |
|
75394 | 91 |
results.sessions.toList.sortBy(sessions_order).map { session => |
75393 | 92 |
val result = results(session) |
93 |
JSON.Object( |
|
94 |
"session" -> session, |
|
95 |
"ok" -> result.ok, |
|
96 |
"return_code" -> result.rc, |
|
97 |
"timeout" -> result.timeout, |
|
98 |
"timing" -> result.timing.json) |
|
75394 | 99 |
}) |
67858 | 100 |
|
71599 | 101 |
if (results.ok) (results_json, results, options, base_info) |
71747 | 102 |
else { |
74306 | 103 |
throw new Server.Error("Session build failed: " + Process_Result.RC.print(results.rc), |
71747 | 104 |
results_json) |
105 |
} |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
106 |
} |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
107 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
108 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
109 |
{ case (context, Session_Build(args)) => |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
110 |
context.make_task(task => Session_Build.command(args, progress = task.progress)._1) } |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
111 |
} |
67869 | 112 |
|
75393 | 113 |
object Session_Start extends Server.Command("session_start") { |
67869 | 114 |
sealed case class Args( |
115 |
build: Session_Build.Args, |
|
116 |
print_mode: List[String] = Nil) |
|
117 |
||
118 |
def unapply(json: JSON.T): Option[Args] = |
|
119 |
for { |
|
120 |
build <- Session_Build.unapply(json) |
|
68742 | 121 |
print_mode <- JSON.strings_default(json, "print_mode") |
67869 | 122 |
} |
123 |
yield Args(build = build, print_mode = print_mode) |
|
124 |
||
75393 | 125 |
def command( |
126 |
args: Args, |
|
127 |
progress: Progress = new Progress, |
|
128 |
log: Logger = No_Logger |
|
129 |
) : (JSON.Object.T, (UUID.T, Headless.Session)) = { |
|
71599 | 130 |
val (_, _, options, base_info) = |
131 |
try { Session_Build.command(args.build, progress = progress) } |
|
67914
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
132 |
catch { case exn: Server.Error => error(exn.message) } |
67869 | 133 |
|
71599 | 134 |
val resources = Headless.Resources(options, base_info, log = log) |
69536 | 135 |
|
136 |
val session = resources.start_session(print_mode = args.print_mode, progress = progress) |
|
67869 | 137 |
|
69458 | 138 |
val id = UUID.random() |
67869 | 139 |
|
67925 | 140 |
val res = |
141 |
JSON.Object( |
|
142 |
"session_id" -> id.toString, |
|
143 |
"tmp_dir" -> File.path(session.tmp_dir).implode) |
|
144 |
||
145 |
(res, id -> session) |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
146 |
} |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
147 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
148 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
149 |
{ case (context, Session_Start(args)) => |
75394 | 150 |
context.make_task { task => |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
151 |
val (res, entry) = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
152 |
Session_Start.command(args, progress = task.progress, log = context.server.log) |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
153 |
context.server.add_session(entry) |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
154 |
res |
75394 | 155 |
} |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
156 |
} |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
157 |
} |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
158 |
|
75393 | 159 |
object Session_Stop extends Server.Command("session_stop") { |
69458 | 160 |
def unapply(json: JSON.T): Option[UUID.T] = |
67885 | 161 |
JSON.uuid(json, "session_id") |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
162 |
|
75393 | 163 |
def command(session: Headless.Session): (JSON.Object.T, Process_Result) = { |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
164 |
val result = session.stop() |
67916 | 165 |
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
|
166 |
|
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
167 |
if (result.ok) (result_json, result) |
71747 | 168 |
else throw new Server.Error("Session shutdown failed: " + result.print_rc, result_json) |
67869 | 169 |
} |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
170 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
171 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
172 |
{ case (context, Session_Stop(id)) => |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
173 |
context.make_task(_ => |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
174 |
{ |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
175 |
val session = context.server.remove_session(id) |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
176 |
Session_Stop.command(session)._1 |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
177 |
}) |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
178 |
} |
67869 | 179 |
} |
67883 | 180 |
|
75393 | 181 |
object Use_Theories extends Server.Command("use_theories") { |
67883 | 182 |
sealed case class Args( |
69458 | 183 |
session_id: UUID.T, |
67940
b4e80f062fbf
clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents:
67937
diff
changeset
|
184 |
theories: List[String], |
67897 | 185 |
master_dir: String = "", |
186 |
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
|
187 |
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
|
188 |
export_pattern: String = "", |
69520 | 189 |
check_delay: Option[Time] = None, |
190 |
check_limit: Option[Int] = None, |
|
191 |
watchdog_timeout: Option[Time] = None, |
|
192 |
nodes_status_delay: Option[Time] = None, |
|
193 |
commit_cleanup_delay: Option[Time] = None) |
|
67883 | 194 |
|
195 |
def unapply(json: JSON.T): Option[Args] = |
|
196 |
for { |
|
67885 | 197 |
session_id <- JSON.uuid(json, "session_id") |
68742 | 198 |
theories <- JSON.strings(json, "theories") |
67883 | 199 |
master_dir <- JSON.string_default(json, "master_dir") |
67897 | 200 |
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
201 |
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
|
202 |
export_pattern <- JSON.string_default(json, "export_pattern") |
69520 | 203 |
check_delay = JSON.seconds(json, "check_delay") |
204 |
check_limit = JSON.int(json, "check_limit") |
|
205 |
watchdog_timeout = JSON.seconds(json, "watchdog_timeout") |
|
206 |
nodes_status_delay = JSON.seconds(json, "nodes_status_delay") |
|
207 |
commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") |
|
67883 | 208 |
} |
67897 | 209 |
yield { |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
210 |
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
|
211 |
unicode_symbols = unicode_symbols, export_pattern = export_pattern, |
68908 | 212 |
check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, |
69520 | 213 |
nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) |
67897 | 214 |
} |
67883 | 215 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
216 |
def command(args: Args, |
69012 | 217 |
session: Headless.Session, |
69458 | 218 |
id: UUID.T = UUID.random(), |
75393 | 219 |
progress: Progress = new Progress |
220 |
): (JSON.Object.T, Headless.Use_Theories_Result) = { |
|
67883 | 221 |
val result = |
67937 | 222 |
session.use_theories(args.theories, master_dir = args.master_dir, |
69520 | 223 |
check_delay = args.check_delay.getOrElse(session.default_check_delay), |
224 |
check_limit = args.check_limit.getOrElse(session.default_check_limit), |
|
225 |
watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), |
|
226 |
nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), |
|
227 |
commit_cleanup_delay = |
|
228 |
args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), |
|
67937 | 229 |
id = id, progress = progress) |
67883 | 230 |
|
72866 | 231 |
def output_text(text: String): String = |
232 |
Symbol.output(args.unicode_symbols, text) |
|
67897 | 233 |
|
75393 | 234 |
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = { |
67897 | 235 |
val position = "pos" -> Position.JSON(pos) |
236 |
tree match { |
|
67901 | 237 |
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position |
67897 | 238 |
case elem: XML.Elem => |
239 |
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
|
240 |
val kind = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67922
diff
changeset
|
241 |
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
|
242 |
if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" |
f7917c15b566
field "kind" is always present, with default "writeln";
wenzelm
parents:
67925
diff
changeset
|
243 |
Server.Reply.message(output_text(msg), kind = kind) + position |
67897 | 244 |
} |
245 |
} |
|
246 |
||
67883 | 247 |
val result_json = |
248 |
JSON.Object( |
|
249 |
"ok" -> result.ok, |
|
67900 | 250 |
"errors" -> |
251 |
(for { |
|
252 |
(name, status) <- result.nodes if !status.ok |
|
68365 | 253 |
(tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) |
67900 | 254 |
} yield output_message(tree, pos)), |
67883 | 255 |
"nodes" -> |
68365 | 256 |
(for ((name, status) <- result.nodes) yield { |
257 |
val snapshot = result.snapshot(name) |
|
67943 | 258 |
name.json + |
259 |
("status" -> status.json) + |
|
260 |
("messages" -> |
|
67947 | 261 |
(for { |
68365 | 262 |
(tree, pos) <- snapshot.messages if Protocol.is_exported(tree) |
68106 | 263 |
} yield output_message(tree, pos))) + |
264 |
("exports" -> |
|
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
265 |
(if (args.export_pattern == "") Nil else { |
75658
5905c7f484b3
clarified signature: read_theory_exports is already ordered;
wenzelm
parents:
75587
diff
changeset
|
266 |
val matcher = Export.make_matcher(List(args.export_pattern)) |
75674 | 267 |
for { entry <- snapshot.exports if matcher(entry.entry_name) } |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
268 |
yield { |
75587 | 269 |
val (base64, body) = entry.uncompressed.maybe_encode_base64 |
68152
619de043389f
guard result exports via export_pattern -- avoid bombing client via huge blobs;
wenzelm
parents:
68106
diff
changeset
|
270 |
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
|
271 |
} |
68365 | 272 |
})) |
273 |
})) |
|
67883 | 274 |
|
275 |
(result_json, result) |
|
276 |
} |
|
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
277 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
278 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
279 |
{ case (context, Use_Theories(args)) => |
75394 | 280 |
context.make_task { task => |
281 |
val session = context.server.the_session(args.session_id) |
|
282 |
Use_Theories.command(args, session, id = task.id, progress = task.progress)._1 |
|
283 |
} |
|
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
284 |
} |
67883 | 285 |
} |
67941 | 286 |
|
75393 | 287 |
object Purge_Theories extends Server.Command("purge_theories") { |
67941 | 288 |
sealed case class Args( |
69458 | 289 |
session_id: UUID.T, |
67941 | 290 |
theories: List[String] = Nil, |
291 |
master_dir: String = "", |
|
292 |
all: Boolean = false) |
|
293 |
||
294 |
def unapply(json: JSON.T): Option[Args] = |
|
295 |
for { |
|
296 |
session_id <- JSON.uuid(json, "session_id") |
|
68742 | 297 |
theories <- JSON.strings_default(json, "theories") |
67941 | 298 |
master_dir <- JSON.string_default(json, "master_dir") |
299 |
all <- JSON.bool_default(json, "all") |
|
300 |
} |
|
301 |
yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } |
|
302 |
||
75393 | 303 |
def command( |
304 |
args: Args, |
|
305 |
session: Headless.Session |
|
306 |
) : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = { |
|
67943 | 307 |
val (purged, retained) = |
67941 | 308 |
session.purge_theories( |
309 |
theories = args.theories, master_dir = args.master_dir, all = args.all) |
|
67943 | 310 |
|
311 |
val result_json = |
|
312 |
JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) |
|
313 |
||
314 |
(result_json, (purged, retained)) |
|
67941 | 315 |
} |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
316 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
317 |
override val command_body: Server.Command_Body = |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
318 |
{ case (context, Purge_Theories(args)) => |
76278 | 319 |
val session = context.server.the_session(args.session_id) |
320 |
command(args, session)._1 |
|
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
321 |
} |
67941 | 322 |
} |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
323 |
} |
72163
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
324 |
|
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
325 |
class Server_Commands extends Server.Commands( |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
326 |
Server_Commands.Help, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
327 |
Server_Commands.Echo, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
328 |
Server_Commands.Cancel, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
329 |
Server_Commands.Shutdown, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
330 |
Server_Commands.Session_Build, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
331 |
Server_Commands.Session_Start, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
332 |
Server_Commands.Session_Stop, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
333 |
Server_Commands.Use_Theories, |
f5722290a4d0
allow user-defined server commands via isabelle_scala_service;
wenzelm
parents:
71981
diff
changeset
|
334 |
Server_Commands.Purge_Theories) |