--- a/src/Pure/PIDE/isar_document.scala Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Sun Jul 10 13:51:21 2011 +0200
@@ -143,15 +143,12 @@
edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
{
val arg1 =
- XML_Data.make_list(
- XML_Data.make_pair(XML_Data.make_string,
- XML_Data.make_option(XML_Data.make_list(
- XML_Data.make_pair(
- XML_Data.make_option(XML_Data.make_long),
- XML_Data.make_option(XML_Data.make_long))))))(edits)
+ { import XML_Data.Make._
+ list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
val arg2 =
- XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers)
+ { import XML_Data.Make._
+ list(pair(string, Thy_Header.make_xml_data))(headers) }
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id),