142 def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, |
142 def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, |
143 edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)]) |
143 edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)]) |
144 { |
144 { |
145 val arg1 = |
145 val arg1 = |
146 XML_Data.make_list( |
146 XML_Data.make_list( |
147 XML_Data.make_pair(XML_Data.make_string)( |
147 XML_Data.make_pair(XML_Data.make_string, |
148 XML_Data.make_option(XML_Data.make_list( |
148 XML_Data.make_option(XML_Data.make_list( |
149 XML_Data.make_pair( |
149 XML_Data.make_pair( |
150 XML_Data.make_option(XML_Data.make_long))( |
150 XML_Data.make_option(XML_Data.make_long), |
151 XML_Data.make_option(XML_Data.make_long))))))(edits) |
151 XML_Data.make_option(XML_Data.make_long))))))(edits) |
152 |
152 |
153 val arg2 = |
153 val arg2 = |
154 XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers) |
154 XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string, Thy_Header.make_xml_data))(headers) |
155 |
155 |
156 input("Isar_Document.edit_version", |
156 input("Isar_Document.edit_version", |
157 Document.ID(old_id), Document.ID(new_id), |
157 Document.ID(old_id), Document.ID(new_id), |
158 YXML.string_of_body(arg1), YXML.string_of_body(arg2)) |
158 YXML.string_of_body(arg1), YXML.string_of_body(arg2)) |
159 } |
159 } |