author | wenzelm |
Fri, 23 Mar 2018 22:53:32 +0100 | |
changeset 67940 | b4e80f062fbf |
parent 67937 | 91eb307511bb |
child 67941 | 49a34b2fa788 |
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) |
67862 | 39 |
options <- JSON.list_default(json, "options", JSON.Value.String.unapply _) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
40 |
dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _) |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
41 |
include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _) |
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) |
|
105 |
print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _) |
|
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, |
|
159 |
unicode_symbols: Boolean = false) |
|
67883 | 160 |
|
161 |
def unapply(json: JSON.T): Option[Args] = |
|
162 |
for { |
|
67885 | 163 |
session_id <- JSON.uuid(json, "session_id") |
67940
b4e80f062fbf
clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents:
67937
diff
changeset
|
164 |
theories <- JSON.list(json, "theories", JSON.Value.String.unapply _) |
67883 | 165 |
master_dir <- JSON.string_default(json, "master_dir") |
67897 | 166 |
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
167 |
unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
|
67883 | 168 |
} |
67897 | 169 |
yield { |
67937 | 170 |
Args(session_id, theories, master_dir = master_dir, |
67897 | 171 |
pretty_margin = pretty_margin, unicode_symbols) |
172 |
} |
|
67883 | 173 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
174 |
def command(args: Args, |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
175 |
session: Thy_Resources.Session, |
67885 | 176 |
id: UUID = UUID(), |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
177 |
progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) = |
67883 | 178 |
{ |
179 |
val result = |
|
67937 | 180 |
session.use_theories(args.theories, master_dir = args.master_dir, |
181 |
id = id, progress = progress) |
|
67883 | 182 |
|
67901 | 183 |
def output_text(s: String): String = |
184 |
if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
|
67897 | 185 |
|
186 |
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = |
|
187 |
{ |
|
188 |
val position = "pos" -> Position.JSON(pos) |
|
189 |
tree match { |
|
67901 | 190 |
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position |
67897 | 191 |
case elem: XML.Elem => |
192 |
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
|
193 |
val kind = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67922
diff
changeset
|
194 |
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
|
195 |
if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" |
f7917c15b566
field "kind" is always present, with default "writeln";
wenzelm
parents:
67925
diff
changeset
|
196 |
Server.Reply.message(output_text(msg), kind = kind) + position |
67897 | 197 |
} |
198 |
} |
|
199 |
||
67883 | 200 |
val result_json = |
201 |
JSON.Object( |
|
202 |
"ok" -> result.ok, |
|
67900 | 203 |
"errors" -> |
204 |
(for { |
|
205 |
(name, status) <- result.nodes if !status.ok |
|
206 |
(tree, pos) <- result.messages(name) if Protocol.is_error(tree) |
|
67923
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67922
diff
changeset
|
207 |
if Protocol.is_exported(tree) |
67900 | 208 |
} yield output_message(tree, pos)), |
67883 | 209 |
"nodes" -> |
67900 | 210 |
(for ((name, status) <- result.nodes) yield |
67897 | 211 |
JSON.Object( |
212 |
"node_name" -> name.node, |
|
213 |
"theory" -> name.theory, |
|
67900 | 214 |
"status" -> status.json, |
67897 | 215 |
"messages" -> |
67900 | 216 |
(for ((tree, pos) <- result.messages(name)) |
217 |
yield output_message(tree, pos))))) |
|
67883 | 218 |
|
219 |
(result_json, result) |
|
220 |
} |
|
221 |
} |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
222 |
} |