src/Pure/PIDE/protocol.scala
author wenzelm
Tue Jan 23 19:25:39 2018 +0100 (22 months ago ago)
changeset 67493 c4e9e0c50487
parent 67472 bddfa23a4ea9
child 67883 171e7735ce25
permissions -rw-r--r--
treat sessions as entities with defining position;
tuned signature;
     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.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   /* theory timing */
   127 
   128   object Theory_Timing
   129   {
   130     def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
   131       props match {
   132         case Markup.THEORY_TIMING :: args =>
   133           (args, args) match {
   134             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
   135             case _ => None
   136           }
   137         case _ => None
   138       }
   139   }
   140 
   141 
   142   /* node status */
   143 
   144   sealed case class Node_Status(
   145     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
   146   {
   147     def total: Int = unprocessed + running + warned + failed + finished
   148     def ok: Boolean = failed == 0
   149   }
   150 
   151   def node_status(
   152     state: Document.State,
   153     version: Document.Version,
   154     name: Document.Node.Name,
   155     node: Document.Node): Node_Status =
   156   {
   157     var unprocessed = 0
   158     var running = 0
   159     var warned = 0
   160     var failed = 0
   161     var finished = 0
   162     for (command <- node.commands.iterator) {
   163       val states = state.command_states(version, command)
   164       val status = Status.merge(states.iterator.map(_.protocol_status))
   165 
   166       if (status.is_running) running += 1
   167       else if (status.is_failed) failed += 1
   168       else if (status.is_warned) warned += 1
   169       else if (status.is_finished) finished += 1
   170       else unprocessed += 1
   171     }
   172     val consolidated = state.node_consolidated(version, name)
   173 
   174     Node_Status(unprocessed, running, warned, failed, finished, consolidated)
   175   }
   176 
   177 
   178   /* node timing */
   179 
   180   sealed case class Node_Timing(total: Double, commands: Map[Command, Double])
   181 
   182   val empty_node_timing = Node_Timing(0.0, Map.empty)
   183 
   184   def node_timing(
   185     state: Document.State,
   186     version: Document.Version,
   187     node: Document.Node,
   188     threshold: Double): Node_Timing =
   189   {
   190     var total = 0.0
   191     var commands = Map.empty[Command, Double]
   192     for {
   193       command <- node.commands.iterator
   194       st <- state.command_states(version, command)
   195     } {
   196       val command_timing =
   197         (0.0 /: st.status)({
   198           case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
   199           case (timing, _) => timing
   200         })
   201       total += command_timing
   202       if (command_timing >= threshold) commands += (command -> command_timing)
   203     }
   204     Node_Timing(total, commands)
   205   }
   206 
   207 
   208   /* result messages */
   209 
   210   def is_result(msg: XML.Tree): Boolean =
   211     msg match {
   212       case XML.Elem(Markup(Markup.RESULT, _), _) => true
   213       case _ => false
   214     }
   215 
   216   def is_tracing(msg: XML.Tree): Boolean =
   217     msg match {
   218       case XML.Elem(Markup(Markup.TRACING, _), _) => true
   219       case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
   220       case _ => false
   221     }
   222 
   223   def is_state(msg: XML.Tree): Boolean =
   224     msg match {
   225       case XML.Elem(Markup(Markup.STATE, _), _) => true
   226       case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
   227       case _ => false
   228     }
   229 
   230   def is_information(msg: XML.Tree): Boolean =
   231     msg match {
   232       case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
   233       case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
   234       case _ => false
   235     }
   236 
   237   def is_warning(msg: XML.Tree): Boolean =
   238     msg match {
   239       case XML.Elem(Markup(Markup.WARNING, _), _) => true
   240       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
   241       case _ => false
   242     }
   243 
   244   def is_legacy(msg: XML.Tree): Boolean =
   245     msg match {
   246       case XML.Elem(Markup(Markup.LEGACY, _), _) => true
   247       case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
   248       case _ => false
   249     }
   250 
   251   def is_error(msg: XML.Tree): Boolean =
   252     msg match {
   253       case XML.Elem(Markup(Markup.ERROR, _), _) => true
   254       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
   255       case _ => false
   256     }
   257 
   258   def is_inlined(msg: XML.Tree): Boolean =
   259     !(is_result(msg) || is_tracing(msg) || is_state(msg))
   260 
   261 
   262   /* breakpoints */
   263 
   264   object ML_Breakpoint
   265   {
   266     def unapply(tree: XML.Tree): Option[Long] =
   267     tree match {
   268       case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
   269       case _ => None
   270     }
   271   }
   272 
   273 
   274   /* dialogs */
   275 
   276   object Dialog_Args
   277   {
   278     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
   279       (props, props, props) match {
   280         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
   281           Some((id, serial, result))
   282         case _ => None
   283       }
   284   }
   285 
   286   object Dialog
   287   {
   288     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
   289       tree match {
   290         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
   291           Some((id, serial, result))
   292         case _ => None
   293       }
   294   }
   295 
   296   object Dialog_Result
   297   {
   298     def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
   299     {
   300       val props = Position.Id(id) ::: Markup.Serial(serial)
   301       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
   302     }
   303 
   304     def unapply(tree: XML.Tree): Option[String] =
   305       tree match {
   306         case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
   307         case _ => None
   308       }
   309   }
   310 }
   311 
   312 
   313 trait Protocol
   314 {
   315   /* protocol commands */
   316 
   317   def protocol_command_bytes(name: String, args: Bytes*): Unit
   318   def protocol_command(name: String, args: String*): Unit
   319 
   320 
   321   /* options */
   322 
   323   def options(opts: Options): Unit =
   324     protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
   325 
   326 
   327   /* session base */
   328 
   329   private def encode_table(table: List[(String, String)]): String =
   330   {
   331     import XML.Encode._
   332     Symbol.encode_yxml(list(pair(string, string))(table))
   333   }
   334 
   335   private def encode_list(lst: List[String]): String =
   336   {
   337     import XML.Encode._
   338     Symbol.encode_yxml(list(string)(lst))
   339   }
   340 
   341   private def encode_sessions(lst: List[(String, Position.T)]): String =
   342   {
   343     import XML.Encode._
   344     Symbol.encode_yxml(list(pair(string, properties))(lst))
   345   }
   346 
   347   def session_base(resources: Resources)
   348   {
   349     val base = resources.session_base.standard_path
   350     protocol_command("Prover.init_session_base",
   351       encode_sessions(base.known.sessions.toList),
   352       encode_list(base.doc_names),
   353       encode_table(base.global_theories.toList),
   354       encode_list(base.loaded_theories.keys),
   355       encode_table(base.dest_known_theories))
   356   }
   357 
   358 
   359   /* interned items */
   360 
   361   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
   362     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
   363 
   364   def define_command(command: Command)
   365   {
   366     val blobs_yxml =
   367     {
   368       import XML.Encode._
   369       val encode_blob: T[Command.Blob] =
   370         variant(List(
   371           { case Exn.Res((a, b)) =>
   372               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
   373           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
   374 
   375       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
   376     }
   377 
   378     val toks = command.span.content
   379     val toks_yxml =
   380     {
   381       import XML.Encode._
   382       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
   383       Symbol.encode_yxml(list(encode_tok)(toks))
   384     }
   385 
   386     protocol_command("Document.define_command",
   387       (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
   388         toks.map(tok => Symbol.encode(tok.source))): _*)
   389   }
   390 
   391 
   392   /* execution */
   393 
   394   def consolidate_execution(): Unit =
   395     protocol_command("Document.consolidate_execution")
   396 
   397   def discontinue_execution(): Unit =
   398     protocol_command("Document.discontinue_execution")
   399 
   400   def cancel_exec(id: Document_ID.Exec): Unit =
   401     protocol_command("Document.cancel_exec", Document_ID(id))
   402 
   403 
   404   /* document versions */
   405 
   406   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
   407     edits: List[Document.Edit_Command])
   408   {
   409     val edits_yxml =
   410     {
   411       import XML.Encode._
   412       def id: T[Command] = (cmd => long(cmd.id))
   413       def encode_edit(name: Document.Node.Name)
   414           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
   415         variant(List(
   416           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   417           { case Document.Node.Deps(header) =>
   418               val master_dir = File.standard_url(name.master_dir)
   419               val imports = header.imports.map({ case (a, _) => a.node })
   420               val keywords =
   421                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
   422               (Nil,
   423                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
   424                     pair(pair(string, list(string)), list(string)))), list(string)))))(
   425                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
   426           { case Document.Node.Perspective(a, b, c) =>
   427               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
   428                 list(pair(id, pair(string, list(string))))(c.dest)) }))
   429       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
   430       {
   431         val (name, edit) = node_edit
   432         pair(string, encode_edit(name))(name.node, edit)
   433       })
   434       Symbol.encode_yxml(encode_edits(edits)) }
   435     protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   436   }
   437 
   438   def remove_versions(versions: List[Document.Version])
   439   {
   440     val versions_yxml =
   441     { import XML.Encode._
   442       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
   443     protocol_command("Document.remove_versions", versions_yxml)
   444   }
   445 
   446 
   447   /* dialog via document content */
   448 
   449   def dialog_result(serial: Long, result: String): Unit =
   450     protocol_command("Document.dialog_result", Value.Long(serial), result)
   451 }