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