equal
deleted
inserted
replaced
49 /* document versions */ |
49 /* document versions */ |
50 |
50 |
51 def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, |
51 def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, |
52 edits: List[Document.Edit[Document.Command_ID]]) |
52 edits: List[Document.Edit[Document.Command_ID]]) |
53 { |
53 { |
54 def make_id1(id1: Option[Document.Command_ID]): XML.Body = |
|
55 XML_Data.make_long(id1 getOrElse Document.NO_ID) |
|
56 |
|
57 val arg = |
54 val arg = |
58 XML_Data.make_list( |
55 XML_Data.make_list( |
59 XML_Data.make_pair(XML_Data.make_string)( |
56 XML_Data.make_pair(XML_Data.make_string)( |
60 XML_Data.make_option(XML_Data.make_list( |
57 XML_Data.make_option(XML_Data.make_list( |
61 XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits) |
58 XML_Data.make_pair( |
|
59 XML_Data.make_option(XML_Data.make_long))( |
|
60 XML_Data.make_option(XML_Data.make_long))))))(edits) |
62 |
61 |
63 input("Isar_Document.edit_version", |
62 input("Isar_Document.edit_version", |
64 Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) |
63 Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) |
65 } |
64 } |
66 } |
65 } |