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