src/Pure/PIDE/protocol.ML
changeset 70030 09f200c658ed
parent 70027 e02e3763e7a4
child 70469 3e17c3a5fd39
     1.1 --- a/src/Pure/PIDE/protocol.ML	Thu Feb 28 21:16:17 2019 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Feb 28 21:37:24 2019 +0100
     1.3 @@ -74,15 +74,18 @@
     1.4  val _ =
     1.5    Isabelle_Process.protocol_command "Document.update"
     1.6      (Future.task_context "Document.update" (Future.new_group NONE)
     1.7 -      (fn [old_id_string, new_id_string, edits_yxml, consolidate_yxml] =>
     1.8 +      (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml =>
     1.9          Document.change_state (fn state =>
    1.10            let
    1.11              val old_id = Document_ID.parse old_id_string;
    1.12              val new_id = Document_ID.parse new_id_string;
    1.13 +            val consolidate =
    1.14 +              YXML.parse_body consolidate_yxml |>
    1.15 +                let open XML.Decode in list string end;
    1.16              val edits =
    1.17 -              YXML.parse_body edits_yxml |>
    1.18 +              edits_yxml |> map (YXML.parse_body #>
    1.19                  let open XML.Decode in
    1.20 -                  list (pair string
    1.21 +                  pair string
    1.22                      (variant
    1.23                       [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    1.24                        fn ([], a) =>
    1.25 @@ -98,11 +101,8 @@
    1.26                          in Document.Deps {master = master, header = header, errors = errors} end,
    1.27                        fn (a :: b, c) =>
    1.28                          Document.Perspective (bool_atom a, map int_atom b,
    1.29 -                          list (pair int (pair string (list string))) c)]))
    1.30 -                end;
    1.31 -            val consolidate =
    1.32 -              YXML.parse_body consolidate_yxml |>
    1.33 -                let open XML.Decode in list string end;
    1.34 +                          list (pair int (pair string (list string))) c)])
    1.35 +                end);
    1.36  
    1.37              val _ = Execution.discontinue ();
    1.38