src/Pure/System/isar_document.scala
author wenzelm
Sun Aug 15 14:18:52 2010 +0200 (2010-08-15)
changeset 38417 b8922ae21111
parent 38414 49f1f657adc2
child 38418 9a7af64d71bb
permissions -rw-r--r--
renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
tuned;
     1 /*  Title:      Pure/System/isar_document.scala
     2     Author:     Makarius
     3 
     4 Interactive Isar documents.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Isar_Document
    11 {
    12   /* protocol messages */
    13 
    14   object Assign {
    15     def unapply(msg: XML.Tree)
    16         : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
    17       msg match {
    18         case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
    19           val id_edits = edits.map(Edit.unapply)
    20           if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
    21           else None
    22         case _ => None
    23       }
    24   }
    25 
    26   object Edit {
    27     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    28       msg match {
    29         case XML.Elem(
    30           Markup(Markup.EDIT,
    31             List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
    32         case _ => None
    33       }
    34   }
    35 }
    36 
    37 
    38 trait Isar_Document extends Isabelle_Process
    39 {
    40   import Isar_Document._
    41 
    42 
    43   /* commands */
    44 
    45   def define_command(id: Document.Command_ID, text: String): Unit =
    46     input("Isar_Document.define_command", Document.ID(id), text)
    47 
    48 
    49   /* document versions */
    50 
    51   def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    52       edits: List[Document.Edit[Document.Command_ID]])
    53   {
    54     def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    55       XML_Data.make_long(id1 getOrElse Document.NO_ID)
    56 
    57     val arg =
    58       XML_Data.make_list(
    59         XML_Data.make_pair(XML_Data.make_string)(
    60           XML_Data.make_option(XML_Data.make_list(
    61               XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    62 
    63     input("Isar_Document.edit_version",
    64       Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    65   }
    66 }