1/* Title: Pure/Tools/server_commands.scala 2 Author: Makarius 3 4Miscellaneous Isabelle server commands. 5*/ 6 7package isabelle 8 9 10object Server_Commands 11{ 12 def default_preferences: String = Options.read_prefs() 13 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 24 object Session_Build 25 { 26 sealed case class Args( 27 session: String, 28 preferences: String = default_preferences, 29 options: List[String] = Nil, 30 dirs: List[String] = Nil, 31 include_sessions: List[String] = Nil, 32 system_mode: Boolean = false, 33 verbose: Boolean = false) 34 35 def unapply(json: JSON.T): Option[Args] = 36 for { 37 session <- JSON.string(json, "session") 38 preferences <- JSON.string_default(json, "preferences", default_preferences) 39 options <- JSON.list_default(json, "options", JSON.Value.String.unapply _) 40 dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _) 41 include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _) 42 system_mode <- JSON.bool_default(json, "system_mode") 43 verbose <- JSON.bool_default(json, "verbose") 44 } 45 yield { 46 Args(session, preferences = preferences, options = options, dirs = dirs, 47 include_sessions = include_sessions, system_mode = system_mode, verbose = verbose) 48 } 49 50 def command(args: Args, progress: Progress = No_Progress) 51 : (JSON.Object.T, Build.Results, Sessions.Base_Info) = 52 { 53 val options = Options.init(prefs = args.preferences, opts = args.options) 54 val dirs = args.dirs.map(Path.explode(_)) 55 56 val base_info = 57 Sessions.base_info(options, args.session, progress = progress, dirs = dirs, 58 include_sessions = args.include_sessions) 59 val base = base_info.check_base 60 61 val results = 62 Build.build(options, 63 progress = progress, 64 build_heap = true, 65 system_mode = args.system_mode, 66 dirs = dirs, 67 infos = base_info.infos, 68 verbose = args.verbose, 69 sessions = List(args.session)) 70 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( 77 "ok" -> results.ok, 78 "return_code" -> results.rc, 79 "sessions" -> 80 results.sessions.toList.sortBy(sessions_order).map(session => 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 })) 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) 93 } 94 } 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 109 def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) 110 : (JSON.Object.T, (UUID, Thy_Resources.Session)) = 111 { 112 val base_info = 113 try { Session_Build.command(args.build, progress = progress)._3 } 114 catch { case exn: Server.Error => error(exn.message) } 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 126 val id = UUID() 127 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) 134 } 135 } 136 137 object Session_Stop 138 { 139 def unapply(json: JSON.T): Option[UUID] = 140 JSON.uuid(json, "session_id") 141 142 def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) = 143 { 144 val result = session.stop() 145 val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) 146 147 if (result.ok) (result_json, result) 148 else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json) 149 } 150 } 151 152 object Use_Theories 153 { 154 sealed case class Args( 155 session_id: UUID, 156 theories: List[String], 157 master_dir: String = "", 158 pretty_margin: Double = Pretty.default_margin, 159 unicode_symbols: Boolean = false, 160 export_pattern: String = "", 161 check_delay: Double = Thy_Resources.default_use_theories_check_delay, 162 check_limit: Int = 0) 163 164 def unapply(json: JSON.T): Option[Args] = 165 for { 166 session_id <- JSON.uuid(json, "session_id") 167 theories <- JSON.list(json, "theories", JSON.Value.String.unapply _) 168 master_dir <- JSON.string_default(json, "master_dir") 169 pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) 170 unicode_symbols <- JSON.bool_default(json, "unicode_symbols") 171 export_pattern <- JSON.string_default(json, "export_pattern") 172 check_delay <- 173 JSON.double_default(json, "check_delay", Thy_Resources.default_use_theories_check_delay) 174 check_limit <- JSON.int_default(json, "check_limit") 175 } 176 yield { 177 Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, 178 unicode_symbols = unicode_symbols, export_pattern = export_pattern, 179 check_delay = check_delay, check_limit = check_limit) 180 } 181 182 def command(args: Args, 183 session: Thy_Resources.Session, 184 id: UUID = UUID(), 185 progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) = 186 { 187 val result = 188 session.use_theories(args.theories, master_dir = args.master_dir, 189 check_delay = Time.seconds(args.check_delay), check_limit = args.check_limit, 190 id = id, progress = progress) 191 192 def output_text(s: String): String = 193 if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) 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 { 199 case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position 200 case elem: XML.Elem => 201 val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) 202 val kind = 203 Markup.messages.collectFirst({ case (a, b) if b == elem.name => 204 if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" 205 Server.Reply.message(output_text(msg), kind = kind) + position 206 } 207 } 208 209 val result_json = 210 JSON.Object( 211 "ok" -> result.ok, 212 "errors" -> 213 (for { 214 (name, status) <- result.nodes if !status.ok 215 (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) 216 } yield output_message(tree, pos)), 217 "nodes" -> 218 (for ((name, status) <- result.nodes) yield { 219 val snapshot = result.snapshot(name) 220 name.json + 221 ("status" -> status.json) + 222 ("messages" -> 223 (for { 224 (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) 225 } yield output_message(tree, pos))) + 226 ("exports" -> 227 (if (args.export_pattern == "") Nil else { 228 val matcher = Export.make_matcher(args.export_pattern) 229 for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } 230 yield { 231 val (base64, body) = entry.uncompressed().maybe_base64 232 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) 233 } 234 })) 235 })) 236 237 (result_json, result) 238 } 239 } 240 241 object Purge_Theories 242 { 243 sealed case class Args( 244 session_id: UUID, 245 theories: List[String] = Nil, 246 master_dir: String = "", 247 all: Boolean = false) 248 249 def unapply(json: JSON.T): Option[Args] = 250 for { 251 session_id <- JSON.uuid(json, "session_id") 252 theories <- JSON.list_default(json, "theories", JSON.Value.String.unapply _) 253 master_dir <- JSON.string_default(json, "master_dir") 254 all <- JSON.bool_default(json, "all") 255 } 256 yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } 257 258 def command(args: Args, session: Thy_Resources.Session) 259 : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = 260 { 261 val (purged, retained) = 262 session.purge_theories( 263 theories = args.theories, master_dir = args.master_dir, all = args.all) 264 265 val result_json = 266 JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) 267 268 (result_json, (purged, retained)) 269 } 270 } 271} 272