src/Pure/PIDE/protocol.scala
author wenzelm
Sat Dec 16 21:53:07 2017 +0100 (21 months ago)
changeset 67219 81e9804b2014
parent 66873 9953ae603a23
child 67471 bddfa23a4ea9
permissions -rw-r--r--
added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
     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   def session_base(resources: Resources)
   342   {
   343     val base = resources.session_base.standard_path
   344     protocol_command("Prover.init_session_base",
   345       encode_list(base.known.sessions.toList),
   346       encode_table(base.global_theories.toList),
   347       encode_list(base.loaded_theories.keys),
   348       encode_table(base.dest_known_theories))
   349   }
   350 
   351 
   352   /* interned items */
   353 
   354   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
   355     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
   356 
   357   def define_command(command: Command)
   358   {
   359     val blobs_yxml =
   360     {
   361       import XML.Encode._
   362       val encode_blob: T[Command.Blob] =
   363         variant(List(
   364           { case Exn.Res((a, b)) =>
   365               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
   366           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
   367 
   368       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
   369     }
   370 
   371     val toks = command.span.content
   372     val toks_yxml =
   373     {
   374       import XML.Encode._
   375       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
   376       Symbol.encode_yxml(list(encode_tok)(toks))
   377     }
   378 
   379     protocol_command("Document.define_command",
   380       (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
   381         toks.map(tok => Symbol.encode(tok.source))): _*)
   382   }
   383 
   384 
   385   /* execution */
   386 
   387   def consolidate_execution(): Unit =
   388     protocol_command("Document.consolidate_execution")
   389 
   390   def discontinue_execution(): Unit =
   391     protocol_command("Document.discontinue_execution")
   392 
   393   def cancel_exec(id: Document_ID.Exec): Unit =
   394     protocol_command("Document.cancel_exec", Document_ID(id))
   395 
   396 
   397   /* document versions */
   398 
   399   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
   400     edits: List[Document.Edit_Command])
   401   {
   402     val edits_yxml =
   403     {
   404       import XML.Encode._
   405       def id: T[Command] = (cmd => long(cmd.id))
   406       def encode_edit(name: Document.Node.Name)
   407           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
   408         variant(List(
   409           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   410           { case Document.Node.Deps(header) =>
   411               val master_dir = File.standard_url(name.master_dir)
   412               val imports = header.imports.map({ case (a, _) => a.node })
   413               val keywords =
   414                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
   415               (Nil,
   416                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
   417                     pair(pair(string, list(string)), list(string)))), list(string)))))(
   418                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
   419           { case Document.Node.Perspective(a, b, c) =>
   420               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
   421                 list(pair(id, pair(string, list(string))))(c.dest)) }))
   422       def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
   423       {
   424         val (name, edit) = node_edit
   425         pair(string, encode_edit(name))(name.node, edit)
   426       })
   427       Symbol.encode_yxml(encode_edits(edits)) }
   428     protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
   429   }
   430 
   431   def remove_versions(versions: List[Document.Version])
   432   {
   433     val versions_yxml =
   434     { import XML.Encode._
   435       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
   436     protocol_command("Document.remove_versions", versions_yxml)
   437   }
   438 
   439 
   440   /* dialog via document content */
   441 
   442   def dialog_result(serial: Long, result: String): Unit =
   443     protocol_command("Document.dialog_result", Value.Long(serial), result)
   444 }