author | wenzelm |
Thu, 22 Mar 2018 16:20:53 +0100 | |
changeset 67922 | 9e668ae81f97 |
parent 67921 | 1722384ffd4a |
child 67923 | 3e072441c96a |
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 |
def default_qualifier: String = Sessions.DRAFT |
14 |
||
15 |
def unapply_name_pos(json: JSON.T): Option[(String, Position.T)] = |
|
16 |
json match { |
|
17 |
case JSON.Value.String(name) => Some((name, Position.none)) |
|
18 |
case JSON.Object(map) if map.keySet == Set("name", "pos") => |
|
19 |
(map("name"), map("pos")) match { |
|
20 |
case (JSON.Value.String(name), Position.JSON(pos)) => Some((name, pos)) |
|
21 |
case _ => None |
|
22 |
} |
|
23 |
case _ => None |
|
24 |
} |
|
67863 | 25 |
|
67920 | 26 |
object Cancel |
27 |
{ |
|
28 |
sealed case class Args(task: UUID) |
|
29 |
||
30 |
def unapply(json: JSON.T): Option[Args] = |
|
31 |
for { task <- JSON.uuid(json, "task") } |
|
32 |
yield Args(task) |
|
33 |
} |
|
34 |
||
35 |
||
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
36 |
object Session_Build |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
37 |
{ |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
38 |
sealed case class Args( |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
39 |
session: String, |
67863 | 40 |
preferences: String = default_preferences, |
67862 | 41 |
options: List[String] = Nil, |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
42 |
dirs: List[String] = Nil, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
43 |
include_sessions: List[String] = Nil, |
67853 | 44 |
system_mode: Boolean = false, |
45 |
verbose: Boolean = false) |
|
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 |
def unapply(json: JSON.T): Option[Args] = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
48 |
for { |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
49 |
session <- JSON.string(json, "session") |
67863 | 50 |
preferences <- JSON.string_default(json, "preferences", default_preferences) |
67862 | 51 |
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
|
52 |
dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _) |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
53 |
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
|
54 |
system_mode <- JSON.bool_default(json, "system_mode") |
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, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
59 |
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
|
60 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
61 |
|
67886 | 62 |
def command(args: Args, progress: Progress = No_Progress) |
67861 | 63 |
: (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
|
64 |
{ |
67862 | 65 |
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
|
66 |
val dirs = args.dirs.map(Path.explode(_)) |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
67 |
|
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
68 |
val base_info = |
67919
dd90faed43b2
clarified signature: do not expose somewhat accidental internal options;
wenzelm
parents:
67916
diff
changeset
|
69 |
Sessions.base_info(options, args.session, progress = progress, dirs = dirs, |
67922
9e668ae81f97
clarified signature: prefer selective include_sessions;
wenzelm
parents:
67921
diff
changeset
|
70 |
include_sessions = args.include_sessions) |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
71 |
val base = base_info.check_base |
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 = |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
74 |
Build.build(options, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
75 |
progress = progress, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
76 |
build_heap = true, |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
77 |
system_mode = args.system_mode, |
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, |
67853 | 80 |
verbose = args.verbose, |
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
81 |
sessions = List(args.session)) |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
82 |
|
67858 | 83 |
val sessions_order = |
84 |
base_info.sessions_structure.imports_topological_order.zipWithIndex. |
|
85 |
toMap.withDefaultValue(-1) |
|
86 |
||
87 |
val results_json = |
|
88 |
JSON.Object( |
|
67912 | 89 |
"ok" -> results.ok, |
67858 | 90 |
"return_code" -> results.rc, |
91 |
"sessions" -> |
|
92 |
results.sessions.toList.sortBy(sessions_order).map(session => |
|
67912 | 93 |
{ |
94 |
val result = results(session) |
|
95 |
JSON.Object( |
|
96 |
"session" -> session, |
|
97 |
"ok" -> result.ok, |
|
98 |
"return_code" -> result.rc, |
|
99 |
"timeout" -> result.timeout, |
|
100 |
"timing" -> result.timing.json) |
|
101 |
})) |
|
67858 | 102 |
|
103 |
if (results.ok) (results_json, results, base_info) |
|
104 |
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
|
105 |
} |
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
106 |
} |
67869 | 107 |
|
108 |
object Session_Start |
|
109 |
{ |
|
110 |
sealed case class Args( |
|
111 |
build: Session_Build.Args, |
|
112 |
print_mode: List[String] = Nil) |
|
113 |
||
114 |
def unapply(json: JSON.T): Option[Args] = |
|
115 |
for { |
|
116 |
build <- Session_Build.unapply(json) |
|
117 |
print_mode <- JSON.list_default(json, "print_mode", JSON.Value.String.unapply _) |
|
118 |
} |
|
119 |
yield Args(build = build, print_mode = print_mode) |
|
120 |
||
67886 | 121 |
def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) |
67885 | 122 |
: (JSON.Object.T, (UUID, Thy_Resources.Session)) = |
67869 | 123 |
{ |
67914
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
124 |
val base_info = |
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
125 |
try { Session_Build.command(args.build, progress = progress)._3 } |
9f82f6cc3bfc
clarified error result, without JSON object from "session_build";
wenzelm
parents:
67912
diff
changeset
|
126 |
catch { case exn: Server.Error => error(exn.message) } |
67869 | 127 |
|
128 |
val session = |
|
129 |
Thy_Resources.start_session( |
|
130 |
base_info.options, |
|
131 |
base_info.session, |
|
132 |
session_dirs = base_info.dirs, |
|
133 |
session_base = Some(base_info.check_base), |
|
134 |
print_mode = args.print_mode, |
|
135 |
progress = progress, |
|
136 |
log = log) |
|
137 |
||
67885 | 138 |
val id = UUID() |
67869 | 139 |
|
67921 | 140 |
(JSON.Object("session_id" -> id.toString), id -> session) |
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
141 |
} |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
142 |
} |
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 |
object Session_Stop |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
145 |
{ |
67885 | 146 |
def unapply(json: JSON.T): Option[UUID] = |
147 |
JSON.uuid(json, "session_id") |
|
67871
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
148 |
|
67878 | 149 |
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
|
150 |
{ |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
151 |
val result = session.stop() |
67916 | 152 |
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
|
153 |
|
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
154 |
if (result.ok) (result_json, result) |
195ff117894c
store session: per Server/Context, not Connection;
wenzelm
parents:
67869
diff
changeset
|
155 |
else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json) |
67869 | 156 |
} |
157 |
} |
|
67883 | 158 |
|
159 |
object Use_Theories |
|
160 |
{ |
|
161 |
sealed case class Args( |
|
67885 | 162 |
session_id: UUID, |
67883 | 163 |
theories: List[(String, Position.T)], |
164 |
qualifier: String = default_qualifier, |
|
67897 | 165 |
master_dir: String = "", |
166 |
pretty_margin: Double = Pretty.default_margin, |
|
167 |
unicode_symbols: Boolean = false) |
|
67883 | 168 |
|
169 |
def unapply(json: JSON.T): Option[Args] = |
|
170 |
for { |
|
67885 | 171 |
session_id <- JSON.uuid(json, "session_id") |
67883 | 172 |
theories <- JSON.list(json, "theories", unapply_name_pos _) |
173 |
qualifier <- JSON.string_default(json, "qualifier", default_qualifier) |
|
174 |
master_dir <- JSON.string_default(json, "master_dir") |
|
67897 | 175 |
pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) |
176 |
unicode_symbols <- JSON.bool_default(json, "unicode_symbols") |
|
67883 | 177 |
} |
67897 | 178 |
yield { |
179 |
Args(session_id, theories, qualifier = qualifier, master_dir = master_dir, |
|
180 |
pretty_margin = pretty_margin, unicode_symbols) |
|
181 |
} |
|
67883 | 182 |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
183 |
def command(args: Args, |
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
184 |
session: Thy_Resources.Session, |
67885 | 185 |
id: UUID = UUID(), |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
186 |
progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) = |
67883 | 187 |
{ |
188 |
val result = |
|
189 |
session.use_theories(args.theories, qualifier = args.qualifier, |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
190 |
master_dir = args.master_dir, id = id, progress = progress) |
67883 | 191 |
|
67901 | 192 |
def output_text(s: String): String = |
193 |
if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) |
|
67897 | 194 |
|
195 |
def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = |
|
196 |
{ |
|
197 |
val position = "pos" -> Position.JSON(pos) |
|
198 |
tree match { |
|
67901 | 199 |
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position |
67897 | 200 |
case elem: XML.Elem => |
201 |
val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) |
|
67901 | 202 |
val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a }) |
203 |
Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position |
|
67897 | 204 |
} |
205 |
} |
|
206 |
||
67883 | 207 |
val result_json = |
208 |
JSON.Object( |
|
209 |
"ok" -> result.ok, |
|
67900 | 210 |
"errors" -> |
211 |
(for { |
|
212 |
(name, status) <- result.nodes if !status.ok |
|
213 |
(tree, pos) <- result.messages(name) if Protocol.is_error(tree) |
|
214 |
} yield output_message(tree, pos)), |
|
67883 | 215 |
"nodes" -> |
67900 | 216 |
(for ((name, status) <- result.nodes) yield |
67897 | 217 |
JSON.Object( |
218 |
"node_name" -> name.node, |
|
219 |
"theory" -> name.theory, |
|
67900 | 220 |
"status" -> status.json, |
67897 | 221 |
"messages" -> |
67900 | 222 |
(for ((tree, pos) <- result.messages(name)) |
223 |
yield output_message(tree, pos))))) |
|
67883 | 224 |
|
225 |
(result_json, result) |
|
226 |
} |
|
227 |
} |
|
67848
dd83610333de
added server command "session_build": similar to JEdit_Resources.session_build;
wenzelm
parents:
diff
changeset
|
228 |
} |