src/Pure/PIDE/isar_document.ML
changeset 43722 9b5dadb0c28d
parent 43713 1ba5331b4623
child 43724 4e58485fa320
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Sat Jul 09 21:53:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 00:21:19 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  val _ =
     1.6    Isabelle_Process.add_command "Isar_Document.edit_version"
     1.7 -    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
     1.8 +    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
     1.9        let
    1.10          val old_id = Document.parse_id old_id_string;
    1.11          val new_id = Document.parse_id new_id_string;
    1.12 @@ -26,9 +26,15 @@
    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  
    1.23        val await_cancellation = Document.cancel_execution state;
    1.24 -      val (updates, state') = Document.edit old_id new_id edits state;
    1.25 +      val (updates, state') = Document.edit old_id new_id edits headers state;
    1.26        val _ = await_cancellation ();
    1.27        val _ =
    1.28          Output.status (Markup.markup (Markup.assign new_id)