--- a/src/Pure/PIDE/isar_document.ML Sun Jul 10 13:00:22 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Sun Jul 10 13:51:21 2011 +0200
@@ -17,21 +17,12 @@
let
val old_id = Document.parse_id old_id_string;
val new_id = Document.parse_id new_id_string;
- val edits =
- XML_Data.dest_list
- (XML_Data.dest_pair
- XML_Data.dest_string
- (XML_Data.dest_option
- (XML_Data.dest_list
- (XML_Data.dest_pair
- (XML_Data.dest_option XML_Data.dest_int)
- (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
- val headers =
- XML_Data.dest_list
- (XML_Data.dest_pair XML_Data.dest_string
- (XML_Data.dest_triple XML_Data.dest_string
- (XML_Data.dest_list XML_Data.dest_string)
- (XML_Data.dest_list XML_Data.dest_string))) (YXML.parse_body headers_yxml);
+ val edits = YXML.parse_body edits_yxml |>
+ let open XML_Data.Dest
+ in list (pair string (option (list (pair (option int) (option int))))) end;
+ val headers = YXML.parse_body headers_yxml |>
+ let open XML_Data.Dest
+ in list (pair string (triple string (list string) (list string))) end;
val await_cancellation = Document.cancel_execution state;
val (updates, state') = Document.edit old_id new_id edits headers state;