src/Pure/PIDE/isar_document.scala
changeset 43722 9b5dadb0c28d
parent 40479 cc06f5528bb1
child 43723 8a63c95b1d5b
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Jul 09 21:53:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 00:21:19 2011 +0200
     1.3 @@ -140,9 +140,9 @@
     1.4    /* document versions */
     1.5  
     1.6    def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
     1.7 -      edits: List[Document.Edit_Command_ID])
     1.8 +      edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
     1.9    {
    1.10 -    val arg =
    1.11 +    val arg1 =
    1.12        XML_Data.make_list(
    1.13          XML_Data.make_pair(XML_Data.make_string)(
    1.14            XML_Data.make_option(XML_Data.make_list(
    1.15 @@ -150,7 +150,11 @@
    1.16                  XML_Data.make_option(XML_Data.make_long))(
    1.17                  XML_Data.make_option(XML_Data.make_long))))))(edits)
    1.18  
    1.19 +    val arg2 =
    1.20 +      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
    1.21 +
    1.22      input("Isar_Document.edit_version",
    1.23 -      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    1.24 +      Document.ID(old_id), Document.ID(new_id),
    1.25 +        YXML.string_of_body(arg1), YXML.string_of_body(arg2))
    1.26    }
    1.27  }