src/Pure/PIDE/protocol.scala
author wenzelm
Sun May 19 18:10:45 2019 +0200 (4 months ago)
changeset 70284 3e17c3a5fd39
parent 69849 09f200c658ed
child 70638 f164cec7ac22
permissions -rw-r--r--
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
     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)
    17       : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
    18     {
    19       try {
    20         import XML.Decode._
    21         def decode_upd(body: XML.Body): (Long, List[Long]) =
    22           space_explode(',', string(body)).map(Value.Long.parse) match {
    23             case a :: bs => (a, bs)
    24             case _ => throw new XML.XML_Body(body)
    25           }
    26         Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
    27       }
    28       catch {
    29         case ERROR(_) => None
    30         case _: XML.Error => None
    31       }
    32     }
    33   }
    34 
    35   object Removed
    36   {
    37     def unapply(text: String): Option[List[Document_ID.Version]] =
    38       try {
    39         import XML.Decode._
    40         Some(list(long)(Symbol.decode_yxml(text)))
    41       }
    42       catch {
    43         case ERROR(_) => None
    44         case _: XML.Error => None
    45       }
    46   }
    47 
    48 
    49   /* command timing */
    50 
    51   object Command_Timing
    52   {
    53     def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
    54       props match {
    55         case Markup.COMMAND_TIMING :: args =>
    56           (args, args) match {
    57             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
    58             case _ => None
    59           }
    60         case _ => None
    61       }
    62   }
    63 
    64 
    65   /* theory timing */
    66 
    67   object Theory_Timing
    68   {
    69     def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
    70       props match {
    71         case Markup.THEORY_TIMING :: args =>
    72           (args, args) match {
    73             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
    74             case _ => None
    75           }
    76         case _ => None
    77       }
    78   }
    79 
    80 
    81   /* result messages */
    82 
    83   def is_result(msg: XML.Tree): Boolean =
    84     msg match {
    85       case XML.Elem(Markup(Markup.RESULT, _), _) => true
    86       case _ => false
    87     }
    88 
    89   def is_tracing(msg: XML.Tree): Boolean =
    90     msg match {
    91       case XML.Elem(Markup(Markup.TRACING, _), _) => true
    92       case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true
    93       case _ => false
    94     }
    95 
    96   def is_state(msg: XML.Tree): Boolean =
    97     msg match {
    98       case XML.Elem(Markup(Markup.STATE, _), _) => true
    99       case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true
   100       case _ => false
   101     }
   102 
   103   def is_information(msg: XML.Tree): Boolean =
   104     msg match {
   105       case XML.Elem(Markup(Markup.INFORMATION, _), _) => true
   106       case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true
   107       case _ => false
   108     }
   109 
   110   def is_writeln(msg: XML.Tree): Boolean =
   111     msg match {
   112       case XML.Elem(Markup(Markup.WRITELN, _), _) => true
   113       case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
   114       case _ => false
   115     }
   116 
   117   def is_warning(msg: XML.Tree): Boolean =
   118     msg match {
   119       case XML.Elem(Markup(Markup.WARNING, _), _) => true
   120       case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true
   121       case _ => false
   122     }
   123 
   124   def is_legacy(msg: XML.Tree): Boolean =
   125     msg match {
   126       case XML.Elem(Markup(Markup.LEGACY, _), _) => true
   127       case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true
   128       case _ => false
   129     }
   130 
   131   def is_error(msg: XML.Tree): Boolean =
   132     msg match {
   133       case XML.Elem(Markup(Markup.ERROR, _), _) => true
   134       case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true
   135       case _ => false
   136     }
   137 
   138   def is_inlined(msg: XML.Tree): Boolean =
   139     !(is_result(msg) || is_tracing(msg) || is_state(msg))
   140 
   141   def is_exported(msg: XML.Tree): Boolean =
   142     is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
   143 
   144 
   145   /* breakpoints */
   146 
   147   object ML_Breakpoint
   148   {
   149     def unapply(tree: XML.Tree): Option[Long] =
   150     tree match {
   151       case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
   152       case _ => None
   153     }
   154   }
   155 
   156 
   157   /* dialogs */
   158 
   159   object Dialog_Args
   160   {
   161     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
   162       (props, props, props) match {
   163         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
   164           Some((id, serial, result))
   165         case _ => None
   166       }
   167   }
   168 
   169   object Dialog
   170   {
   171     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
   172       tree match {
   173         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
   174           Some((id, serial, result))
   175         case _ => None
   176       }
   177   }
   178 
   179   object Dialog_Result
   180   {
   181     def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
   182     {
   183       val props = Position.Id(id) ::: Markup.Serial(serial)
   184       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
   185     }
   186 
   187     def unapply(tree: XML.Tree): Option[String] =
   188       tree match {
   189         case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result)
   190         case _ => None
   191       }
   192   }
   193 }
   194 
   195 
   196 trait Protocol
   197 {
   198   /* protocol commands */
   199 
   200   def protocol_command_bytes(name: String, args: Bytes*): Unit
   201   def protocol_command(name: String, args: String*): Unit
   202 
   203 
   204   /* options */
   205 
   206   def options(opts: Options): Unit =
   207     protocol_command("Prover.options", Symbol.encode_yxml(opts.encode))
   208 
   209 
   210   /* session base */
   211 
   212   private def encode_table(table: List[(String, String)]): String =
   213   {
   214     import XML.Encode._
   215     Symbol.encode_yxml(list(pair(string, string))(table))
   216   }
   217 
   218   private def encode_list(lst: List[String]): String =
   219   {
   220     import XML.Encode._
   221     Symbol.encode_yxml(list(string)(lst))
   222   }
   223 
   224   private def encode_sessions(lst: List[(String, Position.T)]): String =
   225   {
   226     import XML.Encode._
   227     Symbol.encode_yxml(list(pair(string, properties))(lst))
   228   }
   229 
   230   def session_base(resources: Resources)
   231   {
   232     val base = resources.session_base.standard_path
   233     protocol_command("Prover.init_session_base",
   234       encode_sessions(base.known.sessions.toList),
   235       encode_list(base.doc_names),
   236       encode_table(base.global_theories.toList),
   237       encode_list(base.loaded_theories.keys),
   238       encode_table(base.dest_known_theories))
   239   }
   240 
   241 
   242   /* interned items */
   243 
   244   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
   245     protocol_command_bytes("Document.define_blob", Bytes(digest.toString), bytes)
   246 
   247   def define_command(command: Command)
   248   {
   249     val blobs_yxml =
   250     {
   251       import XML.Encode._
   252       val encode_blob: T[Command.Blob] =
   253         variant(List(
   254           { case Exn.Res((a, b)) =>
   255               (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
   256           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
   257 
   258       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
   259     }
   260 
   261     val toks = command.span.content
   262     val toks_yxml =
   263     {
   264       import XML.Encode._
   265       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
   266       Symbol.encode_yxml(list(encode_tok)(toks))
   267     }
   268 
   269     protocol_command("Document.define_command",
   270       (Document_ID(command.id) :: Symbol.encode(command.span.name) :: blobs_yxml :: toks_yxml ::
   271         toks.map(tok => Symbol.encode(tok.source))): _*)
   272   }
   273 
   274 
   275   /* execution */
   276 
   277   def discontinue_execution(): Unit =
   278     protocol_command("Document.discontinue_execution")
   279 
   280   def cancel_exec(id: Document_ID.Exec): Unit =
   281     protocol_command("Document.cancel_exec", Document_ID(id))
   282 
   283 
   284   /* document versions */
   285 
   286   def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
   287     edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name])
   288   {
   289     val consolidate_yxml =
   290     {
   291       import XML.Encode._
   292       Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
   293     }
   294     val edits_yxml =
   295     {
   296       import XML.Encode._
   297       def id: T[Command] = (cmd => long(cmd.id))
   298       def encode_edit(name: Document.Node.Name)
   299           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
   300         variant(List(
   301           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
   302           { case Document.Node.Deps(header) =>
   303               val master_dir = File.standard_url(name.master_dir)
   304               val imports = header.imports.map({ case (a, _) => a.node })
   305               val keywords =
   306                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
   307               (Nil,
   308                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
   309                     pair(pair(string, list(string)), list(string)))), list(string)))))(
   310                 (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
   311           { case Document.Node.Perspective(a, b, c) =>
   312               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
   313                 list(pair(id, pair(string, list(string))))(c.dest)) }))
   314       edits.map({ case (name, edit) =>
   315         Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) })
   316     }
   317     protocol_command("Document.update",
   318       (Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml): _*)
   319   }
   320 
   321   def remove_versions(versions: List[Document.Version])
   322   {
   323     val versions_yxml =
   324     { import XML.Encode._
   325       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
   326     protocol_command("Document.remove_versions", versions_yxml)
   327   }
   328 
   329 
   330   /* dialog via document content */
   331 
   332   def dialog_result(serial: Long, result: String): Unit =
   333     protocol_command("Document.dialog_result", Value.Long(serial), result)
   334 }