src/Pure/PIDE/isar_document.ML
changeset 44157 a21d3e1e64fd
parent 44156 6aa25b80e1a5
child 44182 ecb51b457064
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Thu Aug 11 18:01:28 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 11 20:32:44 2011 +0200
     1.3 @@ -13,23 +13,24 @@
     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, headers_yxml] => Document.change_state (fn state =>
     1.8 +    (fn [old_id_string, new_id_string, edits_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 -        val edits = YXML.parse_body edits_yxml |>
    1.13 -          let open XML.Decode in
    1.14 -            list (pair string
    1.15 -              (variant
    1.16 -               [fn ([], []) => Document.Remove,
    1.17 -                fn ([], a) => Document.Edits (list (pair (option int) (option int)) a)]))
    1.18 -          end;
    1.19 -        val headers = YXML.parse_body headers_yxml |>
    1.20 -          let open XML.Decode
    1.21 -          in list (pair string (triple string (list string) (list string))) end;
    1.22 +        val edits =
    1.23 +          YXML.parse_body edits_yxml |>
    1.24 +            let open XML.Decode in
    1.25 +              list (pair string
    1.26 +                (variant
    1.27 +                 [fn ([], []) => Document.Remove,
    1.28 +                  fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    1.29 +                  fn ([], a) =>
    1.30 +                    Document.Update_Header (Exn.Res (triple string (list string) (list string) a)),
    1.31 +                  fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))]))
    1.32 +            end;
    1.33  
    1.34        val await_cancellation = Document.cancel_execution state;
    1.35 -      val (updates, state') = Document.edit old_id new_id edits headers state;
    1.36 +      val (updates, state') = Document.edit old_id new_id edits state;
    1.37        val _ = await_cancellation ();
    1.38        val _ =
    1.39          Output.status (Markup.markup (Markup.assign new_id)