equal
deleted
inserted
replaced
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 { import XML.Encode._ |
146 { import XML.Encode._ |
147 list(pair(string, option(list(pair(option(long), option(long))))))(edits) } |
147 def encode: T[List[Document.Edit_Command_ID]] = |
|
148 list(pair(string, |
|
149 variant(List( |
|
150 { case Document.Node.Remove() => (Nil, Nil) }, |
|
151 { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) })))) |
|
152 encode(edits) } |
148 |
153 |
149 val arg2 = |
154 val arg2 = |
150 { import XML.Encode._ |
155 { import XML.Encode._ |
151 list(pair(string, Thy_Header.xml_encode))(headers) } |
156 list(pair(string, Thy_Header.xml_encode))(headers) } |
152 |
157 |