# HG changeset patch
# User wenzelm
# Date 1567782623 -7200
# Node ID 4a358f8c7cb735e876e0eee508f56c4d8d53f875
# Parent  0f9a4e8ee1abf74a726aa900a75a7df78be2d6e2
clarified signature;

diff -r 0f9a4e8ee1ab -r 4a358f8c7cb7 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Sep 06 16:48:28 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 06 17:10:23 2019 +0200
@@ -19,8 +19,13 @@
   val init_state: state
   val define_blob: string -> string -> state -> state
   type blob_digest = (string * string option) Exn.result
-  val define_command: Document_ID.command -> string -> blob_digest list -> int ->
-    ((int * int) * string) list -> state -> state
+  type command =
+   {command_id: Document_ID.command,
+    name: string,
+    blobs_digests: blob_digest list,
+    blobs_index: int,
+    tokens: ((int * int) * string) list}
+  val define_command: command -> state -> state
   val command_exec: state -> string -> Document_ID.command -> Command.exec option
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
@@ -404,7 +409,14 @@
 
 (* commands *)
 
-fun define_command command_id name blobs_digests blobs_index toks =
+type command =
+  {command_id: Document_ID.command,
+   name: string,
+   blobs_digests: blob_digest list,
+   blobs_index: int,
+   tokens: ((int * int) * string) list};
+
+fun define_command {command_id, name, blobs_digests, blobs_index, tokens} =
   map_state (fn (versions, blobs, commands, execution) =>
     let
       val id = Document_ID.print command_id;
@@ -413,7 +425,7 @@
           Position.setmp_thread_data (Position.id_only id)
             (fn () =>
               let
-                val (tokens, _) = fold_map Token.make toks (Position.id id);
+                val (tokens, _) = fold_map Token.make tokens (Position.id id);
                 val _ =
                   if blobs_index < 0
                   then (*inlined errors*)
diff -r 0f9a4e8ee1ab -r 4a358f8c7cb7 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Sep 06 16:48:28 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML	Fri Sep 06 17:10:23 2019 +0200
@@ -39,29 +39,34 @@
   Isabelle_Process.protocol_command "Document.define_blob"
     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
 
+fun decode_command id name blobs_yxml toks_yxml sources : Document.command =
+  let
+    open XML.Decode;
+    val (blobs_digests, blobs_index) =
+      YXML.parse_body blobs_yxml |>
+        let
+          val message = YXML.string_of_body o Protocol_Message.command_positions id;
+        in
+          pair
+            (list (variant
+             [fn ([], a) => Exn.Res (pair string (option string) a),
+              fn ([], a) => Exn.Exn (ERROR (message a))]))
+            int
+        end;
+    val toks = YXML.parse_body toks_yxml |> list (pair int int);
+  in
+   {command_id = Document_ID.parse id,
+    name = name,
+    blobs_digests = blobs_digests,
+    blobs_index = blobs_index,
+    tokens = toks ~~ sources}
+  end;
+
 val _ =
   Isabelle_Process.protocol_command "Document.define_command"
     (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
-      let
-        val (blobs, blobs_index) =
-          YXML.parse_body blobs_yxml |>
-            let
-              val message =
-                YXML.string_of_body o Protocol_Message.command_positions id;
-              open XML.Decode;
-            in
-              pair
-                (list (variant
-                 [fn ([], a) => Exn.Res (pair string (option string) a),
-                  fn ([], a) => Exn.Exn (ERROR (message 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 blobs_index toks)
-      end);
+      Document.change_state
+        (Document.define_command (decode_command id name blobs_yxml toks_yxml sources)));
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"