src/Pure/PIDE/protocol.scala
author wenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21)
changeset 65532 febfd9f78bd4
parent 65471 05e5bffcf1d8
child 66379 6392766f3c25
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
     1 /*  Title:      Pure/PIDE/protocol.scala
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive proof documents.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Protocol
    11 {
    12   /* document editing */
    13 
    14   object Assign_Update
    15   {
    16     def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
    17       try {
    18         import XML.Decode._
    19         Some(pair(long, list(pair(long, list(long))))(Symbol.decode_yxml(text)))
    20       }
    21       catch {
    22         case ERROR(_) => None
    23         case _: XML.Error => None
    24       }
    25   }
    26 
    27   object Removed
    28   {
    29     def unapply(text: String): Option[List[Document_ID.Version]] =
    30       try {
    31         import XML.Decode._
    32         Some(list(long)(Symbol.decode_yxml(text)))
    33       }
    34       catch {
    35         case ERROR(_) => None
    36         case _: XML.Error => None
    37       }
    38   }
    39 
    40 
    41   /* command status */
    42 
    43   object Status
    44   {
    45     def make(markup_iterator: Iterator[Markup]): Status =
    46     {
    47       var touched = false
    48       var accepted = false
    49       var warned = false
    50       var failed = false
    51       var forks = 0
    52       var runs = 0
    53       for (markup <- markup_iterator) {
    54         markup.name match {
    55           case Markup.ACCEPTED => accepted = true
    56           case Markup.FORKED => touched = true; forks += 1
    57           case Markup.JOINED => forks -= 1
    58           case Markup.RUNNING => touched = true; runs += 1
    59           case Markup.FINISHED => runs -= 1
    60           case Markup.WARNING | Markup.LEGACY => warned = true
    61           case Markup.FAILED | Markup.ERROR => failed = true
    62           case _ =>
    63         }
    64       }
    65       Status(touched, accepted, warned, failed, forks, runs)
    66     }
    67 
    68     val empty = make(Iterator.empty)
    69 
    70     def merge(status_iterator: Iterator[Status]): Status =
    71       if (status_iterator.hasNext) {
    72         val status0 = status_iterator.next
    73         (status0 /: status_iterator)(_ + _)
    74       }
    75       else empty
    76   }
    77 
    78   sealed case class Status(
    79     private val touched: Boolean,
    80     private val accepted: Boolean,
    81     private val warned: Boolean,
    82     private val failed: Boolean,
    83     forks: Int,
    84     runs: Int)
    85   {
    86     def + (that: Status): Status =
    87       Status(
    88         touched || that.touched,
    89         accepted || that.accepted,
    90         warned || that.warned,
    91         failed || that.failed,
    92         forks + that.forks,
    93         runs + that.runs)
    94 
    95     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
    96     def is_running: Boolean = runs != 0
    97     def is_warned: Boolean = warned
    98     def is_failed: Boolean = failed
    99     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
   100   }
   101 
   102   val proper_status_elements =
   103     Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
   104       Markup.FINISHED, Markup.FAILED)
   105 
   106   val liberal_status_elements =
   107     proper_status_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
   108 
   109 
   110   /* command timing */
   111 
   112   object Command_Timing
   113   {
   114     def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
   115       props match {
   116         case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
   117           (args, args) match {
   118             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
   119             case _ => None
   120           }
   121         case _ => None
   122       }
   123   }
   124 
   125 
   126   /* node status */
   127 
   128   sealed case class Node_Status(
   129     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int)
   130   {
   131     def total: Int = unprocessed + running + warned + failed + finished
   132   }
   133 
   134   def node_status(
   135     state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
   136   {
   137     var unprocessed = 0
   138     var running = 0
   139     var warned = 0
   140     var failed = 0
   141     var finished = 0
   142     for (command <- node.commands.iterator) {
   143       val states = state.command_states(version, command)
   144       val status = Status.merge(states.iterator.map(_.protocol_status))
   145 
   146       if (status.is_running) running += 1
   147       else if (status.is_failed) failed += 1
   148       else if (status.is_warned) warned += 1
   149       else if (status.is_finished) finished += 1
   150       else unprocessed += 1
   151     }
   152     Node_Status(unprocessed, running, warned, failed, finished)
   153   }
   154 
   155 
   156   /* node timing */
   157 
   158   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   159 
   160   val empty_node_timing = Node_Timing(0.0, Map.empty)
   161 
   162   def node_timing(
   163     state: Document.State,
   164     version: Document.Version,
   165     node: Document.Node,
   166     threshold: Double): Node_Timing =
   167   {
   168     var total = 0.0
   169     var commands = Map.empty[Command, Double]
   170     for {
   171       command <- node.commands.iterator
   172       st <- state.command_states(version, command)
   173     } {
   174       val command_timing =
   175         (0.0 /: st.status)({
   176           case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   177           case (timing, _) => timing
   178         })
   179       total += command_timing
   180       if (command_timing >= threshold) commands += (command -> command_timing)
   181     }
   182     Node_Timing(total, commands)
   183   }
   184 
   185 
   186   /* result messages */
   187 
   188   def is_result(msg: XML.Tree): Boolean =
   189     msg match {
   190       case XML.Elem(Markup(Markup.RESULT, _), _) => true
   191       case _ => false
   192     }
   193 
   194   def is_tracing(msg: XML.Tree): Boolean =
   195     msg match {
   196       case XML.Elem(Markup(Markup.TRACING, _), _) => true
   197       case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
   198       case _ => false
   199     }
   200 
   201   def is_state(msg: XML.Tree): Boolean =
   202     msg match {
   203       case XML.Elem(Markup(Markup.STATE, _), _) => true
   204       case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
   205       case _ => false
   206     }
   207 
   208   def is_information(msg: XML.Tree): Boolean =
   209     msg match {
   210       case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
   211       case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
   212       case _ => false
   213     }
   214 
   215   def is_warning(msg: XML.Tree): Boolean =
   216     msg match {
   217       case XML.Elem(Markup(Markup.WARNING, _), _) => true
   218       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
   219       case _ => false
   220     }
   221 
   222   def is_legacy(msg: XML.Tree): Boolean =
   223     msg match {
   224       case XML.Elem(Markup(Markup.LEGACY, _), _) => true
   225       case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
   226       case _ => false
   227     }
   228 
   229   def is_error(msg: XML.Tree): Boolean =
   230     msg match {
   231       case XML.Elem(Markup(Markup.ERROR, _), _) => true
   232       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
   233       case _ => false
   234     }
   235 
   236   def is_inlined(msg: XML.Tree): Boolean =
   237     !(is_result(msg) || is_tracing(msg) || is_state(msg))
   238 
   239 
   240   /* breakpoints */
   241 
   242   object ML_Breakpoint
   243   {
   244     def unapply(tree: XML.Tree): Option[Long] =
   245     tree match {
   246       case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
   247       case _ => None
   248     }
   249   }
   250 
   251 
   252   /* dialogs */
   253 
   254   object Dialog_Args
   255   {
   256     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
   257       (props, props, props) match {
   258         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
   259           Some((id, serial, result))
   260         case _ => None
   261       }
   262   }
   263 
   264   object Dialog
   265   {
   266     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
   267       tree match {
   268         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
   269           Some((id, serial, result))
   270         case _ => None
   271       }
   272   }
   273 
   274   object Dialog_Result
   275   {
   276     def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
   277     {
   278       val props = Position.Id(id) ::: Markup.Serial(serial)
   279       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
   280     }
   281 
   282     def unapply(tree: XML.Tree): Option[String] =
   283       tree match {
   284         case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
   285         case _ => None
   286       }
   287   }
   288 }
   289 
   290 
   291 trait Protocol
   292 {
   293   /* protocol commands */
   294 
   295   def protocol_command_bytes(name: String, args: Bytes*): Unit
   296   def protocol_command(name: String, args: String*): Unit
   297 
   298 
   299   /* options */
   300 
   301   def options(opts: Options): Unit =
   302     protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
   303 
   304 
   305   /* session base */
   306 
   307   private def encode_table(table: List[(String, String)]): String =
   308   {
   309     import XML.Encode._
   310     Symbol.encode_yxml(list(pair(string, string))(table))
   311   }
   312 
   313   def session_base(resources: Resources): Unit =
   314     protocol_command("Prover.session_base",
   315       encode_table(resources.session_base.global_theories.toList),
   316       encode_table(resources.session_base.loaded_theories.toList),
   317       encode_table(resources.session_base.dest_known_theories))
   318 
   319 
   320   /* interned items */
   321 
   322   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
   323     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
   324 
   325   def define_command(command: Command)
   326   {
   327     val blobs_yxml =
   328     {
   329       import XML.Encode._
   330       val encode_blob: T[Command.Blob] =
   331         variant(List(
   332           { case Exn.Res((a, b)) =>
   333               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
   334           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
   335 
   336       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
   337     }
   338 
   339     val toks = command.span.content
   340     val toks_yxml =
   341     {
   342       import XML.Encode._
   343       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
   344       Symbol.encode_yxml(list(encode_tok)(toks))
   345     }
   346 
   347     protocol_command("Document.define_command",
   348       (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
   349         toks.map(tok => Symbol.encode(tok.source))): _*)
   350   }
   351 
   352 
   353   /* execution */
   354 
   355   def discontinue_execution(): Unit =
   356     protocol_command("Document.discontinue_execution")
   357 
   358   def cancel_exec(id: Document_ID.Exec): Unit =
   359     protocol_command("Document.cancel_exec", Document_ID(id))
   360 
   361 
   362   /* document versions */
   363 
   364   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
   365     edits: List[Document.Edit_Command])
   366   {
   367     val edits_yxml =
   368     {
   369       import XML.Encode._
   370       def id: T[Command] = (cmd => long(cmd.id))
   371       def encode_edit(name: Document.Node.Name)
   372           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
   373         variant(List(
   374           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   375           { case Document.Node.Deps(header) =>
   376               val master_dir = File.standard_url(name.master_dir)
   377               val imports = header.imports.map({ case (a, _) => a.node })
   378               val keywords =
   379                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
   380               (Nil,
   381                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
   382                     pair(pair(string, list(string)), list(string)))), list(string)))))(
   383                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
   384           { case Document.Node.Perspective(a, b, c) =>
   385               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
   386                 list(pair(id, pair(string, list(string))))(c.dest)) }))
   387       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
   388       {
   389         val (name, edit) = node_edit
   390         pair(string, encode_edit(name))(name.node, edit)
   391       })
   392       Symbol.encode_yxml(encode_edits(edits)) }
   393     protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   394   }
   395 
   396   def remove_versions(versions: List[Document.Version])
   397   {
   398     val versions_yxml =
   399     { import XML.Encode._
   400       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
   401     protocol_command("Document.remove_versions", versions_yxml)
   402   }
   403 
   404 
   405   /* dialog via document content */
   406 
   407   def dialog_result(serial: Long, result: String): Unit =
   408     protocol_command("Document.dialog_result", Value.Long(serial), result)
   409 }