src/Pure/PIDE/isar_document.ML
changeset 43724 4e58485fa320
parent 43722 9b5dadb0c28d
child 43731 70072780e095
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 13:00:22 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 13:51:21 2011 +0200
     1.3 @@ -17,21 +17,12 @@
     1.4        let
     1.5          val old_id = Document.parse_id old_id_string;
     1.6          val new_id = Document.parse_id new_id_string;
     1.7 -        val edits =
     1.8 -          XML_Data.dest_list
     1.9 -            (XML_Data.dest_pair
    1.10 -              XML_Data.dest_string
    1.11 -              (XML_Data.dest_option
    1.12 -                (XML_Data.dest_list
    1.13 -                  (XML_Data.dest_pair
    1.14 -                    (XML_Data.dest_option XML_Data.dest_int)
    1.15 -                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    1.16 -        val headers =
    1.17 -          XML_Data.dest_list
    1.18 -            (XML_Data.dest_pair XML_Data.dest_string
    1.19 -              (XML_Data.dest_triple XML_Data.dest_string
    1.20 -                (XML_Data.dest_list XML_Data.dest_string)
    1.21 -                (XML_Data.dest_list XML_Data.dest_string))) (YXML.parse_body headers_yxml);
    1.22 +        val edits = YXML.parse_body edits_yxml |>
    1.23 +          let open XML_Data.Dest
    1.24 +          in list (pair string (option (list (pair (option int) (option int))))) end;
    1.25 +        val headers = YXML.parse_body headers_yxml |>
    1.26 +          let open XML_Data.Dest
    1.27 +          in list (pair string (triple string (list string) (list string))) end;
    1.28  
    1.29        val await_cancellation = Document.cancel_execution state;
    1.30        val (updates, state') = Document.edit old_id new_id edits headers state;