src/Pure/Isar/isar_document.scala
changeset 38355 8cb265fb12fe
parent 38271 36187e8443dd
child 38363 af7f41a8a0a8
     1.1 --- a/src/Pure/Isar/isar_document.scala	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.scala	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -23,7 +23,10 @@
     1.4      def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
     1.5        msg match {
     1.6          case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
     1.7 -          Some(cmd_id, state_id)
     1.8 +          (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match {
     1.9 +            case (Some(i), Some(j)) => Some((i, j))
    1.10 +            case _ => None
    1.11 +          }
    1.12          case _ => None
    1.13        }
    1.14    }
    1.15 @@ -38,7 +41,7 @@
    1.16    /* commands */
    1.17  
    1.18    def define_command(id: Document.Command_ID, text: String): Unit =
    1.19 -    input("Isar_Document.define_command", id, text)
    1.20 +    input("Isar_Document.define_command", Document.print_id(id), text)
    1.21  
    1.22  
    1.23    /* documents */
    1.24 @@ -47,13 +50,15 @@
    1.25        edits: List[Document.Edit[Document.Command_ID]])
    1.26    {
    1.27      def make_id1(id1: Option[Document.Command_ID]): XML.Body =
    1.28 -      XML_Data.make_string(id1 getOrElse Document.NO_ID)
    1.29 +      XML_Data.make_long(id1 getOrElse Document.NO_ID)
    1.30 +
    1.31      val arg =
    1.32        XML_Data.make_list(
    1.33          XML_Data.make_pair(XML_Data.make_string)(
    1.34            XML_Data.make_option(XML_Data.make_list(
    1.35 -              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits)
    1.36 +              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
    1.37  
    1.38 -    input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg))
    1.39 +    input("Isar_Document.edit_document",
    1.40 +      Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg))
    1.41    }
    1.42  }