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