src/Pure/PIDE/isar_document.scala
changeset 38483 3d16bebee1d3
parent 38448 62d16c415019
child 38567 b670faa807c9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 19 12:51:48 2010 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +/*  Title:      Pure/PIDE/isar_document.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Protocol commands for interactive Isar documents.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Isar_Document
    1.14 +{
    1.15 +  /* protocol messages */
    1.16 +
    1.17 +  object Assign {
    1.18 +    def unapply(msg: XML.Tree)
    1.19 +        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
    1.20 +      msg match {
    1.21 +        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
    1.22 +          val id_edits = edits.map(Edit.unapply)
    1.23 +          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
    1.24 +          else None
    1.25 +        case _ => None
    1.26 +      }
    1.27 +  }
    1.28 +
    1.29 +  object Edit {
    1.30 +    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    1.31 +      msg match {
    1.32 +        case XML.Elem(
    1.33 +          Markup(Markup.EDIT,
    1.34 +            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
    1.35 +        case _ => None
    1.36 +      }
    1.37 +  }
    1.38 +}
    1.39 +
    1.40 +
    1.41 +trait Isar_Document extends Isabelle_Process
    1.42 +{
    1.43 +  import Isar_Document._
    1.44 +
    1.45 +
    1.46 +  /* commands */
    1.47 +
    1.48 +  def define_command(id: Document.Command_ID, text: String): Unit =
    1.49 +    input("Isar_Document.define_command", Document.ID(id), text)
    1.50 +
    1.51 +
    1.52 +  /* document versions */
    1.53 +
    1.54 +  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    1.55 +      edits: List[Document.Edit[Document.Command_ID]])
    1.56 +  {
    1.57 +    val arg =
    1.58 +      XML_Data.make_list(
    1.59 +        XML_Data.make_pair(XML_Data.make_string)(
    1.60 +          XML_Data.make_option(XML_Data.make_list(
    1.61 +              XML_Data.make_pair(
    1.62 +                XML_Data.make_option(XML_Data.make_long))(
    1.63 +                XML_Data.make_option(XML_Data.make_long))))))(edits)
    1.64 +
    1.65 +    input("Isar_Document.edit_version",
    1.66 +      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    1.67 +  }
    1.68 +}