147 def encode: T[List[Document.Edit_Command_ID]] = |
147 def encode: T[List[Document.Edit_Command_ID]] = |
148 list(pair(string, |
148 list(pair(string, |
149 variant(List( |
149 variant(List( |
150 { case Document.Node.Remove() => (Nil, Nil) }, |
150 { case Document.Node.Remove() => (Nil, Nil) }, |
151 { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }, |
151 { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }, |
152 { case Document.Node.Update_Header( |
152 { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => |
153 Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) => |
|
154 (Nil, triple(string, list(string), list(string))(a, b, c)) }, |
153 (Nil, triple(string, list(string), list(string))(a, b, c)) }, |
155 { case Document.Node.Update_Header( |
154 { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) })))) |
156 Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) })))) |
|
157 YXML.string_of_body(encode(edits)) } |
155 YXML.string_of_body(encode(edits)) } |
158 |
156 |
159 input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml) |
157 input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml) |
160 } |
158 } |
161 |
159 |