src/Pure/PIDE/isar_document.scala
changeset 43723 8a63c95b1d5b
parent 43722 9b5dadb0c28d
child 43724 4e58485fa320
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 00:21:19 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 13:00:22 2011 +0200
     1.3 @@ -144,14 +144,14 @@
     1.4    {
     1.5      val arg1 =
     1.6        XML_Data.make_list(
     1.7 -        XML_Data.make_pair(XML_Data.make_string)(
     1.8 +        XML_Data.make_pair(XML_Data.make_string,
     1.9            XML_Data.make_option(XML_Data.make_list(
    1.10                XML_Data.make_pair(
    1.11 -                XML_Data.make_option(XML_Data.make_long))(
    1.12 +                XML_Data.make_option(XML_Data.make_long),
    1.13                  XML_Data.make_option(XML_Data.make_long))))))(edits)
    1.14  
    1.15      val arg2 =
    1.16 -      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
    1.17 +      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
    1.18  
    1.19      input("Isar_Document.edit_version",
    1.20        Document.ID(old_id), Document.ID(new_id),