--- a/src/Pure/PIDE/protocol.ML Thu Mar 12 20:34:08 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Mar 12 22:00:51 2015 +0100
@@ -30,17 +30,20 @@
Isabelle_Process.protocol_command "Document.define_command"
(fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
let
- val blobs =
+ val (blobs, blobs_index) =
YXML.parse_body blobs_yxml |>
let open XML.Decode in
- list (variant
- [fn ([], a) => Exn.Res (pair string (option string) a),
- fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
+ pair
+ (list (variant
+ [fn ([], a) => Exn.Res (pair string (option string) a),
+ fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
+ int
end;
val toks =
(YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
in
- Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
+ Document.change_state
+ (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
end);
val _ =