src/Pure/PIDE/isar_document.ML
changeset 43731 70072780e095
parent 43724 4e58485fa320
child 43748 c70bd78ec83c
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 17:58:11 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 20:59:04 2011 +0200
     1.3 @@ -18,10 +18,10 @@
     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_Data.Dest
     1.8 +          let open XML_Data.Decode
     1.9            in list (pair string (option (list (pair (option int) (option int))))) end;
    1.10          val headers = YXML.parse_body headers_yxml |>
    1.11 -          let open XML_Data.Dest
    1.12 +          let open XML_Data.Decode
    1.13            in list (pair string (triple string (list string) (list string))) end;
    1.14  
    1.15        val await_cancellation = Document.cancel_execution state;