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.T) 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 verbose: Boolean = false) 33 34 def unapply(json: JSON.T): Option[Args] = 35 for { 36 session <- JSON.string(json, "session") 37 preferences <- JSON.string_default(json, "preferences", default_preferences) 38 options <- JSON.strings_default(json, "options") 39 dirs <- JSON.strings_default(json, "dirs") 40 include_sessions <- JSON.strings_default(json, "include_sessions") 41 verbose <- JSON.bool_default(json, "verbose") 42 } 43 yield { 44 Args(session, preferences = preferences, options = options, dirs = dirs, 45 include_sessions = include_sessions, verbose = verbose) 46 } 47 48 def command(args: Args, progress: Progress = No_Progress) 49 : (JSON.Object.T, Build.Results, Sessions.Base_Info) = 50 { 51 val options = Options.init(prefs = args.preferences, opts = args.options) 52 val dirs = args.dirs.map(Path.explode(_)) 53 54 val base_info = 55 Sessions.base_info(options, args.session, progress = progress, dirs = dirs, 56 include_sessions = args.include_sessions) 57 val base = base_info.check_base 58 59 val results = 60 Build.build(options, 61 progress = progress, 62 build_heap = true, 63 dirs = dirs, 64 infos = base_info.infos, 65 verbose = args.verbose, 66 sessions = List(args.session)) 67 68 val sessions_order = 69 base_info.sessions_structure.imports_topological_order.zipWithIndex. 70 toMap.withDefaultValue(-1) 71 72 val results_json = 73 JSON.Object( 74 "ok" -> results.ok, 75 "return_code" -> results.rc, 76 "sessions" -> 77 results.sessions.toList.sortBy(sessions_order).map(session => 78 { 79 val result = results(session) 80 JSON.Object( 81 "session" -> session, 82 "ok" -> result.ok, 83 "return_code" -> result.rc, 84 "timeout" -> result.timeout, 85 "timing" -> result.timing.json) 86 })) 87 88 if (results.ok) (results_json, results, base_info) 89 else throw new Server.Error("Session build failed: return code " + results.rc, results_json) 90 } 91 } 92 93 object Session_Start 94 { 95 sealed case class Args( 96 build: Session_Build.Args, 97 print_mode: List[String] = Nil) 98 99 def unapply(json: JSON.T): Option[Args] = 100 for { 101 build <- Session_Build.unapply(json) 102 print_mode <- JSON.strings_default(json, "print_mode") 103 } 104 yield Args(build = build, print_mode = print_mode) 105 106 def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger) 107 : (JSON.Object.T, (UUID.T, Headless.Session)) = 108 { 109 val base_info = 110 try { Session_Build.command(args.build, progress = progress)._3 } 111 catch { case exn: Server.Error => error(exn.message) } 112 113 val resources = Headless.Resources(base_info, log = log) 114 115 val session = resources.start_session(print_mode = args.print_mode, progress = progress) 116 117 val id = UUID.random() 118 119 val res = 120 JSON.Object( 121 "session_id" -> id.toString, 122 "tmp_dir" -> File.path(session.tmp_dir).implode) 123 124 (res, id -> session) 125 } 126 } 127 128 object Session_Stop 129 { 130 def unapply(json: JSON.T): Option[UUID.T] = 131 JSON.uuid(json, "session_id") 132 133 def command(session: Headless.Session): (JSON.Object.T, Process_Result) = 134 { 135 val result = session.stop() 136 val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc) 137 138 if (result.ok) (result_json, result) 139 else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json) 140 } 141 } 142 143 object Use_Theories 144 { 145 sealed case class Args( 146 session_id: UUID.T, 147 theories: List[String], 148 master_dir: String = "", 149 pretty_margin: Double = Pretty.default_margin, 150 unicode_symbols: Boolean = false, 151 export_pattern: String = "", 152 check_delay: Option[Time] = None, 153 check_limit: Option[Int] = None, 154 watchdog_timeout: Option[Time] = None, 155 nodes_status_delay: Option[Time] = None, 156 commit_cleanup_delay: Option[Time] = None) 157 158 def unapply(json: JSON.T): Option[Args] = 159 for { 160 session_id <- JSON.uuid(json, "session_id") 161 theories <- JSON.strings(json, "theories") 162 master_dir <- JSON.string_default(json, "master_dir") 163 pretty_margin <- JSON.double_default(json, "pretty_margin", Pretty.default_margin) 164 unicode_symbols <- JSON.bool_default(json, "unicode_symbols") 165 export_pattern <- JSON.string_default(json, "export_pattern") 166 check_delay = JSON.seconds(json, "check_delay") 167 check_limit = JSON.int(json, "check_limit") 168 watchdog_timeout = JSON.seconds(json, "watchdog_timeout") 169 nodes_status_delay = JSON.seconds(json, "nodes_status_delay") 170 commit_cleanup_delay = JSON.seconds(json, "commit_cleanup_delay") 171 } 172 yield { 173 Args(session_id, theories, master_dir = master_dir, pretty_margin = pretty_margin, 174 unicode_symbols = unicode_symbols, export_pattern = export_pattern, 175 check_delay = check_delay, check_limit = check_limit, watchdog_timeout = watchdog_timeout, 176 nodes_status_delay = nodes_status_delay, commit_cleanup_delay = commit_cleanup_delay) 177 } 178 179 def command(args: Args, 180 session: Headless.Session, 181 id: UUID.T = UUID.random(), 182 progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) = 183 { 184 val result = 185 session.use_theories(args.theories, master_dir = args.master_dir, 186 check_delay = args.check_delay.getOrElse(session.default_check_delay), 187 check_limit = args.check_limit.getOrElse(session.default_check_limit), 188 watchdog_timeout = args.watchdog_timeout.getOrElse(session.default_watchdog_timeout), 189 nodes_status_delay = args.nodes_status_delay.getOrElse(session.default_nodes_status_delay), 190 commit_cleanup_delay = 191 args.commit_cleanup_delay.getOrElse(session.default_commit_cleanup_delay), 192 id = id, progress = progress) 193 194 def output_text(s: String): String = 195 if (args.unicode_symbols) Symbol.decode(s) else Symbol.encode(s) 196 197 def output_message(tree: XML.Tree, pos: Position.T): JSON.Object.T = 198 { 199 val position = "pos" -> Position.JSON(pos) 200 tree match { 201 case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position 202 case elem: XML.Elem => 203 val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin)) 204 val kind = 205 Markup.messages.collectFirst({ case (a, b) if b == elem.name => 206 if (Protocol.is_legacy(elem)) Markup.WARNING else a }) getOrElse "" 207 Server.Reply.message(output_text(msg), kind = kind) + position 208 } 209 } 210 211 val result_json = 212 JSON.Object( 213 "ok" -> result.ok, 214 "errors" -> 215 (for { 216 (name, status) <- result.nodes if !status.ok 217 (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) 218 } yield output_message(tree, pos)), 219 "nodes" -> 220 (for ((name, status) <- result.nodes) yield { 221 val snapshot = result.snapshot(name) 222 name.json + 223 ("status" -> status.json) + 224 ("messages" -> 225 (for { 226 (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) 227 } yield output_message(tree, pos))) + 228 ("exports" -> 229 (if (args.export_pattern == "") Nil else { 230 val matcher = Export.make_matcher(args.export_pattern) 231 for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } 232 yield { 233 val (base64, body) = entry.uncompressed().maybe_base64 234 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) 235 } 236 })) 237 })) 238 239 (result_json, result) 240 } 241 } 242 243 object Purge_Theories 244 { 245 sealed case class Args( 246 session_id: UUID.T, 247 theories: List[String] = Nil, 248 master_dir: String = "", 249 all: Boolean = false) 250 251 def unapply(json: JSON.T): Option[Args] = 252 for { 253 session_id <- JSON.uuid(json, "session_id") 254 theories <- JSON.strings_default(json, "theories") 255 master_dir <- JSON.string_default(json, "master_dir") 256 all <- JSON.bool_default(json, "all") 257 } 258 yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) } 259 260 def command(args: Args, session: Headless.Session) 261 : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) = 262 { 263 val (purged, retained) = 264 session.purge_theories( 265 theories = args.theories, master_dir = args.master_dir, all = args.all) 266 267 val result_json = 268 JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json)) 269 270 (result_json, (purged, retained)) 271 } 272 } 273} 274