src/Pure/PIDE/isar_document.ML
changeset 44156 6aa25b80e1a5
parent 43767 e0219ef7f84c
child 44157 a21d3e1e64fd
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Thu Aug 11 13:24:49 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 11 18:01:28 2011 +0200
     1.3 @@ -18,8 +18,12 @@
     1.4          val old_id = Document.parse_id old_id_string;
     1.5          val new_id = Document.parse_id new_id_string;
     1.6          val edits = YXML.parse_body edits_yxml |>
     1.7 -          let open XML.Decode
     1.8 -          in list (pair string (option (list (pair (option int) (option int))))) end;
     1.9 +          let open XML.Decode in
    1.10 +            list (pair string
    1.11 +              (variant
    1.12 +               [fn ([], []) => Document.Remove,
    1.13 +                fn ([], a) => Document.Edits (list (pair (option int) (option int)) a)]))
    1.14 +          end;
    1.15          val headers = YXML.parse_body headers_yxml |>
    1.16            let open XML.Decode
    1.17            in list (pair string (triple string (list string) (list string))) end;