1/* Title: Pure/PIDE/protocol.scala 2 Author: Makarius 3 4Protocol message formats for interactive proof documents. 5*/ 6 7package isabelle 8 9 10object Protocol 11{ 12 /* document editing */ 13 14 object Commands_Accepted 15 { 16 def unapply(text: String): Option[List[Document_ID.Command]] = 17 try { Some(space_explode(',', text).map(Value.Long.parse)) } 18 catch { case ERROR(_) => None } 19 20 val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED))) 21 } 22 23 object Assign_Update 24 { 25 def unapply(text: String) 26 : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = 27 { 28 try { 29 import XML.Decode._ 30 def decode_upd(body: XML.Body): (Long, List[Long]) = 31 space_explode(',', string(body)).map(Value.Long.parse) match { 32 case a :: bs => (a, bs) 33 case _ => throw new XML.XML_Body(body) 34 } 35 Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text))) 36 } 37 catch { 38 case ERROR(_) => None 39 case _: XML.Error => None 40 } 41 } 42 } 43 44 object Removed 45 { 46 def unapply(text: String): Option[List[Document_ID.Version]] = 47 try { 48 import XML.Decode._ 49 Some(list(long)(Symbol.decode_yxml(text))) 50 } 51 catch { 52 case ERROR(_) => None 53 case _: XML.Error => None 54 } 55 } 56 57 58 /* command timing */ 59 60 object Command_Timing 61 { 62 def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] = 63 props match { 64 case Markup.COMMAND_TIMING :: args => 65 (args, args) match { 66 case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing)) 67 case _ => None 68 } 69 case _ => None 70 } 71 } 72 73 74 /* theory timing */ 75 76 object Theory_Timing 77 { 78 def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = 79 props match { 80 case Markup.THEORY_TIMING :: args => 81 (args, args) match { 82 case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) 83 case _ => None 84 } 85 case _ => None 86 } 87 } 88 89 90 /* result messages */ 91 92 def is_result(msg: XML.Tree): Boolean = 93 msg match { 94 case XML.Elem(Markup(Markup.RESULT, _), _) => true 95 case _ => false 96 } 97 98 def is_tracing(msg: XML.Tree): Boolean = 99 msg match { 100 case XML.Elem(Markup(Markup.TRACING, _), _) => true 101 case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true 102 case _ => false 103 } 104 105 def is_state(msg: XML.Tree): Boolean = 106 msg match { 107 case XML.Elem(Markup(Markup.STATE, _), _) => true 108 case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true 109 case _ => false 110 } 111 112 def is_information(msg: XML.Tree): Boolean = 113 msg match { 114 case XML.Elem(Markup(Markup.INFORMATION, _), _) => true 115 case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true 116 case _ => false 117 } 118 119 def is_writeln(msg: XML.Tree): Boolean = 120 msg match { 121 case XML.Elem(Markup(Markup.WRITELN, _), _) => true 122 case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true 123 case _ => false 124 } 125 126 def is_warning(msg: XML.Tree): Boolean = 127 msg match { 128 case XML.Elem(Markup(Markup.WARNING, _), _) => true 129 case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true 130 case _ => false 131 } 132 133 def is_legacy(msg: XML.Tree): Boolean = 134 msg match { 135 case XML.Elem(Markup(Markup.LEGACY, _), _) => true 136 case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true 137 case _ => false 138 } 139 140 def is_error(msg: XML.Tree): Boolean = 141 msg match { 142 case XML.Elem(Markup(Markup.ERROR, _), _) => true 143 case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true 144 case _ => false 145 } 146 147 def is_inlined(msg: XML.Tree): Boolean = 148 !(is_result(msg) || is_tracing(msg) || is_state(msg)) 149 150 def is_exported(msg: XML.Tree): Boolean = 151 is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) 152 153 def message_text(msg: XML.Tree): String = 154 { 155 val text = Pretty.string_of(List(msg)) 156 if (is_warning(msg) || is_legacy(msg)) Library.prefix_lines("### ", text) 157 else if (is_error(msg)) Library.prefix_lines("*** ", text) 158 else text 159 } 160 161 162 /* breakpoints */ 163 164 object ML_Breakpoint 165 { 166 def unapply(tree: XML.Tree): Option[Long] = 167 tree match { 168 case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) 169 case _ => None 170 } 171 } 172 173 174 /* dialogs */ 175 176 object Dialog_Args 177 { 178 def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = 179 (props, props, props) match { 180 case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => 181 Some((id, serial, result)) 182 case _ => None 183 } 184 } 185 186 object Dialog 187 { 188 def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = 189 tree match { 190 case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => 191 Some((id, serial, result)) 192 case _ => None 193 } 194 } 195 196 object Dialog_Result 197 { 198 def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = 199 { 200 val props = Position.Id(id) ::: Markup.Serial(serial) 201 XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) 202 } 203 204 def unapply(tree: XML.Tree): Option[String] = 205 tree match { 206 case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) 207 case _ => None 208 } 209 } 210} 211 212 213trait Protocol 214{ 215 /* protocol commands */ 216 217 def protocol_command_raw(name: String, args: List[Bytes]): Unit 218 def protocol_command_args(name: String, args: List[String]) 219 def protocol_command(name: String, args: String*): Unit 220 221 222 /* options */ 223 224 def options(opts: Options): Unit = 225 protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) 226 227 228 /* session base */ 229 230 private def encode_table(table: List[(String, String)]): String = 231 { 232 import XML.Encode._ 233 Symbol.encode_yxml(list(pair(string, string))(table)) 234 } 235 236 private def encode_list(lst: List[String]): String = 237 { 238 import XML.Encode._ 239 Symbol.encode_yxml(list(string)(lst)) 240 } 241 242 private def encode_sessions(lst: List[(String, Position.T)]): String = 243 { 244 import XML.Encode._ 245 Symbol.encode_yxml(list(pair(string, properties))(lst)) 246 } 247 248 def session_base(resources: Resources) 249 { 250 protocol_command("Prover.init_session_base", 251 encode_sessions(resources.sessions_structure.session_positions), 252 encode_table(resources.sessions_structure.dest_session_directories), 253 encode_list(resources.session_base.doc_names), 254 encode_table(resources.session_base.global_theories.toList), 255 encode_list(resources.session_base.loaded_theories.keys)) 256 } 257 258 259 /* interned items */ 260 261 def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = 262 protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes)) 263 264 private def encode_command(command: Command): (String, String, String, String, List[String]) = 265 { 266 import XML.Encode._ 267 268 val blobs_yxml = 269 { 270 val encode_blob: T[Command.Blob] = 271 variant(List( 272 { case Exn.Res((a, b)) => 273 (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, 274 { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) 275 276 Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) 277 } 278 279 val toks_yxml = 280 { 281 val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) 282 Symbol.encode_yxml(list(encode_tok)(command.span.content)) 283 } 284 val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source)) 285 286 (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources) 287 } 288 289 def define_command(command: Command) 290 { 291 val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) 292 protocol_command_args( 293 "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources) 294 } 295 296 def define_commands(commands: List[Command]) 297 { 298 protocol_command_args("Document.define_commands", 299 commands.map(command => 300 { 301 import XML.Encode._ 302 val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) 303 val body = 304 pair(string, pair(string, pair(string, pair(string, list(string)))))( 305 command_id, (name, (blobs_yxml, (toks_yxml, toks_sources)))) 306 YXML.string_of_body(body) 307 })) 308 } 309 310 def define_commands_bulk(commands: List[Command]) 311 { 312 val (irregular, regular) = commands.partition(command => YXML.detect(command.source)) 313 irregular.foreach(define_command(_)) 314 regular match { 315 case Nil => 316 case List(command) => define_command(command) 317 case _ => define_commands(regular) 318 } 319 } 320 321 322 /* execution */ 323 324 def discontinue_execution(): Unit = 325 protocol_command("Document.discontinue_execution") 326 327 def cancel_exec(id: Document_ID.Exec): Unit = 328 protocol_command("Document.cancel_exec", Document_ID(id)) 329 330 331 /* document versions */ 332 333 def update(old_id: Document_ID.Version, new_id: Document_ID.Version, 334 edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) 335 { 336 val consolidate_yxml = 337 { 338 import XML.Encode._ 339 Symbol.encode_yxml(list(string)(consolidate.map(_.node))) 340 } 341 val edits_yxml = 342 { 343 import XML.Encode._ 344 def id: T[Command] = (cmd => long(cmd.id)) 345 def encode_edit(name: Document.Node.Name) 346 : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = 347 variant(List( 348 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, 349 { case Document.Node.Deps(header) => 350 val master_dir = File.standard_url(name.master_dir) 351 val imports = header.imports.map(_.node) 352 val keywords = 353 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) 354 (Nil, 355 pair(string, pair(string, pair(list(string), pair(list(pair(string, 356 pair(pair(string, list(string)), list(string)))), list(string)))))( 357 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, 358 { case Document.Node.Perspective(a, b, c) => 359 (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), 360 list(pair(id, pair(string, list(string))))(c.dest)) })) 361 edits.map({ case (name, edit) => 362 Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) }) 363 } 364 protocol_command_args("Document.update", 365 Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml) 366 } 367 368 def remove_versions(versions: List[Document.Version]) 369 { 370 val versions_yxml = 371 { import XML.Encode._ 372 Symbol.encode_yxml(list(long)(versions.map(_.id))) } 373 protocol_command("Document.remove_versions", versions_yxml) 374 } 375 376 377 /* dialog via document content */ 378 379 def dialog_result(serial: Long, result: String): Unit = 380 protocol_command("Document.dialog_result", Value.Long(serial), result) 381} 382